Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.

Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.

Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.

Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.

Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) of type (set → (set → prop) → prop) → set.

Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set → (set → prop) → prop) → set → prop.

Theorem. (DescrR_i_io_12)

∀R : set → (set → prop) → prop, (∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) → R (DescrR_i_io_1 R) (DescrR_i_io_2 R)

In Proofgold the corresponding term root is a4fae2... and proposition id is da4f02...

Proof:
Proof not loaded.

Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.

Theorem. (PNoEq_ref_)

∀alpha, ∀p : set → prop, PNoEq_ alpha p p

In Proofgold the corresponding term root is c27ebb... and proposition id is df4cf6...

Proof:
Proof not loaded.

Theorem. (PNoEq_sym_)

∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p

In Proofgold the corresponding term root is b813f3... and proposition id is bfda0b...

Proof:
Proof not loaded.

Theorem. (PNoEq_tra_)

∀alpha, ∀p q r : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q r → PNoEq_ alpha p r

In Proofgold the corresponding term root is dded4c... and proposition id is fc92f3...

Proof:
Proof not loaded.

Theorem. (PNoEq_antimon_)

∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoEq_ alpha p q → PNoEq_ beta p q

In Proofgold the corresponding term root is 8868e6... and proposition id is 094ae2...

Proof:
Proof not loaded.

Definition. We define PNoLt_ to be λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type set → (set → prop) → (set → prop) → prop.

Theorem. (PNoLt_E_)

∀alpha, ∀p q : set → prop, PNoLt_ alpha p q → ∀R : prop, (∀beta, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → q beta → R) → R

In Proofgold the corresponding term root is 9ba543... and proposition id is 45aec8...

Proof:
Proof not loaded.

Theorem. (PNoLt_irref_)

∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p

In Proofgold the corresponding term root is fcb502... and proposition id is 987dff...

Proof:
Proof not loaded.

Theorem. (PNoLt_mon_)

∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoLt_ beta p q → PNoLt_ alpha p q

In Proofgold the corresponding term root is b1c3cf... and proposition id is d8d0f0...

Proof:
Proof not loaded.

Theorem. (PNoLt_trichotomy_or_)

∀p q : set → prop, ∀alpha, ordinal alpha → PNoLt_ alpha p q ∨ PNoEq_ alpha p q ∨ PNoLt_ alpha q p

In Proofgold the corresponding term root is 664408... and proposition id is 8d3824...

Proof:
Proof not loaded.

Theorem. (PNoLt_tra_)

∀alpha, ordinal alpha → ∀p q r : set → prop, PNoLt_ alpha p q → PNoLt_ alpha q r → PNoLt_ alpha p r

In Proofgold the corresponding term root is 3d7d91... and proposition id is 44767a...

Proof:
Proof not loaded.

Definition. We define PNoLt to be λalpha p beta q ⇒ PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta of type set → (set → prop) → set → (set → prop) → prop.

Theorem. (PNoLtI1)

∀alpha beta, ∀p q : set → prop, PNoLt_ (alpha ∩ beta) p q → PNoLt alpha p beta q

In Proofgold the corresponding term root is c5735c... and proposition id is ecbc71...

Proof:
Proof not loaded.

Theorem. (PNoLtI2)

∀alpha beta, ∀p q : set → prop, alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q

In Proofgold the corresponding term root is 419b53... and proposition id is 030093...

Proof:
Proof not loaded.

Theorem. (PNoLtI3)

∀alpha beta, ∀p q : set → prop, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → PNoLt alpha p beta q

In Proofgold the corresponding term root is c392cb... and proposition id is 410442...

Proof:
Proof not loaded.

Theorem. (PNoLtE)

∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → ∀R : prop, (PNoLt_ (alpha ∩ beta) p q → R) → (alpha ∈ beta → PNoEq_ alpha p q → q alpha → R) → (beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → R) → R

In Proofgold the corresponding term root is f7e6e3... and proposition id is af36ce...

Proof:
Proof not loaded.

Theorem. (PNoLt_irref)

∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p

In Proofgold the corresponding term root is ff1a80... and proposition id is d4c379...

Proof:
Proof not loaded.

Theorem. (PNoLt_trichotomy_or)

∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q ∨ PNoLt beta q alpha p

In Proofgold the corresponding term root is 4f39e4... and proposition id is 90b387...

Proof:
Proof not loaded.

Theorem. (PNoLtEq_tra)

∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoLt alpha p beta q → PNoEq_ beta q r → PNoLt alpha p beta r

In Proofgold the corresponding term root is 2e082a... and proposition id is 2f2a82...

Proof:
Proof not loaded.

Theorem. (PNoEqLt_tra)

∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLt alpha q beta r → PNoLt alpha p beta r

In Proofgold the corresponding term root is fe144b... and proposition id is f07654...

Proof:
Proof not loaded.

Theorem. (PNoLt_tra)

∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r

In Proofgold the corresponding term root is b72127... and proposition id is 8eff85...

Proof:
Proof not loaded.

Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type set → (set → prop) → set → (set → prop) → prop.

Theorem. (PNoLeI1)

∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → PNoLe alpha p beta q

In Proofgold the corresponding term root is 1f0528... and proposition id is 674a2c...

Proof:
Proof not loaded.

Theorem. (PNoLeI2)

∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q

In Proofgold the corresponding term root is b45332... and proposition id is 0b2157...

Proof:
Proof not loaded.

Theorem. (PNoLe_ref)

∀alpha, ∀p : set → prop, PNoLe alpha p alpha p

In Proofgold the corresponding term root is 1b91bd... and proposition id is 613386...

Proof:
Proof not loaded.

Theorem. (PNoLe_antisym)

∀alpha beta, ordinal alpha → ordinal beta → ∀p q : set → prop, PNoLe alpha p beta q → PNoLe beta q alpha p → alpha = beta ∧ PNoEq_ alpha p q

In Proofgold the corresponding term root is 934d7a... and proposition id is 4e3594...

Proof:
Proof not loaded.

Theorem. (PNoLtLe_tra)

∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLe beta q gamma r → PNoLt alpha p gamma r

In Proofgold the corresponding term root is 156586... and proposition id is 09246b...

Proof:
Proof not loaded.

Theorem. (PNoLeLt_tra)

∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r

In Proofgold the corresponding term root is a260ca... and proposition id is ad6971...

Proof:
Proof not loaded.

Theorem. (PNoEqLe_tra)

∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLe alpha q beta r → PNoLe alpha p beta r

In Proofgold the corresponding term root is 7d3ff8... and proposition id is 002ebf...

Proof:
Proof not loaded.

Theorem. (PNoLe_tra)

∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLe beta q gamma r → PNoLe alpha p gamma r

In Proofgold the corresponding term root is 70b92b... and proposition id is 4b557d...

Proof:
Proof not loaded.

Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoLe_downc)

∀L : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_downc L alpha p → PNoLe beta q alpha p → PNo_downc L beta q

In Proofgold the corresponding term root is 6b1f0d... and proposition id is cd130e...

Proof:
Proof not loaded.

Theorem. (PNo_downc_ref)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, L alpha p → PNo_downc L alpha p

In Proofgold the corresponding term root is 347aa9... and proposition id is 69dfcb...

Proof:
Proof not loaded.

Theorem. (PNo_upc_ref)

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, R alpha p → PNo_upc R alpha p

In Proofgold the corresponding term root is 403942... and proposition id is c4bf71...

Proof:
Proof not loaded.

Theorem. (PNoLe_upc)

∀R : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_upc R alpha p → PNoLe alpha p beta q → PNo_upc R beta q

In Proofgold the corresponding term root is 111b74... and proposition id is eb9ed5...

Proof:
Proof not loaded.

Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop, L gamma p → ∀delta, ordinal delta → ∀q : set → prop, R delta q → PNoLt gamma p delta q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → prop.

Theorem. (PNoLt_pwise_downc_upc)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)

In Proofgold the corresponding term root is 2b8e3b... and proposition id is 2f244c...

Proof:
Proof not loaded.

Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_downc L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_upc R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p ∧ PNo_rel_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoEq_rel_strict_upperbd)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L alpha q

In Proofgold the corresponding term root is bb65cf... and proposition id is db4b82...

Proof:
Proof not loaded.

Theorem. (PNo_rel_strict_upperbd_antimon)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p

In Proofgold the corresponding term root is 9986af... and proposition id is ed53da...

Proof:
Proof not loaded.

Theorem. (PNoEq_rel_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R alpha q

In Proofgold the corresponding term root is 76080e... and proposition id is 614e58...

Proof:
Proof not loaded.

Theorem. (PNo_rel_strict_lowerbd_antimon)

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p

In Proofgold the corresponding term root is 27f253... and proposition id is 344b63...

Proof:
Proof not loaded.

Theorem. (PNoEq_rel_strict_imv)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R alpha q

In Proofgold the corresponding term root is e3f251... and proposition id is 7ae13d...

Proof:
Proof not loaded.

Theorem. (PNo_rel_strict_imv_antimon)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p

In Proofgold the corresponding term root is 2434dc... and proposition id is 87e0ce...

Proof:
Proof not loaded.

Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∧ ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha) ∧ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNo_extend0_eq)

∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)

In Proofgold the corresponding term root is 2d441e... and proposition id is 5ed08e...

Proof:
Proof not loaded.

Theorem. (PNo_extend1_eq)

∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)

In Proofgold the corresponding term root is 8eb99c... and proposition id is 4cac1a...

Proof:
Proof not loaded.

Theorem. (PNo_rel_imv_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) ∨ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)

In Proofgold the corresponding term root is 3e3224... and proposition id is 749b63...

Proof:
Proof not loaded.

Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : set → prop, L beta p → beta ∈ alpha of type set → (set → (set → prop) → prop) → prop.

Theorem. (PNo_lenbdd_strict_imv_extend0)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)

In Proofgold the corresponding term root is 17a114... and proposition id is 69327e...

Proof:
Proof not loaded.

Theorem. (PNo_lenbdd_strict_imv_extend1)

In Proofgold the corresponding term root is ad69ec... and proposition id is 5ff993...

Proof:
Proof not loaded.

Theorem. (PNo_lenbdd_strict_imv_split)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_split_imv L R alpha p

In Proofgold the corresponding term root is 76ae4f... and proposition id is f98998...

Proof:
Proof not loaded.

Theorem. (PNo_rel_imv_bdd_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R beta p

In Proofgold the corresponding term root is 9a98e4... and proposition id is 25bcd2...

Proof:
Proof not loaded.

Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNoEq_strict_upperbd)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_upperbd L alpha p → PNo_strict_upperbd L alpha q

In Proofgold the corresponding term root is 9b7b8e... and proposition id is f28b04...

Proof:
Proof not loaded.

Theorem. (PNoEq_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_lowerbd R alpha p → PNo_strict_lowerbd R alpha q

In Proofgold the corresponding term root is 4db3f9... and proposition id is 67fa73...

Proof:
Proof not loaded.

Theorem. (PNoEq_strict_imv)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_imv L R alpha p → PNo_strict_imv L R alpha q

In Proofgold the corresponding term root is 1ec352... and proposition id is 5f582f...

Proof:
Proof not loaded.

Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p

In Proofgold the corresponding term root is 2898f0... and proposition id is 3cdd3b...

Proof:
Proof not loaded.

Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p

In Proofgold the corresponding term root is 442af5... and proposition id is 04acc2...

Proof:
Proof not loaded.

Theorem. (PNo_strict_imv_imp_rel_strict_imv)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p

In Proofgold the corresponding term root is f4fc71... and proposition id is 46a6aa...

Proof:
Proof not loaded.

Theorem. (PNo_rel_split_imv_imp_strict_imv)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, PNo_rel_strict_split_imv L R alpha p → PNo_strict_imv L R alpha p

In Proofgold the corresponding term root is 72be36... and proposition id is adfdb0...

Proof:
Proof not loaded.

Theorem. (PNo_lenbdd_strict_imv_ex)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_strict_imv L R beta p

In Proofgold the corresponding term root is 9485d6... and proposition id is a864a5...

Proof:
Proof not loaded.

Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta ∧ PNo_strict_imv L R beta p ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.

Theorem. (PNo_strict_imv_pred_eq)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → ∀p q : set → prop, PNo_least_rep L R alpha p → PNo_strict_imv L R alpha q → ∀beta ∈ alpha, p beta ↔ q beta

In Proofgold the corresponding term root is 5e7822... and proposition id is 72e14d...

Proof:
Proof not loaded.

Theorem. (PNo_lenbdd_least_rep2_exuniq2)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta, (∃p : set → prop, PNo_least_rep2 L R beta p) ∧ (∀p q : set → prop, PNo_least_rep2 L R beta p → PNo_least_rep2 L R beta q → p = q)

In Proofgold the corresponding term root is 5060a9... and proposition id is 8b62c5...

Proof:
Proof not loaded.

Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.

Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.

Theorem. (PNo_bd_pred_lem)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)

In Proofgold the corresponding term root is 749b8f... and proposition id is 5de4a3...

Proof:
Proof not loaded.

Theorem. (PNo_bd_pred)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep L R (PNo_bd L R) (PNo_pred L R)

In Proofgold the corresponding term root is 42224b... and proposition id is 3309f6...

Proof:
Proof not loaded.

Theorem. (PNo_bd_In)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_bd L R ∈ ordsucc alpha

In Proofgold the corresponding term root is ad857b... and proposition id is 4719e1...

Proof:
Proof not loaded.