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.
Primitive. The name DescrR_i_io_1 is a term of type (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is 1d3fd4... and object id is 82aecc...
Primitive. The name DescrR_i_io_2 is a term of type (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is 768eb2... and object id is 3f82bc...
Axiom. (DescrR_i_io_12) We take the following as an axiom:
∀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...
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.
In Proofgold the corresponding term root is d7d959... and object id is 144b65...
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
In Proofgold the corresponding term root is c27ebb... and proposition id is df4cf6...
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀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...
Axiom. (PNoEq_tra_) We take the following as an axiom:
∀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...
Axiom. (PNoEq_antimon_) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 34de68... and object id is c95964...
Axiom. (PNoLt_E_) We take the following as an axiom:
∀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...
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
In Proofgold the corresponding term root is fcb502... and proposition id is 987dff...
Axiom. (PNoLt_mon_) We take the following as an axiom:
∀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...
Axiom. (PNoLt_trichotomy_or_) We take the following as an axiom:
∀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...
Axiom. (PNoLt_tra_) We take the following as an axiom:
∀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...
Primitive. The name PNoLt is a term of type set → (set → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 8f57a0... and object id is f2094c...
Axiom. (PNoLtI1) We take the following as an axiom:
∀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...
Axiom. (PNoLtI2) We take the following as an axiom:
∀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...
Axiom. (PNoLtI3) We take the following as an axiom:
∀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...
Axiom. (PNoLtE) We take the following as an axiom:
∀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...
Axiom. (PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
In Proofgold the corresponding term root is ff1a80... and proposition id is d4c379...
Axiom. (PNoLt_trichotomy_or) We take the following as an axiom:
∀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...
Axiom. (PNoLtEq_tra) We take the following as an axiom:
∀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...
Axiom. (PNoEqLt_tra) We take the following as an axiom:
∀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...
Axiom. (PNoLt_tra) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is ac6311... and object id is 770cf7...
Axiom. (PNoLeI1) We take the following as an axiom:
∀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...
Axiom. (PNoLeI2) We take the following as an axiom:
∀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...
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
In Proofgold the corresponding term root is 1b91bd... and proposition id is 613386...
Axiom. (PNoLe_antisym) We take the following as an axiom:
∀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...
Axiom. (PNoLtLe_tra) We take the following as an axiom:
∀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...
Axiom. (PNoLeLt_tra) We take the following as an axiom:
∀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...
Axiom. (PNoEqLe_tra) We take the following as an axiom:
∀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...
Axiom. (PNoLe_tra) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 93dab1... and object id is f6c962...
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.
In Proofgold the corresponding term root is 543712... and object id is b97935...
Axiom. (PNoLe_downc) We take the following as an axiom:
∀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...
Axiom. (PNo_downc_ref) We take the following as an axiom:
∀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...
Axiom. (PNo_upc_ref) We take the following as an axiom:
∀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...
Axiom. (PNoLe_upc) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is ae448b... and object id is 123808...
Axiom. (PNoLt_pwise_downc_upc) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is dc1665... and object id is 3e1663...
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.
In Proofgold the corresponding term root is e5a4b6... and object id is ff3150...
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.
In Proofgold the corresponding term root is 64ce99... and object id is 5b35fb...
Axiom. (PNoEq_rel_strict_upperbd) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_strict_upperbd_antimon) We take the following as an axiom:
∀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...
Axiom. (PNoEq_rel_strict_lowerbd) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_strict_lowerbd_antimon) We take the following as an axiom:
∀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...
Axiom. (PNoEq_rel_strict_imv) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_strict_imv_antimon) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 23c9d9... and object id is 56ed1b...
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.
In Proofgold the corresponding term root is 217d17... and object id is dd9cee...
Axiom. (PNo_extend0_eq) We take the following as an axiom:
∀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...
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_imv_ex) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 009fa7... and object id is a452a6...
Axiom. (PNo_lenbdd_strict_imv_extend0) We take the following as an axiom:
∀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...
Axiom. (PNo_lenbdd_strict_imv_extend1) We take the following as an axiom:
∀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 ad69ec... and proposition id is 5ff993...
Axiom. (PNo_lenbdd_strict_imv_split) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_imv_bdd_ex) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 6913bd... and object id is 3723ab...
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.
In Proofgold the corresponding term root is 87fac4... and object id is 3606d4...
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.
In Proofgold the corresponding term root is ee97f6... and object id is bc6c55...
Axiom. (PNoEq_strict_upperbd) We take the following as an axiom:
∀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...
Axiom. (PNoEq_strict_lowerbd) We take the following as an axiom:
∀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...
Axiom. (PNoEq_strict_imv) We take the following as an axiom:
∀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...
Axiom. (PNo_strict_upperbd_imp_rel_strict_upperbd) We take the following as an axiom:
∀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...
Axiom. (PNo_strict_lowerbd_imp_rel_strict_lowerbd) We take the following as an axiom:
∀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...
Axiom. (PNo_strict_imv_imp_rel_strict_imv) We take the following as an axiom:
∀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...
Axiom. (PNo_rel_split_imv_imp_strict_imv) We take the following as an axiom:
∀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...
Axiom. (PNo_lenbdd_strict_imv_ex) We take the following as an axiom:
∀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...
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.
In Proofgold the corresponding term root is 0711e2... and object id is e4c707...
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.
In Proofgold the corresponding term root is 1f6dc5... and object id is 09d320...
Axiom. (PNo_strict_imv_pred_eq) We take the following as an axiom:
∀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...
Axiom. (PNo_lenbdd_least_rep2_exuniq2) We take the following as an axiom:
∀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...
Primitive. The name PNo_bd is a term of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is ed76e7... and object id is aa75ef...
Primitive. The name PNo_pred is a term of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is b2d51d... and object id is 2efd18...
Axiom. (PNo_bd_pred_lem) We take the following as an axiom:
∀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...
Axiom. (PNo_bd_pred) We take the following as an axiom:
∀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...
Axiom. (PNo_bd_In) We take the following as an axiom:
∀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...