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.
Primitive. The name
DescrR_i_io_2 is a term of type
(set → (set → prop) → prop) → set → prop.
L14Axiom. (
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)
L15Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type
set → (set → prop) → (set → prop) → prop.
L16Axiom. (
PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
L17Axiom. (
PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
L18Axiom. (
PNoEq_tra_) We take the following as an axiom:
L19Axiom. (
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
L20Definition. 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.
L21Axiom. (
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
L22Axiom. (
PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
L23Axiom. (
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
L25Axiom. (
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
Primitive. The name
PNoLt is a term of type
set → (set → prop) → set → (set → prop) → prop.
L28Axiom. (
PNoLtI1) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, PNoLt_ (alpha ∩ beta) p q → PNoLt alpha p beta q
L29Axiom. (
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
L30Axiom. (
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
L31Axiom. (
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
L32Axiom. (
PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
L33Axiom. (
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
L34Axiom. (
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
L35Axiom. (
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
L36Axiom. (
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
L37Definition. 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.
L38Axiom. (
PNoLeI1) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → PNoLe alpha p beta q
L39Axiom. (
PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
L40Axiom. (
PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
L41Axiom. (
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
L42Axiom. (
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
L43Axiom. (
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
L44Axiom. (
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
L45Axiom. (
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
L46Definition. 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.
L47Definition. 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.
L48Axiom. (
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
L49Axiom. (
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
L50Axiom. (
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
L51Axiom. (
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
L52Definition. 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.
L54Definition. 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.
L55Definition. 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.
L64Definition. 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.
L65Axiom. (
PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
L66Axiom. (
PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
L68Definition. 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.
L73Definition. 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.
L74Definition. 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.
L84Definition. 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.
L85Definition. 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.
Primitive. The name
PNo_bd is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
Primitive. The name
PNo_pred is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
L93Axiom. (
PNo_bd_pred) We take the following as an axiom:
L94Axiom. (
PNo_bd_In) We take the following as an axiom: