Primitive. The name
Eps_i is a term of type
(set → prop) → set.
L110Axiom. (
Eps_i_R) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
Primitive. The name
False is a term of type
prop.
Primitive. The name
True is a term of type
prop.
Primitive. The name
not is a term of type
prop → prop.
Notation. We use
¬ as a prefix operator with priority 700 corresponding to applying term
not.
L122Axiom. (
dneg) We take the following as an axiom:
Primitive. The name
and is a term of type
prop → prop → prop.
Notation. We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and.
Primitive. The name
or is a term of type
prop → prop → prop.
Notation. We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or.
Primitive. The name
iff is a term of type
prop → prop → prop.
Notation. We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff.
Beginning of Section Eq
L143Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
L145Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop.
End of Section Eq
Notation. We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq.
Notation. We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq.
Beginning of Section Ex
L156Definition. We define
ex to be
λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type
(A → prop) → prop.
End of Section Ex
Notation. We use
∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex.
Beginning of Section FE
L168Axiom. (
func_ext) We take the following as an axiom:
∀f g : A → B, (∀x : A, f x = g x) → f = g
End of Section FE
L170Axiom. (
prop_ext) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A = B
Primitive. The name
In is a term of type
set → set → prop.
Notation. We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In. Furthermore, we may write
∀ x ∈ A, B to mean
∀ x : set, x ∈ A → B.
Primitive. The name
Subq is a term of type
set → set → prop.
Notation. We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq. Furthermore, we may write
∀ x ⊆ A, B to mean
∀ x : set, x ⊆ A → B.
Notation. We use
∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and.
L184Axiom. (
set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
Primitive. The name
∅ is a term of type
set.
L193Axiom. (
EmptyAx) We take the following as an axiom:
Primitive. The name
⋃ is a term of type
set → set.
L198Axiom. (
UnionEq) We take the following as an axiom:
∀X : set, ∀x : set, x ∈ ⋃ X ↔ ∃Y : set, x ∈ Y ∧ Y ∈ X
Primitive. The name
𝒫 is a term of type
set → set.
L205Axiom. (
PowerEq) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X ↔ Y ⊆ X
Primitive. The name
Repl is a term of type
set → (set → set) → set.
Notation.
{B| x ∈ A} is notation for
Repl A (λ x . B).
L215Axiom. (
ReplEq) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X} ↔ ∃x : set, x ∈ X ∧ y = F x
Primitive. The name
TransSet is a term of type
set → prop.
L220Axiom. (
HF_Min) We take the following as an axiom:
∀p : set → prop, (∀X, p X → ∀x ∈ X, p x) → p ∅ → (∀X, p X → p (⋃ X)) → (∀X, p X → p (𝒫 X)) → (∀X, p X → ∀F : set → set, (∀x ∈ X, p (F x)) → p {F x|x ∈ X}) → ∀x, p x
L228Axiom. (
In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x : set, x ∈ X → P x) → P X) → ∀X : set, P X
Primitive. The name
atleast2 is a term of type
set → prop.
Primitive. The name
atleast3 is a term of type
set → prop.
Primitive. The name
atleast4 is a term of type
set → prop.
Primitive. The name
atleast5 is a term of type
set → prop.
Primitive. The name
atleast6 is a term of type
set → prop.
Primitive. The name
exactly2 is a term of type
set → prop.
Primitive. The name
exactly3 is a term of type
set → prop.
Primitive. The name
exactly4 is a term of type
set → prop.
Primitive. The name
exactly5 is a term of type
set → prop.
Primitive. The name
exu_i is a term of type
(set → prop) → prop.
Primitive. The name
reflexive_i is a term of type
(set → set → prop) → prop.
Primitive. The name
irreflexive_i is a term of type
(set → set → prop) → prop.
Primitive. The name
symmetric_i is a term of type
(set → set → prop) → prop.
Primitive. The name
antisymmetric_i is a term of type
(set → set → prop) → prop.
Primitive. The name
transitive_i is a term of type
(set → set → prop) → prop.
Primitive. The name
eqreln_i is a term of type
(set → set → prop) → prop.
Primitive. The name
per_i is a term of type
(set → set → prop) → prop.
Primitive. The name
linear_i is a term of type
(set → set → prop) → prop.
Primitive. The name
partialorder_i is a term of type
(set → set → prop) → prop.
Primitive. The name
totalorder_i is a term of type
(set → set → prop) → prop.
Primitive. The name
If_i is a term of type
prop → set → set → set.
Primitive. The name
exactly1of2 is a term of type
prop → prop → prop.
Primitive. The name
exactly1of3 is a term of type
prop → prop → prop → prop.
Primitive. The name
nIn is a term of type
set → set → prop.
Primitive. The name
nSubq is a term of type
set → set → prop.
Primitive. The name
UPair is a term of type
set → set → set.
Primitive. The name
Sing is a term of type
set → set.
Primitive. The name
binunion is a term of type
set → set → set.
Primitive. The name
SetAdjoin is a term of type
set → set → set.
Primitive. The name
famunion is a term of type
set → (set → set) → set.
Primitive. The name
Sep is a term of type
set → (set → prop) → set.
Notation.
{x ∈ A | B} is notation for
Sep A (λ x . B).
Primitive. The name
ReplSep is a term of type
set → (set → prop) → (set → set) → set.
Notation.
{B| x ∈ A, C} is notation for
ReplSep A (λ x . C) (λ x . B).
Primitive. The name
binintersect is a term of type
set → set → set.
Notation. We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect.
Primitive. The name
setminus is a term of type
set → set → set.
Notation. We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus.
Primitive. The name
inj is a term of type
set → set → (set → set) → prop.
Primitive. The name
bij is a term of type
set → set → (set → set) → prop.
Primitive. The name
atleastp is a term of type
set → set → prop.
Primitive. The name
equip is a term of type
set → set → prop.
Primitive. The name
In_rec_G_i is a term of type
(set → (set → set) → set) → set → set → prop.
Primitive. The name
In_rec_i is a term of type
(set → (set → set) → set) → set → set.
Primitive. The name
ordsucc is a term of type
set → set.
Primitive. The name
nat_p is a term of type
set → prop.
Primitive. The name
nat_primrec is a term of type
set → (set → set → set) → set → set.
Primitive. The name
add_nat is a term of type
set → set → set.
Primitive. The name
mul_nat is a term of type
set → set → set.
Primitive. The name
ordinal is a term of type
set → prop.
Primitive. The name
V_ is a term of type
set → set.
Primitive. The name
Inj1 is a term of type
set → set.
Primitive. The name
Inj0 is a term of type
set → set.
Primitive. The name
Unj is a term of type
set → set.
Primitive. The name
combine_funcs is a term of type
set → set → (set → set) → (set → set) → set → set.
Primitive. The name
setsum is a term of type
set → set → set.
Primitive. The name
proj0 is a term of type
set → set.
Primitive. The name
proj1 is a term of type
set → set.
Primitive. The name
binrep is a term of type
set → set → set.
Primitive. The name
lam is a term of type
set → (set → set) → set.
Primitive. The name
setprod is a term of type
set → set → set.
Primitive. The name
ap is a term of type
set → set → set.
Primitive. The name
setsum_p is a term of type
set → prop.
Primitive. The name
tuple_p is a term of type
set → set → prop.
Primitive. The name
Pi is a term of type
set → (set → set) → set.
Primitive. The name
setexp is a term of type
set → set → set.
Primitive. The name
Sep2 is a term of type
set → (set → set) → (set → set → prop) → set.
Primitive. The name
set_of_pairs is a term of type
set → prop.
Primitive. The name
lam2 is a term of type
set → (set → set) → (set → set → set) → set.
Primitive. The name
PNoEq_ is a term of type
set → (set → prop) → (set → prop) → prop.
Primitive. The name
PNoLt_ is a term of type
set → (set → prop) → (set → prop) → prop.
Primitive. The name
PNoLt is a term of type
set → (set → prop) → set → (set → prop) → prop.
Primitive. The name
PNoLe is a term of type
set → (set → prop) → set → (set → prop) → prop.
Primitive. The name
PNo_downc is a term of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
Primitive. The name
PNo_upc is a term of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
Primitive. The name
SNoElts_ is a term of type
set → set.
Primitive. The name
SNo_ is a term of type
set → set → prop.
Primitive. The name
PSNo is a term of type
set → (set → prop) → set.
Primitive. The name
SNo is a term of type
set → prop.
Primitive. The name
SNoLev is a term of type
set → set.
Primitive. The name
SNoEq_ is a term of type
set → set → set → prop.
Primitive. The name
SNoLt is a term of type
set → set → prop.
Primitive. The name
SNoLe is a term of type
set → set → prop.
Primitive. The name
binop_on is a term of type
set → (set → set → set) → prop.
Primitive. The name
Loop is a term of type
set → (set → set → set) → (set → set → set) → (set → set → set) → set → prop.
Primitive. The name
Loop_with_defs is a term of type
set → (set → set → set) → (set → set → set) → (set → set → set) → set → (set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → prop.
Primitive. The name
Loop_with_defs_cex1 is a term of type
set → (set → set → set) → (set → set → set) → (set → set → set) → set → (set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → prop.
Primitive. The name
Loop_with_defs_cex2 is a term of type
set → (set → set → set) → (set → set → set) → (set → set → set) → set → (set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set → set) → (set → set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → (set → set → set) → prop.
Primitive. The name
combinator is a term of type
set → prop.
Primitive. The name
equip_mod is a term of type
set → set → set → prop.
L358Axiom. (
False_def) We take the following as an axiom:
L360Axiom. (
True_def) We take the following as an axiom:
True = (∀X0 : prop, (X0 → X0))
L361Axiom. (
not_def) We take the following as an axiom:
L362Axiom. (
and_def) We take the following as an axiom:
and = (λA B : prop ⇒ ∀P : prop, (A → B → P) → P)
L363Axiom. (
or_def) We take the following as an axiom:
or = (λA B : prop ⇒ ∀P : prop, (A → P) → (B → P) → P)
L364Axiom. (
iff_def) We take the following as an axiom:
iff = (λA B : prop ⇒ (A → B) ∧ (B → A))
L365Axiom. (
Subq_def) We take the following as an axiom:
Subq = (λX Y ⇒ ∀x : set, x ∈ X → x ∈ Y)
L376Axiom. (
exu_i_def) We take the following as an axiom:
exu_i = (λX0 : set → prop ⇒ (and (∃X1 : set, (X0 X1)) (∀X1 : set, (∀X2 : set, ((X0 X1) → ((X0 X2) → (X1 = X2)))))))
L379Axiom. (
symmetric_i_def) We take the following as an axiom:
symmetric_i = (λX0 : set → set → prop ⇒ (∀X1 : set, (∀X2 : set, ((X0 X1 X2) → (X0 X2 X1)))))
L381Axiom. (
transitive_i_def) We take the following as an axiom:
transitive_i = (λX0 : set → set → prop ⇒ (∀X1 : set, (∀X2 : set, (∀X3 : set, ((X0 X1 X2) → ((X0 X2 X3) → (X0 X1 X3)))))))
L383Axiom. (
per_i_def) We take the following as an axiom:
L384Axiom. (
linear_i_def) We take the following as an axiom:
linear_i = (λX0 : set → set → prop ⇒ (∀X1 : set, (∀X2 : set, (or (X0 X1 X2) (X0 X2 X1)))))
L390Axiom. (
If_i_def) We take the following as an axiom:
If_i = (λX0 : prop ⇒ (λX1 : set ⇒ (λX2 : set ⇒ (Eps_i (λX3 : set ⇒ (or (and X0 (X3 = X1)) (and (not X0) (X3 = X2))))))))
L393Axiom. (
nIn_def) We take the following as an axiom:
nIn = (λX0 : set ⇒ (λX1 : set ⇒ (not (In X0 X1))))
L394Axiom. (
nSubq_def) We take the following as an axiom:
L395Axiom. (
UPair_def) We take the following as an axiom:
L396Axiom. (
Sing_def) We take the following as an axiom:
L399Axiom. (
famunion_def) We take the following as an axiom:
famunion = (λX0 : set ⇒ (λX1 : set → set ⇒ (⋃ (Repl X0 (λX2 : set ⇒ (X1 X2))))))
L400Axiom. (
Sep_def) We take the following as an axiom:
Sep = (λX0 : set ⇒ (λX1 : set → prop ⇒ (If_i (∃X2 : set, (and (In X2 X0) (X1 X2))) (Repl X0 (λX2 : set ⇒ ((λX3 : set ⇒ (If_i (X1 X3) X3 (Eps_i (λX4 : set ⇒ (and (In X4 X0) (X1 X4)))))) X2))) ∅)))
L401Axiom. (
ReplSep_def) We take the following as an axiom:
ReplSep = (λX0 : set ⇒ (λX1 : set → prop ⇒ (λX2 : set → set ⇒ (Repl (Sep X0 (λX3 : set ⇒ (X1 X3))) (λX3 : set ⇒ (X2 X3))))))
L404Axiom. (
inj_def) We take the following as an axiom:
inj = (λX0 : set ⇒ (λX1 : set ⇒ (λX2 : set → set ⇒ (and (∀X3 : set, ((In X3 X0) → (In (X2 X3) X1))) (∀X3 : set, ((In X3 X0) → (∀X4 : set, ((In X4 X0) → (((X2 X3) = (X2 X4)) → (X3 = X4))))))))))
L405Axiom. (
bij_def) We take the following as an axiom:
bij = (λX0 : set ⇒ (λX1 : set ⇒ (λX2 : set → set ⇒ (and (inj X0 X1 X2) (∀X3 : set, ((In X3 X1) → (∃X4 : set, (and (In X4 X0) ((X2 X4) = X3)))))))))
L407Axiom. (
equip_def) We take the following as an axiom:
L408Axiom. (
In_rec_G_i_def) We take the following as an axiom:
In_rec_G_i = (λX0 : set → (set → set) → set ⇒ (λX1 : set ⇒ (λX2 : set ⇒ (∀X3 : set → set → prop, ((∀X4 : set, (∀X5 : set → set, ((∀X6 : set, ((In X6 X4) → (X3 X6 (X5 X6)))) → (X3 X4 (X0 X4 X5))))) → (X3 X1 X2))))))
L410Axiom. (
ordsucc_def) We take the following as an axiom:
L411Axiom. (
nat_p_def) We take the following as an axiom:
nat_p = (λX0 : set ⇒ (∀X1 : set → prop, ((X1 ∅) → ((∀X2 : set, ((X1 X2) → (X1 (ordsucc X2)))) → (X1 X0)))))
L413Axiom. (
add_nat_def) We take the following as an axiom:
L414Axiom. (
mul_nat_def) We take the following as an axiom:
L415Axiom. (
ordinal_def) We take the following as an axiom:
L416Axiom. (
V__def) We take the following as an axiom:
L417Axiom. (
Inj1_def) We take the following as an axiom:
L418Axiom. (
Inj0_def) We take the following as an axiom:
L419Axiom. (
Unj_def) We take the following as an axiom:
L421Axiom. (
setsum_def) We take the following as an axiom:
L422Axiom. (
proj0_def) We take the following as an axiom:
L423Axiom. (
proj1_def) We take the following as an axiom:
L424Axiom. (
binrep_def) We take the following as an axiom:
L425Axiom. (
lam_def) We take the following as an axiom:
lam = (λX0 : set ⇒ (λX1 : set → set ⇒ (famunion X0 (λX2 : set ⇒ (Repl (X1 X2) (λX3 : set ⇒ (setsum X2 X3)))))))
L426Axiom. (
setprod_def) We take the following as an axiom:
setprod = (λX0 : set ⇒ (λX1 : set ⇒ (lam X0 (λX2 : set ⇒ X1))))
L427Axiom. (
ap_def) We take the following as an axiom:
ap = (λX0 : set ⇒ (λX1 : set ⇒ (ReplSep X0 (λX2 : set ⇒ (∃X3 : set, (X2 = (setsum X1 X3)))) (λX2 : set ⇒ (proj1 X2)))))
L429Axiom. (
tuple_p_def) We take the following as an axiom:
tuple_p = (λX0 : set ⇒ (λX1 : set ⇒ (∀X2 : set, ((In X2 X1) → (∃X3 : set, (and (In X3 X0) (∃X4 : set, (X2 = (setsum X3 X4)))))))))
L430Axiom. (
Pi_def) We take the following as an axiom:
Pi = (λX0 : set ⇒ (λX1 : set → set ⇒ (Sep (𝒫 (lam X0 (λX2 : set ⇒ (⋃ (X1 X2))))) (λX2 : set ⇒ (∀X3 : set, ((In X3 X0) → (In (ap X2 X3) (X1 X3))))))))
L431Axiom. (
setexp_def) We take the following as an axiom:
setexp = (λX0 : set ⇒ (λX1 : set ⇒ (Pi X1 (λX2 : set ⇒ X0))))
L432Axiom. (
Sep2_def) We take the following as an axiom:
Sep2 = (λX0 : set ⇒ (λX1 : set → set ⇒ (λX2 : set → set → prop ⇒ (Sep (lam X0 (λX3 : set ⇒ (X1 X3))) (λX3 : set ⇒ (X2 (ap X3 ∅) (ap X3 (ordsucc ∅))))))))
L434Axiom. (
lam2_def) We take the following as an axiom:
lam2 = (λX0 : set ⇒ (λX1 : set → set ⇒ (λX2 : set → set → set ⇒ (lam X0 (λX3 : set ⇒ (lam (X1 X3) (λX4 : set ⇒ (X2 X3 X4))))))))
L435Axiom. (
PNoEq__def) We take the following as an axiom:
PNoEq_ = (λX0 : set ⇒ (λX1 : set → prop ⇒ (λX2 : set → prop ⇒ (∀X3 : set, ((In X3 X0) → (iff (X1 X3) (X2 X3)))))))
L436Axiom. (
PNoLt__def) We take the following as an axiom:
PNoLt_ = (λX0 : set ⇒ (λX1 : set → prop ⇒ (λX2 : set → prop ⇒ (∃X3 : set, (and (In X3 X0) (and (and (PNoEq_ X3 X1 X2) (not (X1 X3))) (X2 X3)))))))
L437Axiom. (
PNoLt_def) We take the following as an axiom:
L438Axiom. (
PNoLe_def) We take the following as an axiom:
PNoLe = (λX0 : set ⇒ (λX1 : set → prop ⇒ (λX2 : set ⇒ (λX3 : set → prop ⇒ (or (PNoLt X0 X1 X2 X3) (and (X0 = X2) (PNoEq_ X0 X1 X3)))))))
L439Axiom. (
PNo_downc_def) We take the following as an axiom:
PNo_downc = (λX0 : set → (set → prop) → prop ⇒ (λX1 : set ⇒ (λX2 : set → prop ⇒ (∃X3 : set, (and (ordinal X3) (∃X4 : set → prop, (and (X0 X3 X4) (PNoLe X1 X2 X3 X4))))))))
L440Axiom. (
PNo_upc_def) We take the following as an axiom:
PNo_upc = (λX0 : set → (set → prop) → prop ⇒ (λX1 : set ⇒ (λX2 : set → prop ⇒ (∃X3 : set, (and (ordinal X3) (∃X4 : set → prop, (and (X0 X3 X4) (PNoLe X3 X4 X1 X2))))))))
L442Axiom. (
SNo__def) We take the following as an axiom:
L443Axiom. (
PSNo_def) We take the following as an axiom:
L444Axiom. (
SNo_def) We take the following as an axiom:
L445Axiom. (
SNoLev_def) We take the following as an axiom:
L446Axiom. (
SNoEq__def) We take the following as an axiom:
SNoEq_ = (λX0 : set ⇒ (λX1 : set ⇒ (λX2 : set ⇒ (PNoEq_ X0 (λX3 : set ⇒ (In X3 X1)) (λX3 : set ⇒ (In X3 X2))))))
L447Axiom. (
SNoLt_def) We take the following as an axiom:
L448Axiom. (
SNoLe_def) We take the following as an axiom:
L449Axiom. (
binop_on_def) We take the following as an axiom:
binop_on = (λX0 : set ⇒ (λX1 : set → set → set ⇒ (∀X2 : set, ((In X2 X0) → (∀X3 : set, ((In X3 X0) → (In (X1 X2 X3) X0)))))))
L450Axiom. (
Loop_def) We take the following as an axiom:
Loop = (λX : set ⇒ (λm b s : set → set → set ⇒ (λe : set ⇒ binop_on X m ∧ binop_on X b ∧ binop_on X s ∧ (∀x ∈ X, (m e x = x ∧ m x e = x)) ∧ (∀x y ∈ X, (b x (m x y) = y ∧ m x (b x y) = y ∧ s (m x y) y = x ∧ m (s x y) y = x)))))
L456Axiom. (
Loop_with_defs_def) We take the following as an axiom:
Loop_with_defs = λX m b s e K a T L R I1 J1 I2 J2 ⇒ Loop X m b s e ∧ (∀x y ∈ X, K x y = b (m y x) (m x y)) ∧ (∀x y z ∈ X, a x y z = b (m x (m y z)) (m (m x y) z)) ∧ (∀x u ∈ X, T x u = b x (m u x) ∧ I1 x u = m x (m u (b x e)) ∧ J1 x u = m (m (s e x) u) x ∧ I2 x u = m (b x u) (b (b x e) e) ∧ J2 x u = m (s e (s e x)) (s u x)) ∧ (∀x y u ∈ X, L x y u = b (m y x) (m y (m x u)) ∧ R x y u = s (m (m u x) y) (m x y))
L493Axiom. (
TrueI) We take the following as an axiom:
L495Axiom. (
FalseE) We take the following as an axiom:
L496Axiom. (
notE) We take the following as an axiom:
L497Axiom. (
notI) We take the following as an axiom:
L498Axiom. (
andE) We take the following as an axiom:
∀A B : prop, A ∧ B → ∀p : prop, (A → B → p) → p
L499Axiom. (
andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
L500Axiom. (
orE) We take the following as an axiom:
∀A B : prop, A ∨ B → ∀p : prop, (A → p) → (B → p) → p
L501Axiom. (
orIL) We take the following as an axiom:
L502Axiom. (
orIR) We take the following as an axiom:
L503Axiom. (
xm) We take the following as an axiom:
L504Axiom. (
xmcases) We take the following as an axiom:
∀A p : prop, (A → p) → (¬ A → p) → p
L505Axiom. (
iffE) We take the following as an axiom:
∀A B : prop, (A ↔ B) → ∀p : prop, (A → B → p) → (¬ A → ¬ B → p) → p
L506Axiom. (
iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
Notation. We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn.
Notation. We use
⊈ as an infix operator with priority 502 and no associativity corresponding to applying term
nSubq.
L513Axiom. (
dnegI) We take the following as an axiom:
L515Axiom. (
contra) We take the following as an axiom:
L516Axiom. (
keepcopy) We take the following as an axiom:
L517Axiom. (
orI_contra) We take the following as an axiom:
∀p q : prop, (¬ p → ¬ q → False) → p ∨ q
L518Axiom. (
orI_imp1) We take the following as an axiom:
∀p q : prop, (p → q) → ¬ p ∨ q
L519Axiom. (
orI_imp2) We take the following as an axiom:
∀p q : prop, (q → p) → p ∨ ¬ q
L521Axiom. (
tab_pos_and) We take the following as an axiom:
L522Axiom. (
tab_pos_or) We take the following as an axiom:
L523Axiom. (
tab_pos_imp) We take the following as an axiom:
L524Axiom. (
tab_pos_iff) We take the following as an axiom:
L525Axiom. (
tab_neg_imp) We take the following as an axiom:
L526Axiom. (
tab_neg_and) We take the following as an axiom:
L527Axiom. (
tab_neg_or) We take the following as an axiom:
L528Axiom. (
tab_neg_iff) We take the following as an axiom:
L529Axiom. (
prop_ext_2) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → A = B
L530Axiom. (
eqo_iff) We take the following as an axiom:
∀A B : prop, (A = B) → (A ↔ B)
L531Axiom. (
tab_pos_eqo) We take the following as an axiom:
L532Axiom. (
tab_neg_eqo) We take the following as an axiom:
L535Axiom. (
tab_pos_ex_i) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → (∀y, P y → False) → False
L536Axiom. (
tab_mat_i_o) We take the following as an axiom:
∀P : set → prop, ∀X1 Y1, P X1 → ¬ P Y1 → (¬ (X1 = Y1) → False) → False
L537Axiom. (
tab_mat_i_i_o) We take the following as an axiom:
∀P : set → set → prop, ∀X1 X2 Y1 Y2, P X1 X2 → ¬ P Y1 Y2 → (¬ (X1 = Y1) → False) → (¬ (X2 = Y2) → False) → False
L539Axiom. (
f_equal_i_i) We take the following as an axiom:
∀F : set → set, ∀X1 Y1, X1 = Y1 → F X1 = F Y1
L540Axiom. (
tab_dec_i) We take the following as an axiom:
∀F : set → set, ∀X1 Y1, ¬ (F X1 = F Y1) → (¬ (X1 = Y1) → False) → False
L541Axiom. (
f_equal_i_i_i) We take the following as an axiom:
∀F : set → set → set, ∀X1 Y1 X2 Y2, X1 = Y1 → X2 = Y2 → F X1 X2 = F Y1 Y2
L542Axiom. (
tab_dec_i_i) We take the following as an axiom:
∀F : set → set → set, ∀X1 Y1 X2 Y2, ¬ (F X1 X2 = F Y1 Y2) → (¬ (X1 = Y1) → False) → (¬ (X2 = Y2) → False) → False
L545Axiom. (
andEL) We take the following as an axiom:
L546Axiom. (
andER) We take the following as an axiom:
L547Axiom. (
iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
L548Axiom. (
iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
L549Axiom. (
exandI_i) We take the following as an axiom:
∀P Q : set → prop, ∀x, P x → Q x → (∃x, P x ∧ Q x)
L550Axiom. (
exandE_i) We take the following as an axiom:
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀p : prop, (∀x, P x → Q x → p) → p
L551Axiom. (
SubqI) We take the following as an axiom:
∀A B, (∀x ∈ A, x ∈ B) → Subq A B
L552Axiom. (
SubqE) We take the following as an axiom:
∀A B, Subq A B → (∀x ∈ A, x ∈ B)
L555Axiom. (
TransSetI) We take the following as an axiom:
L556Axiom. (
TransSetE) We take the following as an axiom:
L557Axiom. (
atleast2_I) We take the following as an axiom:
L558Axiom. (
atleast2_E) We take the following as an axiom:
L559Axiom. (
atleast3_I) We take the following as an axiom:
L560Axiom. (
atleast3_E) We take the following as an axiom:
L561Axiom. (
atleast4_I) We take the following as an axiom:
L562Axiom. (
atleast4_E) We take the following as an axiom:
L563Axiom. (
atleast5_I) We take the following as an axiom:
L564Axiom. (
atleast5_E) We take the following as an axiom:
L565Axiom. (
atleast6_I) We take the following as an axiom:
L566Axiom. (
atleast6_E) We take the following as an axiom:
L567Axiom. (
exactly2_I) We take the following as an axiom:
L568Axiom. (
exactly2_E) We take the following as an axiom:
L569Axiom. (
exactly3_I) We take the following as an axiom:
L570Axiom. (
exactly3_E) We take the following as an axiom:
L571Axiom. (
exactly4_I) We take the following as an axiom:
L572Axiom. (
exactly4_E) We take the following as an axiom:
L573Axiom. (
exactly5_I) We take the following as an axiom:
L574Axiom. (
exactly5_E) We take the following as an axiom:
L575Axiom. (
nIn_I) We take the following as an axiom:
L576Axiom. (
nIn_E) We take the following as an axiom:
L577Axiom. (
nIn_I2) We take the following as an axiom:
L578Axiom. (
nIn_E2) We take the following as an axiom:
L579Axiom. (
contra_In) We take the following as an axiom:
L580Axiom. (
neg_nIn) We take the following as an axiom:
L581Axiom. (
nSubq_I) We take the following as an axiom:
L582Axiom. (
nSubq_E) We take the following as an axiom:
L583Axiom. (
nSubq_I2) We take the following as an axiom:
L584Axiom. (
nSubq_E2) We take the following as an axiom:
L585Axiom. (
neg_nSubq) We take the following as an axiom:
L586Axiom. (
contra_Subq) We take the following as an axiom:
L587Axiom. (
Subq_ref) We take the following as an axiom:
L588Axiom. (
Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
L589Axiom. (
Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X
L590Axiom. (
EmptyE) We take the following as an axiom:
L591Axiom. (
nIn_Empty) We take the following as an axiom:
L592Axiom. (
Subq_Empty) We take the following as an axiom:
L594Axiom. (
Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x ∉ X) → X = ∅
L595Axiom. (
UnionE) We take the following as an axiom:
∀X x : set, x ∈ (⋃ X) → ∃Y : set, x ∈ Y ∧ Y ∈ X
L596Axiom. (
UnionE2) We take the following as an axiom:
∀X x : set, x ∈ (⋃ X) → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
L597Axiom. (
UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ (⋃ X)
L600Axiom. (
Union_Empty) We take the following as an axiom:
L601Axiom. (
PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
L602Axiom. (
PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
L607Axiom. (
ReplE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X} → ∃x : set, x ∈ X ∧ y = F x
L608Axiom. (
ReplE2) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X} → ∀p : prop, (∀x : set, x ∈ X → y = F x → p) → p
L609Axiom. (
ReplI) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → F x ∈ {F x|x ∈ X}
L612Axiom. (
Repl_Empty) We take the following as an axiom:
L613Axiom. (
ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}
L614Axiom. (
ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}
L615Axiom. (
set_ext_2) We take the following as an axiom:
∀A B, (∀x, x ∈ A → x ∈ B) → (∀x, x ∈ B → x ∈ A) → A = B
L617Axiom. (
neq_i_sym) We take the following as an axiom:
∀x y, ¬ (x = y) → ¬ (y = x)
L619Axiom. (
tab_Eps_i) We take the following as an axiom:
L620Axiom. (
If_i_0) We take the following as an axiom:
∀p : prop, ∀x y, ¬ p → If_i p x y = y
L621Axiom. (
If_i_1) We take the following as an axiom:
∀p : prop, ∀x y, p → If_i p x y = x
L622Axiom. (
If_i_or) We take the following as an axiom:
Notation.
{x,y} is notation for
UPair x y.
L626Axiom. (
UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
L627Axiom. (
UPairE_cases) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → ∀p : prop, (x = y → p) → (x = z → p) → p
L628Axiom. (
UPairI1) We take the following as an axiom:
L629Axiom. (
UPairI2) We take the following as an axiom:
L630Axiom. (
UPair_com) We take the following as an axiom:
Notation.
{x} is notation for
Sing x.
L634Axiom. (
SingI) We take the following as an axiom:
L635Axiom. (
SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
Notation. We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion.
L640Axiom. (
binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
L641Axiom. (
binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
L642Axiom. (
binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
L643Axiom. (
binunionE_cases) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → p
Notation. We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
∅ is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
L648Axiom. (
Repl_UPair) We take the following as an axiom:
∀F : set → set, ∀x y : set, {F z|z ∈ {x,y}} = {F x,F y}
L649Axiom. (
Repl_Sing) We take the following as an axiom:
∀F : set → set, ∀x : set, {F z|z ∈ {x}} = {F x}
Notation. We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion.
L653Axiom. (
famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
L654Axiom. (
famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
L655Axiom. (
famunionE2) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
Notation.
if cond then T else E is notation corresponding to
If_i type cond T E where
type is the inferred type of
T.
Beginning of Section PropN
L664Variable P1 P2 P3 : prop
L666Axiom. (
and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
L668Axiom. (
and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
L670Axiom. (
or3I1) We take the following as an axiom:
L672Axiom. (
or3I2) We take the following as an axiom:
L674Axiom. (
or3I3) We take the following as an axiom:
L676Axiom. (
or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
L680Axiom. (
and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
L682Axiom. (
and4E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 → (∀p : prop, (P1 → P2 → P3 → P4 → p) → p)
L684Axiom. (
or4I1) We take the following as an axiom:
L686Axiom. (
or4I2) We take the following as an axiom:
L688Axiom. (
or4I3) We take the following as an axiom:
L690Axiom. (
or4I4) We take the following as an axiom:
L692Axiom. (
or4E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 ∨ P4 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → p)
L696Axiom. (
and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
L698Axiom. (
and5E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → p) → p)
L700Axiom. (
or5I1) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L702Axiom. (
or5I2) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L704Axiom. (
or5I3) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L706Axiom. (
or5I4) We take the following as an axiom:
P4 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L708Axiom. (
or5I5) We take the following as an axiom:
P5 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L710Axiom. (
or5E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → (P5 → p) → p)
L714Axiom. (
and6I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
L716Axiom. (
and6E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → p) → p)
L720Axiom. (
and7I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
L722Axiom. (
and7E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → P7 → p) → p)
End of Section PropN
L728Axiom. (
Eps_i_R2) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
L729Axiom. (
xmcases_In) We take the following as an axiom:
∀x X : set, ∀p : prop, (x ∈ X → p) → (x ∉ X → p) → p
L730Axiom. (
SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
L731Axiom. (
SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
L732Axiom. (
SepE_impred) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → ∀q : prop, (x ∈ X → P x → q) → q
L733Axiom. (
SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
L734Axiom. (
SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
L735Axiom. (
Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
L736Axiom. (
Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
L737Axiom. (
tab_pos_Sep) We take the following as an axiom:
L738Axiom. (
tab_neg_Sep) We take the following as an axiom:
L739Axiom. (
ReplSepI) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}
L740Axiom. (
ReplSepE) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∃x : set, x ∈ X ∧ P x ∧ y = F x
L741Axiom. (
ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∀p : prop, (∀x ∈ X, P x → y = F x → p) → p
L742Axiom. (
tab_pos_ReplSep) We take the following as an axiom:
∀X, ∀P : set → prop, ∀F : set → set, ∀y, y ∈ {F x|x ∈ X, P x} → (∀x, x ∈ X → P x → y = F x → False) → False
L744Axiom. (
binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
L745Axiom. (
binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
L753Axiom. (
binunion_nIn_I) We take the following as an axiom:
∀X Y z : set, z ∉ X → z ∉ Y → z ∉ X ∪ Y
L754Axiom. (
binunion_nIn_E) We take the following as an axiom:
∀X Y z : set, z ∉ X ∪ Y → z ∉ X ∧ z ∉ Y
L755Axiom. (
binunion_nIn_E_impred) We take the following as an axiom:
∀X Y z : set, z ∉ X ∪ Y → ∀p : prop, (z ∉ X → z ∉ Y → p) → p
L756Axiom. (
binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
L757Axiom. (
binintersectE) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
L779Axiom. (
setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
L780Axiom. (
setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
L781Axiom. (
setminusE_impred) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → ∀p : prop, (z ∈ X → z ∉ Y → p) → p
L782Axiom. (
setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
L783Axiom. (
setminusE2) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∉ Y
L789Axiom. (
setminus_nIn_E_impred) We take the following as an axiom:
∀X Y z, z ∉ X ∖ Y → ∀p : prop, (z ∉ X → p) → (z ∈ Y → p) → p
L800Axiom. (
eq_sym_i) We take the following as an axiom:
∀x y : set, x = y → y = x
L802Axiom. (
neq_sym_i) We take the following as an axiom:
∀x y : set, x ≠ y → y ≠ x
L803Axiom. (
In_irref) We take the following as an axiom:
L804Axiom. (
In_no2cycle) We take the following as an axiom:
L805Axiom. (
In_no3cycle) We take the following as an axiom:
L806Axiom. (
ordsuccI1) We take the following as an axiom:
L807Axiom. (
ordsuccI1b) We take the following as an axiom:
L808Axiom. (
ordsuccI2) We take the following as an axiom:
L809Axiom. (
ordsuccE) We take the following as an axiom:
L810Axiom. (
ordsuccE_impred) We take the following as an axiom:
∀x y : set, y ∈ ordsucc x → ∀p : prop, (y ∈ x → p) → (y = x → p) → p
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
∅ as 0 and forming successors with
ordsucc.
L814Axiom. (
ordsucc_inj) We take the following as an axiom:
L816Axiom. (
In_0_1) We take the following as an axiom:
L817Axiom. (
In_0_2) We take the following as an axiom:
L818Axiom. (
In_1_2) We take the following as an axiom:
L819Axiom. (
cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
L820Axiom. (
cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
L821Axiom. (
cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
L822Axiom. (
cases_4) We take the following as an axiom:
∀i ∈ 4, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p i
L823Axiom. (
cases_5) We take the following as an axiom:
∀i ∈ 5, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p i
L824Axiom. (
cases_6) We take the following as an axiom:
∀i ∈ 6, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p i
L825Axiom. (
cases_7) We take the following as an axiom:
∀i ∈ 7, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p i
L826Axiom. (
cases_8) We take the following as an axiom:
∀i ∈ 8, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p 7 → p i
L827Axiom. (
cases_9) We take the following as an axiom:
∀i ∈ 9, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p 7 → p 8 → p i
L828Axiom. (
neq_0_1) We take the following as an axiom:
L829Axiom. (
neq_1_0) We take the following as an axiom:
L830Axiom. (
neq_0_2) We take the following as an axiom:
L831Axiom. (
neq_2_0) We take the following as an axiom:
L832Axiom. (
neq_1_2) We take the following as an axiom:
L833Axiom. (
neq_2_1) We take the following as an axiom:
L834Axiom. (
Subq_0_0) We take the following as an axiom:
L835Axiom. (
Subq_0_1) We take the following as an axiom:
L836Axiom. (
Subq_0_2) We take the following as an axiom:
L837Axiom. (
Subq_1_1) We take the following as an axiom:
L838Axiom. (
Subq_1_2) We take the following as an axiom:
L839Axiom. (
Subq_2_2) We take the following as an axiom:
L842Axiom. (
eq_1_Sing0) We take the following as an axiom:
L846Axiom. (
nat_0) We take the following as an axiom:
L847Axiom. (
nat_ordsucc) We take the following as an axiom:
L848Axiom. (
nat_1) We take the following as an axiom:
L849Axiom. (
nat_2) We take the following as an axiom:
L852Axiom. (
nat_ind) We take the following as an axiom:
L853Axiom. (
nat_inv) We take the following as an axiom:
L855Axiom. (
nat_p_trans) We take the following as an axiom:
L856Axiom. (
nat_trans) We take the following as an axiom:
L858Axiom. (
nat_ordinal) We take the following as an axiom:
L861Axiom. (
In_0_3) We take the following as an axiom:
L862Axiom. (
In_1_3) We take the following as an axiom:
L863Axiom. (
In_2_3) We take the following as an axiom:
L864Axiom. (
In_0_4) We take the following as an axiom:
L865Axiom. (
In_1_4) We take the following as an axiom:
L866Axiom. (
In_2_4) We take the following as an axiom:
L867Axiom. (
In_3_4) We take the following as an axiom:
L868Axiom. (
In_0_5) We take the following as an axiom:
L869Axiom. (
In_1_5) We take the following as an axiom:
L870Axiom. (
In_2_5) We take the following as an axiom:
L871Axiom. (
In_3_5) We take the following as an axiom:
L872Axiom. (
In_4_5) We take the following as an axiom:
L873Axiom. (
In_0_6) We take the following as an axiom:
L874Axiom. (
In_1_6) We take the following as an axiom:
L875Axiom. (
In_2_6) We take the following as an axiom:
L876Axiom. (
In_3_6) We take the following as an axiom:
L877Axiom. (
In_4_6) We take the following as an axiom:
L878Axiom. (
In_5_6) We take the following as an axiom:
L879Axiom. (
In_0_7) We take the following as an axiom:
L880Axiom. (
In_1_7) We take the following as an axiom:
L881Axiom. (
In_2_7) We take the following as an axiom:
L882Axiom. (
In_3_7) We take the following as an axiom:
L883Axiom. (
In_4_7) We take the following as an axiom:
L884Axiom. (
In_5_7) We take the following as an axiom:
L885Axiom. (
In_6_7) We take the following as an axiom:
L886Axiom. (
In_0_8) We take the following as an axiom:
L887Axiom. (
In_1_8) We take the following as an axiom:
L888Axiom. (
In_2_8) We take the following as an axiom:
L889Axiom. (
In_3_8) We take the following as an axiom:
L890Axiom. (
In_4_8) We take the following as an axiom:
L891Axiom. (
In_5_8) We take the following as an axiom:
L892Axiom. (
In_6_8) We take the following as an axiom:
L893Axiom. (
In_7_8) We take the following as an axiom:
L894Axiom. (
In_0_9) We take the following as an axiom:
L895Axiom. (
In_1_9) We take the following as an axiom:
L896Axiom. (
In_2_9) We take the following as an axiom:
L897Axiom. (
In_3_9) We take the following as an axiom:
L898Axiom. (
In_4_9) We take the following as an axiom:
L899Axiom. (
In_5_9) We take the following as an axiom:
L900Axiom. (
In_6_9) We take the following as an axiom:
L901Axiom. (
In_7_9) We take the following as an axiom:
L902Axiom. (
In_8_9) We take the following as an axiom:
L903Axiom. (
nIn_0_0) We take the following as an axiom:
L904Axiom. (
nIn_1_0) We take the following as an axiom:
L905Axiom. (
nIn_2_0) We take the following as an axiom:
L906Axiom. (
nIn_1_1) We take the following as an axiom:
L907Axiom. (
nIn_2_1) We take the following as an axiom:
L908Axiom. (
nIn_2_2) We take the following as an axiom:
L909Axiom. (
nSubq_1_0) We take the following as an axiom:
L910Axiom. (
nSubq_2_0) We take the following as an axiom:
L911Axiom. (
nSubq_2_1) We take the following as an axiom:
L912Axiom. (
exandE_ii) We take the following as an axiom:
∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
L918Axiom. (
Regularity) We take the following as an axiom:
∀X x : set, x ∈ X → ∃Y : set, Y ∈ X ∧ ¬ ∃z : set, z ∈ X ∧ z ∈ Y
Beginning of Section EpsilonRec
L920Variable F : set → (set → set) → set
L923Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
L927Axiom. (
In_rec_i_eq) We take the following as an axiom:
End of Section EpsilonRec
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
∅ as 0 and forming successors with
ordsucc.
L930Axiom. (
Inj1_eq) We take the following as an axiom:
L931Axiom. (
Inj1I1) We take the following as an axiom:
L932Axiom. (
Inj1I2) We take the following as an axiom:
L933Axiom. (
Inj1E) We take the following as an axiom:
L934Axiom. (
Inj1E_impred) We take the following as an axiom:
∀X y : set, y ∈ Inj1 X → ∀p : set → prop, p 0 → (∀x ∈ X, p (Inj1 x)) → p y
L935Axiom. (
Inj1NE1) We take the following as an axiom:
L936Axiom. (
Inj1NE2) We take the following as an axiom:
L937Axiom. (
Inj0I) We take the following as an axiom:
L938Axiom. (
Inj0E) We take the following as an axiom:
L939Axiom. (
Inj0E_impred) We take the following as an axiom:
∀X y : set, y ∈ Inj0 X → ∀p : set → prop, (∀x, x ∈ X → p (Inj1 x)) → p y
L940Axiom. (
Unj_eq) We take the following as an axiom:
L941Axiom. (
Unj_Inj1_eq) We take the following as an axiom:
L942Axiom. (
Inj1_inj) We take the following as an axiom:
L943Axiom. (
Unj_Inj0_eq) We take the following as an axiom:
L944Axiom. (
Inj0_inj) We take the following as an axiom:
L945Axiom. (
Inj0_0) We take the following as an axiom:
Notation. We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum.
L949Axiom. (
Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
L950Axiom. (
Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
L954Axiom. (
setsum_mon) We take the following as an axiom:
∀X Y W Z, X ⊆ W → Y ⊆ Z → X + Y ⊆ W + Z
L957Axiom. (
exandE_iii) We take the following as an axiom:
∀P Q : (set → set → set) → prop, (∃x : set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p
L959Axiom. (
exandE_iiii) We take the following as an axiom:
∀P Q : (set → set → set → set) → prop, (∃x : set → set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p
L960Axiom. (
exandE_iio) We take the following as an axiom:
∀P Q : (set → set → prop) → prop, (∃x : set → set → prop, P x ∧ Q x) → ∀p : prop, (∀x : set → set → prop, P x → Q x → p) → p
L961Axiom. (
exandE_iiio) We take the following as an axiom:
∀P Q : (set → set → set → prop) → prop, (∃x : set → set → set → prop, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → prop, P x → Q x → p) → p
Primitive. The name
Descr_ii is a term of type
((set → set) → prop) → (set → set).
L964Axiom. (
Descr_ii_prop) We take the following as an axiom:
∀P : (set → set) → prop, (∃f : set → set, P f) → (∀f g : set → set, P f → P g → f = g) → P (Descr_ii P)
Primitive. The name
Descr_iii is a term of type
((set → set → set) → prop) → (set → set → set).
L967Axiom. (
Descr_iii_prop) We take the following as an axiom:
∀P : (set → set → set) → prop, (∃f : set → set → set, P f) → (∀f g : set → set → set, P f → P g → f = g) → P (Descr_iii P)
Primitive. The name
Descr_iio is a term of type
((set → set → prop) → prop) → (set → set → prop).
L970Axiom. (
Descr_iio_prop) We take the following as an axiom:
∀P : (set → set → prop) → prop, (∃f : set → set → prop, P f) → (∀f g : set → set → prop, P f → P g → f = g) → P (Descr_iio P)
Primitive. The name
Descr_Vo1 is a term of type
(Vo 1 → prop) → Vo 1.
L973Axiom. (
Descr_Vo1_prop) We take the following as an axiom:
∀P : Vo 1 → prop, (∃f : Vo 1, P f) → (∀f g : Vo 1, P f → P g → f = g) → P (Descr_Vo1 P)
Primitive. The name
Descr_Vo2 is a term of type
(Vo 2 → prop) → Vo 2.
L976Axiom. (
Descr_Vo2_prop) We take the following as an axiom:
∀P : Vo 2 → prop, (∃f : Vo 2, P f) → (∀f g : Vo 2, P f → P g → f = g) → P (Descr_Vo2 P)
Primitive. The name
Descr_Vo3 is a term of type
(Vo 3 → prop) → Vo 3.
L979Axiom. (
Descr_Vo3_prop) We take the following as an axiom:
∀P : Vo 3 → prop, (∃f : Vo 3, P f) → (∀f g : Vo 3, P f → P g → f = g) → P (Descr_Vo3 P)
Primitive. The name
Descr_Vo4 is a term of type
(Vo 4 → prop) → Vo 4.
L982Axiom. (
Descr_Vo4_prop) We take the following as an axiom:
∀P : Vo 4 → prop, (∃f : Vo 4, P f) → (∀f g : Vo 4, P f → P g → f = g) → P (Descr_Vo4 P)
Primitive. The name
If_ii is a term of type
prop → (set → set) → (set → set) → (set → set).
L991Axiom. (
If_ii_1) We take the following as an axiom:
∀p : prop, ∀x y : (set → set), p → If_ii p x y = x
L992Axiom. (
If_ii_0) We take the following as an axiom:
∀p : prop, ∀x y : (set → set), ¬ p → If_ii p x y = y
Primitive. The name
If_iii is a term of type
prop → (set → set → set) → (set → set → set) → (set → set → set).
L994Axiom. (
If_iii_1) We take the following as an axiom:
∀p : prop, ∀x y : (set → set → set), p → If_iii p x y = x
L995Axiom. (
If_iii_0) We take the following as an axiom:
∀p : prop, ∀x y : (set → set → set), ¬ p → If_iii p x y = y
Primitive. The name
If_iio is a term of type
prop → (set → set → prop) → (set → set → prop) → (set → set → prop).
L997Axiom. (
If_iio_1) We take the following as an axiom:
∀p : prop, ∀x y : (set → set → prop), p → If_iio p x y = x
L998Axiom. (
If_iio_0) We take the following as an axiom:
∀p : prop, ∀x y : (set → set → prop), ¬ p → If_iio p x y = y
Primitive. The name
If_Vo1 is a term of type
prop → Vo 1 → Vo 1 → Vo 1.
L1000Axiom. (
If_Vo1_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 1, p → If_Vo1 p x y = x
L1001Axiom. (
If_Vo1_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 1, ¬ p → If_Vo1 p x y = y
Primitive. The name
If_Vo2 is a term of type
prop → Vo 2 → Vo 2 → Vo 2.
L1003Axiom. (
If_Vo2_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 2, p → If_Vo2 p x y = x
L1004Axiom. (
If_Vo2_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 2, ¬ p → If_Vo2 p x y = y
Primitive. The name
If_Vo3 is a term of type
prop → Vo 3 → Vo 3 → Vo 3.
L1006Axiom. (
If_Vo3_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 3, p → If_Vo3 p x y = x
L1007Axiom. (
If_Vo3_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 3, ¬ p → If_Vo3 p x y = y
Primitive. The name
If_Vo4 is a term of type
prop → Vo 4 → Vo 4 → Vo 4.
L1009Axiom. (
If_Vo4_1) We take the following as an axiom:
∀p : prop, ∀x y : Vo 4, p → If_Vo4 p x y = x
L1010Axiom. (
If_Vo4_0) We take the following as an axiom:
∀p : prop, ∀x y : Vo 4, ¬ p → If_Vo4 p x y = y
Primitive. The name
In_rec_ii is a term of type
(set → (set → (set → set)) → (set → set)) → set → (set → set).
L1019Axiom. (
In_rec_ii_eq) We take the following as an axiom:
∀F : set → (set → (set → set)) → (set → set), (∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_ii F X = F X (In_rec_ii F)
Primitive. The name
In_rec_iii is a term of type
(set → (set → (set → set → set)) → (set → set → set)) → set → (set → set → set).
L1021Axiom. (
In_rec_iii_eq) We take the following as an axiom:
∀F : set → (set → (set → set → set)) → (set → set → set), (∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_iii F X = F X (In_rec_iii F)
Primitive. The name
In_rec_iio is a term of type
(set → (set → (set → set → prop)) → (set → set → prop)) → set → (set → set → prop).
L1023Axiom. (
In_rec_iio_eq) We take the following as an axiom:
∀F : set → (set → (set → set → prop)) → (set → set → prop), (∀X : set, ∀g h : set → (set → set → prop), (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_iio F X = F X (In_rec_iio F)
Primitive. The name
In_rec_Vo1 is a term of type
(set → (set → Vo 1) → Vo 1) → set → Vo 1.
L1025Axiom. (
In_rec_Vo1_eq) We take the following as an axiom:
∀F : set → (set → Vo 1) → Vo 1, (∀X : set, ∀g h : set → Vo 1, (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_Vo1 F X = F X (In_rec_Vo1 F)
Primitive. The name
In_rec_Vo2 is a term of type
(set → (set → Vo 2) → Vo 2) → set → Vo 2.
L1027Axiom. (
In_rec_Vo2_eq) We take the following as an axiom:
∀F : set → (set → Vo 2) → Vo 2, (∀X : set, ∀g h : set → Vo 2, (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_Vo2 F X = F X (In_rec_Vo2 F)
Primitive. The name
In_rec_Vo3 is a term of type
(set → (set → Vo 3) → Vo 3) → set → Vo 3.
L1029Axiom. (
In_rec_Vo3_eq) We take the following as an axiom:
∀F : set → (set → Vo 3) → Vo 3, (∀X : set, ∀g h : set → Vo 3, (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_Vo3 F X = F X (In_rec_Vo3 F)
Primitive. The name
In_rec_Vo4 is a term of type
(set → (set → Vo 4) → Vo 4) → set → Vo 4.
L1031Axiom. (
In_rec_Vo4_eq) We take the following as an axiom:
∀F : set → (set → Vo 4) → Vo 4, (∀X : set, ∀g h : set → Vo 4, (∀x ∈ X, g x = h x) → F X g = F X h) → ∀X : set, In_rec_Vo4 F X = F X (In_rec_Vo4 F)
L1032Definition. We define
incl_0_1 to be
λx ⇒ λy ⇒ y ∈ x of type
Vo 0 → Vo 1.
L1033Definition. We define
In_1 to be
λX Y ⇒ ∃x : Vo 0, X = incl_0_1 x ∧ Y x of type
Vo 1 → Vo 1 → prop.
L1034Definition. We define
incl_1_2 to be
λX ⇒ λY ⇒ In_1 Y X of type
Vo 1 → Vo 2.
L1035Definition. We define
In_2 to be
λX Y ⇒ ∃x : Vo 1, X = incl_1_2 x ∧ Y x of type
Vo 2 → Vo 2 → prop.
L1036Definition. We define
incl_2_3 to be
λX ⇒ λY ⇒ In_2 Y X of type
Vo 2 → Vo 3.
L1037Definition. We define
In_3 to be
λX Y ⇒ ∃x : Vo 2, X = incl_2_3 x ∧ Y x of type
Vo 3 → Vo 3 → prop.
L1038Definition. We define
incl_3_4 to be
λX ⇒ λY ⇒ In_3 Y X of type
Vo 3 → Vo 4.
L1039Definition. We define
In_4 to be
λX Y ⇒ ∃x : Vo 3, X = incl_3_4 x ∧ Y x of type
Vo 4 → Vo 4 → prop.
L1040Axiom. (
In_1_I) We take the following as an axiom:
L1041Axiom. (
In_1_E) We take the following as an axiom:
∀X Y : Vo 1, In_1 X Y → ∀p : Vo 1 → prop, (∀x, Y x → p (incl_0_1 x)) → p X
L1043Axiom. (
In_1_up) We take the following as an axiom:
L1044Axiom. (
In_1_down) We take the following as an axiom:
L1045Axiom. (
In_2_I) We take the following as an axiom:
L1046Axiom. (
In_2_E) We take the following as an axiom:
∀X Y : Vo 2, In_2 X Y → ∀p : Vo 2 → prop, (∀x : Vo 1, Y x → p (incl_1_2 x)) → p X
L1048Axiom. (
In_2_up) We take the following as an axiom:
L1049Axiom. (
In_2_down) We take the following as an axiom:
L1050Axiom. (
In_3_I) We take the following as an axiom:
L1051Axiom. (
In_3_E) We take the following as an axiom:
∀X Y : Vo 3, In_3 X Y → ∀p : Vo 3 → prop, (∀x : Vo 2, Y x → p (incl_2_3 x)) → p X
L1053Axiom. (
In_3_up) We take the following as an axiom:
L1054Axiom. (
In_3_down) We take the following as an axiom:
L1055Axiom. (
In_4_I) We take the following as an axiom:
L1056Axiom. (
In_4_E) We take the following as an axiom:
∀X Y : Vo 4, In_4 X Y → ∀p : Vo 4 → prop, (∀x : Vo 3, Y x → p (incl_3_4 x)) → p X
L1058Axiom. (
In_4_up) We take the following as an axiom:
L1059Axiom. (
In_4_down) We take the following as an axiom:
L1060Axiom. (
PowerI2) We take the following as an axiom:
∀X Y, (∀y ∈ Y, y ∈ X) → Y ∈ 𝒫 X
L1062Axiom. (
PowerE2) We take the following as an axiom:
∀X Y, Y ∈ 𝒫 X → ∀y ∈ Y, y ∈ X
L1065Axiom. (
setsum_0_0) We take the following as an axiom:
L1068Let pair : set → set → set ≝ setsum
L1069Axiom. (
pair_0_0) We take the following as an axiom:
L1070Axiom. (
pair_1_0_1) We take the following as an axiom:
L1071Axiom. (
pair_1_1_2) We take the following as an axiom:
L1075Axiom. (
pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
L1076Axiom. (
pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
L1077Axiom. (
pairE) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
L1078Axiom. (
pairE_impred) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → ∀p : set → prop, (∀x ∈ X, p (pair 0 x)) → (∀y ∈ Y, p (pair 1 y)) → p z
L1079Axiom. (
pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
L1080Axiom. (
pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
L1081Axiom. (
pairEq) We take the following as an axiom:
∀X Y z, z ∈ pair X Y ↔ (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
L1082Axiom. (
pairSubq) We take the following as an axiom:
∀X Y W Z, X ⊆ W → Y ⊆ Z → pair X Y ⊆ pair W Z
L1083Axiom. (
proj0I) We take the following as an axiom:
L1084Axiom. (
proj0E) We take the following as an axiom:
L1085Axiom. (
proj1I) We take the following as an axiom:
L1086Axiom. (
proj1E) We take the following as an axiom:
L1089Axiom. (
pair_inj) We take the following as an axiom:
∀x y w z : set, pair x y = pair w z → x = w ∧ y = z
L1091Let Sigma : set → (set → set) → set ≝ lam
Notation. We use
∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma.
L1095Axiom. (
pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x
L1098Axiom. (
proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X
L1099Axiom. (
proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)
L1100Axiom. (
pair_Sigma_E0) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → x ∈ X
L1101Axiom. (
pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x
L1102Axiom. (
Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y
L1103Axiom. (
Sigma_Eq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) ↔ ∃x ∈ X, ∃y ∈ Y x, z = pair x y
L1104Axiom. (
Sigma_mon) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z W : set → set, (∀x ∈ X, Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑y ∈ Y, W y
L1105Axiom. (
Sigma_mon0) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z : set → set, (∑x ∈ X, Z x) ⊆ ∑y ∈ Y, Z y
L1106Axiom. (
Sigma_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set → set, (∀x, x ∈ X → Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑x ∈ X, W x
L1107Axiom. (
Sigma_Power_1) We take the following as an axiom:
∀X : set, X ∈ 𝒫 1 → ∀Y : set → set, (∀x ∈ X, Y x ∈ 𝒫 1) → (∑x ∈ X, Y x) ∈ 𝒫 1
Notation. We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod.
L1110Axiom. (
pair_setprod) We take the following as an axiom:
∀X Y : set, ∀(x ∈ X)(y ∈ Y), pair x y ∈ X ⨯ Y
L1113Axiom. (
setprod_mon) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ Y ⨯ W
L1114Axiom. (
setprod_mon0) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z : set, X ⨯ Z ⊆ Y ⨯ Z
L1115Axiom. (
setprod_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ X ⨯ W
L1116Axiom. (
pair_setprod_E0) We take the following as an axiom:
∀X Y x y : set, pair x y ∈ X ⨯ Y → x ∈ X
L1117Axiom. (
pair_setprod_E1) We take the following as an axiom:
∀X Y x y : set, pair x y ∈ X ⨯ Y → y ∈ Y
Notation. When
x is a set, a term
x y is notation for
ap x y.
Notation.
λ x ∈ A ⇒ B is notation for the set
lam A (λ x : set ⇒ B).
Notation. We now use n-tuple notation (
a0,...,
an-1) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1.
L1120Axiom. (
lamI) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x
L1121Axiom. (
lamE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y
L1122Axiom. (
lamEq) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z, z ∈ (λx ∈ X ⇒ F x) ↔ ∃x ∈ X, ∃y ∈ F x, z = pair x y
L1123Axiom. (
apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
L1124Axiom. (
apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
L1125Axiom. (
apEq) We take the following as an axiom:
∀f x y, y ∈ f x ↔ pair x y ∈ f
L1126Axiom. (
beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
L1127Axiom. (
beta0) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∉ X → (λx ∈ X ⇒ F x) x = 0
L1128Axiom. (
neq_3_0) We take the following as an axiom:
L1130Axiom. (
neq_3_1) We take the following as an axiom:
L1131Axiom. (
neq_3_2) We take the following as an axiom:
L1132Axiom. (
neq_4_0) We take the following as an axiom:
L1133Axiom. (
neq_4_1) We take the following as an axiom:
L1134Axiom. (
neq_4_2) We take the following as an axiom:
L1135Axiom. (
neq_4_3) We take the following as an axiom:
L1136Axiom. (
neq_5_0) We take the following as an axiom:
L1137Axiom. (
neq_5_1) We take the following as an axiom:
L1138Axiom. (
neq_5_2) We take the following as an axiom:
L1139Axiom. (
neq_5_3) We take the following as an axiom:
L1140Axiom. (
neq_5_4) We take the following as an axiom:
L1141Axiom. (
neq_6_0) We take the following as an axiom:
L1142Axiom. (
neq_6_1) We take the following as an axiom:
L1143Axiom. (
neq_6_2) We take the following as an axiom:
L1144Axiom. (
neq_6_3) We take the following as an axiom:
L1145Axiom. (
neq_6_4) We take the following as an axiom:
L1146Axiom. (
neq_6_5) We take the following as an axiom:
L1147Axiom. (
neq_7_0) We take the following as an axiom:
L1148Axiom. (
neq_7_1) We take the following as an axiom:
L1149Axiom. (
neq_7_2) We take the following as an axiom:
L1150Axiom. (
neq_7_3) We take the following as an axiom:
L1151Axiom. (
neq_7_4) We take the following as an axiom:
L1152Axiom. (
neq_7_5) We take the following as an axiom:
L1153Axiom. (
neq_7_6) We take the following as an axiom:
L1154Axiom. (
neq_8_0) We take the following as an axiom:
L1155Axiom. (
neq_8_1) We take the following as an axiom:
L1156Axiom. (
neq_8_2) We take the following as an axiom:
L1157Axiom. (
neq_8_3) We take the following as an axiom:
L1158Axiom. (
neq_8_4) We take the following as an axiom:
L1159Axiom. (
neq_8_5) We take the following as an axiom:
L1160Axiom. (
neq_8_6) We take the following as an axiom:
L1161Axiom. (
neq_8_7) We take the following as an axiom:
L1162Axiom. (
neq_9_0) We take the following as an axiom:
L1163Axiom. (
neq_9_1) We take the following as an axiom:
L1164Axiom. (
neq_9_2) We take the following as an axiom:
L1165Axiom. (
neq_9_3) We take the following as an axiom:
L1166Axiom. (
neq_9_4) We take the following as an axiom:
L1167Axiom. (
neq_9_5) We take the following as an axiom:
L1168Axiom. (
neq_9_6) We take the following as an axiom:
L1169Axiom. (
neq_9_7) We take the following as an axiom:
L1170Axiom. (
neq_9_8) We take the following as an axiom:
L1171Axiom. (
TransSetIb) We take the following as an axiom:
L1172Axiom. (
TransSetEb) We take the following as an axiom:
L1179Axiom. (
ordinal_ind) We take the following as an axiom:
∀p : set → prop, (∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha) → ∀alpha, ordinal alpha → p alpha
L1187Axiom. (
ordinal_1) We take the following as an axiom:
L1188Axiom. (
ordinal_2) We take the following as an axiom:
L1209Axiom. (
ordinal_Sep) We take the following as an axiom:
L1215Definition. We define
AC_1 to be
∃C : (Vo 1 → prop) → Vo 1, ∀P : Vo 1 → prop, ∀x : Vo 1, P x → P (C P) of type
prop.
L1217Definition. We define
AC_2 to be
∃C : (Vo 2 → prop) → Vo 2, ∀P : Vo 2 → prop, ∀x : Vo 2, P x → P (C P) of type
prop.
L1218Definition. We define
AC_3 to be
∃C : (Vo 3 → prop) → Vo 3, ∀P : Vo 3 → prop, ∀x : Vo 3, P x → P (C P) of type
prop.
L1226Axiom. (
Skolem_0) We take the following as an axiom:
∀r : set → set → prop, (∀x, ∃y, r x y) → ∃f : set → set, ∀x, r x (f x)
L1227Axiom. (
Skolem_0_bdd) We take the following as an axiom:
∀X : set, ∀r : set → set → prop, (∀x ∈ X, ∃y, r x y) → ∃f : set → set, ∀x ∈ X, r x (f x)
L1228Axiom. (
Skolem_1) We take the following as an axiom:
AC_1 → ∀r : Vo 1 → Vo 1 → prop, (∀x : Vo 1, ∃y : Vo 1, r x y) → ∃f : Vo 1 → Vo 1, ∀x : Vo 1, r x (f x)
L1229Axiom. (
Skolem_1_bdd) We take the following as an axiom:
AC_1 → ∀X : Vo 1, ∀r : Vo 1 → Vo 1 → prop, (∀x : Vo 1, In_1 x X → ∃y : Vo 1, r x y) → ∃f : Vo 1 → Vo 1, ∀x : Vo 1, In_1 x X → r x (f x)
L1230Axiom. (
Skolem_2) We take the following as an axiom:
AC_2 → ∀r : Vo 2 → Vo 2 → prop, (∀x : Vo 2, ∃y : Vo 2, r x y) → ∃f : Vo 2 → Vo 2, ∀x : Vo 2, r x (f x)
L1231Axiom. (
Skolem_2_bdd) We take the following as an axiom:
AC_2 → ∀X : Vo 2, ∀r : Vo 2 → Vo 2 → prop, (∀x : Vo 2, In_2 x X → ∃y : Vo 2, r x y) → ∃f : Vo 2 → Vo 2, ∀x : Vo 2, In_2 x X → r x (f x)
L1232Axiom. (
Skolem_3) We take the following as an axiom:
AC_3 → ∀r : Vo 3 → Vo 3 → prop, (∀x : Vo 3, ∃y : Vo 3, r x y) → ∃f : Vo 3 → Vo 3, ∀x : Vo 3, r x (f x)
L1233Axiom. (
Skolem_3_bdd) We take the following as an axiom:
AC_3 → ∀X : Vo 3, ∀r : Vo 3 → Vo 3 → prop, (∀x : Vo 3, In_3 x X → ∃y : Vo 3, r x y) → ∃f : Vo 3 → Vo 3, ∀x : Vo 3, In_3 x X → r x (f x)
L1234Axiom. (
proj0_ap_0) We take the following as an axiom:
L1236Axiom. (
proj1_ap_1) We take the following as an axiom:
L1237Axiom. (
pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
L1238Axiom. (
pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
L1239Axiom. (
pair_ap_n2) We take the following as an axiom:
∀x y i : set, i ∉ 2 → (pair x y) i = 0
L1241Axiom. (
ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
L1242Axiom. (
ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
L1243Axiom. (
Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (z 0) (z 1) = z
L1244Axiom. (
ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}
L1245Axiom. (
setsum_p_E) We take the following as an axiom:
L1246Axiom. (
setsum_p_I) We take the following as an axiom:
L1247Axiom. (
setsum_p_I2) We take the following as an axiom:
L1249Axiom. (
pred_ext_i) We take the following as an axiom:
∀p q : set → prop, (∀x, p x → q x) → (∀x, q x → p x) → p = q
L1254Axiom. (
tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
Notation. We use
∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi.
L1257Axiom. (
PiI) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, setsum_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x
L1259Axiom. (
PiE_impred) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → ∀p : prop, ((∀u ∈ f, setsum_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → p) → p
L1261Axiom. (
PiE) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (∀u ∈ f, setsum_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)
L1263Axiom. (
PiEq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ Pi X Y ↔ (∀u ∈ f, setsum_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)
L1265Axiom. (
lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)
L1267Axiom. (
ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
L1268Axiom. (
Pi_ext_Subq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x ⊆ g x) → f ⊆ g
L1269Axiom. (
Pi_ext) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x = g x) → f = g
L1270Axiom. (
Pi_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (λx ∈ X ⇒ f x) = f
L1271Axiom. (
Pi_Power_1) We take the following as an axiom:
∀X : set, ∀Y : set → set, (∀x ∈ X, Y x ∈ 𝒫 1) → (∏x ∈ X, Y x) ∈ 𝒫 1
L1272Axiom. (
Pi_0_dom_mon) We take the following as an axiom:
∀X Y : set, ∀A : set → set, X ⊆ Y → (∀y ∈ Y, y ∉ X → 0 ∈ A y) → (∏x ∈ X, A x) ⊆ ∏y ∈ Y, A y
L1274Axiom. (
Pi_cod_mon) We take the following as an axiom:
∀X : set, ∀A B : set → set, (∀x ∈ X, A x ⊆ B x) → (∏x ∈ X, A x) ⊆ ∏x ∈ X, B x
L1275Axiom. (
Pi_0_mon) We take the following as an axiom:
∀X Y : set, ∀A B : set → set, (∀x ∈ X, A x ⊆ B x) → X ⊆ Y → (∀y ∈ Y, y ∉ X → 0 ∈ B y) → (∏x ∈ X, A x) ⊆ ∏y ∈ Y, B y
Notation. We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp.
L1280Axiom. (
setexp_2_eq) We take the following as an axiom:
L1281Axiom. (
setexp_0_dom_mon) We take the following as an axiom:
∀A : set, 0 ∈ A → ∀X Y : set, X ⊆ Y → AX ⊆ AY
L1282Axiom. (
setexp_0_mon) We take the following as an axiom:
∀X Y A B : set, 0 ∈ B → A ⊆ B → X ⊆ Y → AX ⊆ BY
Beginning of Section Tuples
L1285Variable x0 x1 : set
End of Section Tuples
L1294Axiom. (
tupleI0) We take the following as an axiom:
L1295Axiom. (
tupleI1) We take the following as an axiom:
L1296Axiom. (
tupleE) We take the following as an axiom:
L1297Axiom. (
tuple_2_inj) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z) → x = w ∧ y = z
L1298Axiom. (
tuple_2_inj_impred) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z) → ∀p : prop, (x = w → y = z → p) → p
L1299Axiom. (
tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x
L1300Axiom. (
tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
L1301Axiom. (
tuple_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), (z 0,z 1) = z
L1302Axiom. (
lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
L1303Axiom. (
lamE2) We take the following as an axiom:
∀X, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = (x,y)
L1304Axiom. (
lamE_impred) We take the following as an axiom:
∀X, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∀p : set → prop, (∀x ∈ X, ∀y ∈ F x, p (pair x y)) → p z
L1305Axiom. (
lamE2_impred) We take the following as an axiom:
∀X, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∀p : set → prop, (∀x ∈ X, ∀y ∈ F x, p (x,y)) → p z
L1306Axiom. (
apI2) We take the following as an axiom:
∀f x y, (x,y) ∈ f → y ∈ f x
L1307Axiom. (
apE2) We take the following as an axiom:
∀f x y, y ∈ f x → (x,y) ∈ f
L1308Axiom. (
ap_const_0) We take the following as an axiom:
L1309Axiom. (
lam_ext_sub) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) ⊆ (λx ∈ X ⇒ G x)
L1310Axiom. (
lam_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) = (λx ∈ X ⇒ G x)
L1311Axiom. (
lam_eta) We take the following as an axiom:
∀X, ∀F : set → set, (λx ∈ X ⇒ (λx ∈ X ⇒ F x) x) = (λx ∈ X ⇒ F x)
L1312Axiom. (
tuple_2_eta) We take the following as an axiom:
L1313Axiom. (
tuple_3_eta) We take the following as an axiom:
L1314Axiom. (
tuple_4_eta) We take the following as an axiom:
∀x y z w, (λi ∈ 4 ⇒ (x,y,z,w) i) = (x,y,z,w)
L1315Axiom. (
Sep2I) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x ∈ X, ∀y ∈ Y x, R x y → (x,y) ∈ Sep2 X Y R
L1317Axiom. (
Sep2E_impred) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀u ∈ Sep2 X Y R, ∀p : set → prop, (∀x ∈ X, ∀y ∈ Y x, R x y → p (x,y)) → p u
L1319Axiom. (
Sep2E) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀u ∈ Sep2 X Y R, ∃x ∈ X, ∃y ∈ Y x, u = (x,y) ∧ R x y
L1321Axiom. (
Sep2E'_impred) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → ∀p : prop, (x ∈ X → y ∈ Y x → R x y → p) → p
L1323Axiom. (
Sep2E'1) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → x ∈ X
L1325Axiom. (
Sep2E'2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → y ∈ Y x
L1327Axiom. (
Sep2E'3) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → R x y
L1335Axiom. (
Sep2_ext) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R R' : set → set → prop, (∀x ∈ X, ∀y ∈ Y x, R x y ↔ R' x y) → Sep2 X Y R = Sep2 X Y R'
L1338Axiom. (
beta2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀x ∈ X, ∀y ∈ Y x, lam2 X Y F x y = F x y
L1339Axiom. (
lam2_ext) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y x, F x y = G x y) → lam2 X Y F = lam2 X Y G
L1343Axiom. (
tuple_3_in_A_3) We take the following as an axiom:
∀x y z A, x ∈ A → y ∈ A → z ∈ A → (x,y,z) ∈ A3
L1344Axiom. (
injI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀x ∈ X, f x ∈ Y) → (∀x z ∈ X, f x = f z → x = z) → inj X Y f
L1345Axiom. (
injE_impred) We take the following as an axiom:
∀X Y, ∀f : set → set, inj X Y f → ∀p : prop, ((∀x ∈ X, f x ∈ Y) → (∀x z ∈ X, f x = f z → x = z) → p) → p
L1346Axiom. (
bijI) We take the following as an axiom:
∀X Y, ∀f : set → set, inj X Y f → (∀y ∈ Y, ∃x ∈ X, f x = y) → bij X Y f
L1347Axiom. (
bijE_impred) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, (inj X Y f → (∀y ∈ Y, ∃x ∈ X, f x = y) → p) → p
L1352Axiom. (
In_irref_b) We take the following as an axiom:
L1354Axiom. (
neq_i_E) We take the following as an axiom:
∀x y, x ≠ y → x = y → ∀p : prop, p
L1355Axiom. (
neq_i_sym_E) We take the following as an axiom:
∀x y, x ≠ y → y = x → ∀p : prop, p
Beginning of Section Tuples
L1357Variable x0 x1 x2 x3 : set
L1369Axiom. (
tuple_6_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 0 = x0
L1370Axiom. (
tuple_6_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 1 = x1
L1371Axiom. (
tuple_6_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 2 = x2
L1372Axiom. (
tuple_6_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 3 = x3
L1373Axiom. (
tuple_6_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 4 = x4
L1374Axiom. (
tuple_6_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 5 = x5
L1376Axiom. (
tuple_7_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 0 = x0
L1377Axiom. (
tuple_7_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 1 = x1
L1378Axiom. (
tuple_7_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 2 = x2
L1379Axiom. (
tuple_7_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 3 = x3
L1380Axiom. (
tuple_7_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 4 = x4
L1381Axiom. (
tuple_7_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 5 = x5
L1382Axiom. (
tuple_7_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 6 = x6
L1384Axiom. (
tuple_8_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 0 = x0
L1385Axiom. (
tuple_8_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 1 = x1
L1386Axiom. (
tuple_8_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 2 = x2
L1387Axiom. (
tuple_8_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 3 = x3
L1388Axiom. (
tuple_8_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 4 = x4
L1389Axiom. (
tuple_8_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 5 = x5
L1390Axiom. (
tuple_8_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 6 = x6
L1391Axiom. (
tuple_8_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 7 = x7
L1393Axiom. (
tuple_9_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 0 = x0
L1394Axiom. (
tuple_9_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 1 = x1
L1395Axiom. (
tuple_9_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 2 = x2
L1396Axiom. (
tuple_9_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 3 = x3
L1397Axiom. (
tuple_9_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 4 = x4
L1398Axiom. (
tuple_9_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 5 = x5
L1399Axiom. (
tuple_9_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 6 = x6
L1400Axiom. (
tuple_9_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 7 = x7
L1401Axiom. (
tuple_9_8_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 8 = x8
End of Section Tuples
L1403Axiom. (
tuple_4_in_A_4) We take the following as an axiom:
∀x y z w A, x ∈ A → y ∈ A → z ∈ A → w ∈ A → (x,y,z,w) ∈ A4
L1404Axiom. (
tuple_4_bij_4) We take the following as an axiom:
∀x y z w, x ∈ 4 → y ∈ 4 → z ∈ 4 → w ∈ 4 → x ≠ y → x ≠ z → x ≠ w → y ≠ z → y ≠ w → z ≠ w → bij 4 4 (λi ⇒ (x,y,z,w) i)
L1405Axiom. (
V_eq) We take the following as an axiom:
L1406Axiom. (
V_I) We take the following as an axiom:
∀y x X : set, x ∈ X → y ⊆ V_ x → y ∈ V_ X
L1407Axiom. (
V_E) We take the following as an axiom:
∀y X : set, y ∈ V_ X → ∀p : prop, (∀x ∈ X, y ⊆ V_ x → p) → p
L1408Axiom. (
V_Subq) We take the following as an axiom:
L1409Axiom. (
V_Subq_2) We take the following as an axiom:
L1410Axiom. (
V_In) We take the following as an axiom:
L1413Axiom. (
iff_refl) We take the following as an axiom:
L1414Axiom. (
iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
L1415Axiom. (
iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
L1416Axiom. (
PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
L1417Axiom. (
PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
L1418Axiom. (
PNoEq_tra_) We take the following as an axiom:
L1420Axiom. (
PNoLt_E_) We take the following as an axiom:
L1422Axiom. (
PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
L1424Axiom. (
PNoLt_mon_) We take the following as an axiom:
L1431Axiom. (
PNoLt_tra_) We take the following as an axiom:
L1432Axiom. (
PNoLtI1) We take the following as an axiom:
L1434Axiom. (
PNoLtI2) We take the following as an axiom:
L1436Axiom. (
PNoLtI3) We take the following as an axiom:
L1438Axiom. (
PNoLtE) We take the following as an axiom:
L1445Axiom. (
PNoLtE2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoLt alpha p alpha q → PNoLt_ alpha p q
L1447Axiom. (
PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
L1452Axiom. (
PNoLtEq_tra) We take the following as an axiom:
L1453Axiom. (
PNoEqLt_tra) We take the following as an axiom:
L1454Axiom. (
PNoLt_tra) We take the following as an axiom:
L1455Axiom. (
PNoLeI1) We take the following as an axiom:
L1457Axiom. (
PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
L1459Axiom. (
PNoLeE) We take the following as an axiom:
L1462Axiom. (
PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
L1466Axiom. (
PNoLtLe_tra) We take the following as an axiom:
L1467Axiom. (
PNoLeLt_tra) We take the following as an axiom:
L1468Axiom. (
PNoEqLe_tra) We take the following as an axiom:
L1469Axiom. (
PNoLeEq_tra) We take the following as an axiom:
L1470Axiom. (
PNoLe_tra) We take the following as an axiom:
L1471Axiom. (
exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p
L1477Axiom. (
exactly1of3_E) We take the following as an axiom:
∀A B C : prop, exactly1of3 A B C → ∀p : prop, (A → ¬ B → ¬ C → p) → (¬ A → B → ¬ C → p) → (¬ A → ¬ B → C → p) → p
L1483Axiom. (
exu_i_E1) We take the following as an axiom:
∀P : set → prop, (exu_i P) → ∃x, P x
L1484Axiom. (
exu_i_E2) We take the following as an axiom:
∀P : set → prop, (exu_i P) → ∀x y, P x → P y → x = y
L1485Axiom. (
exu_i_I) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → (∀x y, P x → P y → x = y) → exu_i P
L1486Axiom. (
atleastp_I) We take the following as an axiom:
L1489Axiom. (
ordinalI) We take the following as an axiom:
L1498Axiom. (
transitive_i_I) We take the following as an axiom:
∀R : set → set → prop, (∀x y z, R x y → R y z → R x z) → transitive_i R
L1500Axiom. (
eqreln_i_I) We take the following as an axiom:
L1501Axiom. (
eqreln_i_E) We take the following as an axiom:
L1502Axiom. (
per_i_I) We take the following as an axiom:
L1503Axiom. (
per_i_E) We take the following as an axiom:
L1504Axiom. (
linear_i_I) We take the following as an axiom:
∀R : set → set → prop, (∀x y, R x y ∨ R y x) → linear_i R
L1505Axiom. (
linear_i_E) We take the following as an axiom:
∀R : set → set → prop, linear_i R → ∀x y, R x y ∨ R y x
L1516Axiom. (
binrep_I1) We take the following as an axiom:
L1517Axiom. (
binrep_I2) We take the following as an axiom:
L1518Axiom. (
binrep_E) We take the following as an axiom:
∀X Y, ∀z ∈ binrep X Y, ∀p : set → prop, (∀x ∈ X, p (Inj0 x)) → (∀Z, Z ⊆ Y → p (Inj1 Z)) → p z
L1524Axiom. (
equip_mod_E) We take the following as an axiom:
L1528Axiom. (
tuple_p_I) We take the following as an axiom:
L1529Axiom. (
tuple_p_E) We take the following as an axiom:
L1530Axiom. (
setexp_I) We take the following as an axiom:
∀X Y, ∀f ∈ (∏x ∈ X, Y), f ∈ YX
L1531Axiom. (
setexp_E) We take the following as an axiom:
∀X Y, ∀f ∈ YX, f ∈ ∏x ∈ X, Y
L1532Axiom. (
lam2_I) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀x ∈ X, ∀y ∈ Y x, ∀z ∈ F x y, x + (y + z) ∈ lam2 X Y F
L1535Axiom. (
lam2_E) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀w ∈ lam2 X Y F, ∃x ∈ X, ∃y ∈ Y x, ∃z ∈ F x y, w = x + (y + z)
L1539Axiom. (
lam2_E_impred) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀w ∈ lam2 X Y F, ∀p : set → prop, (∀x ∈ X, ∀y ∈ Y x, ∀z ∈ F x y, p (x + (y + z))) → p w
L1544Axiom. (
lam2_I2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀x ∈ X, ∀y ∈ Y x, ∀z ∈ F x y, (x,(y,z)) ∈ lam2 X Y F
L1547Axiom. (
lam2_E2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀w ∈ lam2 X Y F, ∃x ∈ X, ∃y ∈ Y x, ∃z ∈ F x y, w = (x,(y,z))
L1551Axiom. (
lam2_E2_impred) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀w ∈ lam2 X Y F, ∀p : set → prop, (∀x ∈ X, ∀y ∈ Y x, ∀z ∈ F x y, p (x,(y,z))) → p w
L1556Axiom. (
binop_on_I) We take the following as an axiom:
∀X, ∀f : set → set → set, (∀x y ∈ X, f x y ∈ X) → binop_on X f
L1557Axiom. (
binop_on_E) We take the following as an axiom:
∀X, ∀f : set → set → set, binop_on X f → ∀x y ∈ X, f x y ∈ X
Beginning of Section NatRec
L1562Variable f : set → set → set
L1563Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
L1564Axiom. (
nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section NatRec
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat.
L1572Axiom. (
add_nat_0R) We take the following as an axiom:
L1574Axiom. (
add_nat_SR) We take the following as an axiom:
L1575Axiom. (
add_nat_p) We take the following as an axiom:
L1577Axiom. (
add_nat_0L) We take the following as an axiom:
L1578Axiom. (
add_nat_SL) We take the following as an axiom:
L1579Axiom. (
add_nat_com) We take the following as an axiom:
L1582Axiom. (
add_nat_leq) We take the following as an axiom:
L1583Axiom. (
add_nat_ltL) We take the following as an axiom:
L1584Axiom. (
add_nat_ltR) We take the following as an axiom:
L1585Axiom. (
add_nat_mem_impred) We take the following as an axiom:
∀m, ∀n, nat_p n → ∀y ∈ m + n, ∀p : prop, (y ∈ m → p) → (∀i ∈ n, y = m + i → p) → p
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat.
L1590Axiom. (
mul_nat_0R) We take the following as an axiom:
L1591Axiom. (
mul_nat_SR) We take the following as an axiom:
L1592Axiom. (
mul_nat_p) We take the following as an axiom:
L1593Axiom. (
mul_nat_0L) We take the following as an axiom:
L1594Axiom. (
mul_nat_SL) We take the following as an axiom:
L1595Axiom. (
mul_nat_com) We take the following as an axiom:
L1599Definition. We define
exp_nat to be
λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type
set → set → set.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_nat.
L1602Axiom. (
exp_nat_0) We take the following as an axiom:
L1603Axiom. (
exp_nat_S) We take the following as an axiom:
L1604Axiom. (
equipI) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → equip X Y
L1605Axiom. (
equipE_impred) We take the following as an axiom:
∀X Y, equip X Y → ∀p : prop, (∀f : set → set, bij X Y f → p) → p
L1606Axiom. (
inj_incl) We take the following as an axiom:
∀X Y, X ⊆ Y → inj X Y (λx ⇒ x)
L1608Axiom. (
inj_id) We take the following as an axiom:
L1609Axiom. (
bij_id) We take the following as an axiom:
L1610Definition. We define
inv to be
λX f ⇒ λy : set ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y) of type
set → (set → set) → set → set.
L1612Axiom. (
surj_rinv) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀w ∈ Y, ∃u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X ∧ f (inv X f y) = y
L1614Axiom. (
inj_linv) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
L1615Axiom. (
bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
L1616Axiom. (
inj_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, inj X Y f → inj Y Z g → inj X Z (λx ⇒ g (f x))
L1617Axiom. (
bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))
L1618Axiom. (
equip_ref) We take the following as an axiom:
L1619Axiom. (
equip_sym) We take the following as an axiom:
L1620Axiom. (
equip_tra) We take the following as an axiom:
L1628Axiom. (
inj_Inj0) We take the following as an axiom:
L1629Axiom. (
inj_Inj1) We take the following as an axiom:
L1632Axiom. (
LoopI) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, binop_on X m → binop_on X b → binop_on X s → (∀x ∈ X, (m e x = x ∧ m x e = x)) → (∀x y ∈ X, (b x (m x y) = y ∧ m x (b x y) = y ∧ s (m x y) y = x ∧ m (s x y) y = x)) → Loop X m b s e
L1640Axiom. (
LoopE) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, Loop X m b s e → ∀p : prop, (binop_on X m → binop_on X b → binop_on X s → (∀x ∈ X, (m e x = x ∧ m x e = x)) → (∀x y ∈ X, (b x (m x y) = y ∧ m x (b x y) = y ∧ s (m x y) y = x ∧ m (s x y) y = x)) → p) → p
L1649Axiom. (
Loop_with_defs_I) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop X m b s e → (∀x y ∈ X, K x y = b (m y x) (m x y)) → (∀x y z ∈ X, a x y z = b (m x (m y z)) (m (m x y) z)) → (∀x u ∈ X, T x u = b x (m u x) ∧ I1 x u = m x (m u (b x e)) ∧ J1 x u = m (m (s e x) u) x ∧ I2 x u = m (b x u) (b (b x e) e) ∧ J2 x u = m (s e (s e x)) (s u x)) → (∀x y u ∈ X, L x y u = b (m y x) (m y (m x u)) ∧ R x y u = s (m (m u x) y) (m x y)) → Loop_with_defs X m b s e K a T L R I1 J1 I2 J2
L1664Axiom. (
Loop_with_defs_E) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → ∀p : prop, (Loop X m b s e → (∀x y ∈ X, K x y = b (m y x) (m x y)) → (∀x y z ∈ X, a x y z = b (m x (m y z)) (m (m x y) z)) → (∀x u ∈ X, T x u = b x (m u x) ∧ I1 x u = m x (m u (b x e)) ∧ J1 x u = m (m (s e x) u) x ∧ I2 x u = m (b x u) (b (b x e) e) ∧ J2 x u = m (s e (s e x)) (s u x)) → (∀x y u ∈ X, L x y u = b (m y x) (m y (m x u)) ∧ R x y u = s (m (m u x) y) (m x y)) → p) → p
L1682Axiom. (
Loop_with_defs_cex1_I0) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → (∃u x y w ∈ X, K (m (b (L x y u) e) u) w ≠ e) → Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2
L1689Axiom. (
Loop_with_defs_cex1_E0) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2 → ∀p : prop, (Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → (∃u x y w ∈ X, K (m (b (L x y u) e) u) w ≠ e) → p) → p
L1699Axiom. (
Loop_with_defs_cex1_I) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, ∀u x y w ∈ X, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → K (m (b (L x y u) e) u) w ≠ e → Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2
L1707Axiom. (
andE_imp) We take the following as an axiom:
∀A B p : prop, (A → B → p) → (A ∧ B → p)
L1708Axiom. (
orE_imp) We take the following as an axiom:
∀A B p : prop, (A → p) → (B → p) → (A ∨ B → p)
L1709Axiom. (
Loop_with_defs_cex1_E) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs_cex1 X m b s e K a T L R I1 J1 I2 J2 → ∀p : prop, (∀u x y w ∈ X, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → K (m (b (L x y u) e) u) w ≠ e → p) → p
L1720Axiom. (
Loop_with_defs_cex2_I0) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → (∃u x y z w ∈ X, a w (m (s e u) (R x y u)) z ≠ e) → Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2
L1727Axiom. (
Loop_with_defs_cex2_E0) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2 → ∀p : prop, (Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → (∃u x y z w ∈ X, a w (m (s e u) (R x y u)) z ≠ e) → p) → p
L1737Axiom. (
Loop_with_defs_cex2_I) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, ∀u x y z w ∈ X, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → a w (m (s e u) (R x y u)) z ≠ e → Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2
L1745Axiom. (
Loop_with_defs_cex2_E) We take the following as an axiom:
∀X, ∀m b s : set → set → set, ∀e : set, ∀K : set → set → set, ∀a : set → set → set → set, ∀T : set → set → set, ∀L R : set → set → set → set, ∀I1 J1 I2 J2 : set → set → set, Loop_with_defs_cex2 X m b s e K a T L R I1 J1 I2 J2 → ∀p : prop, (∀u x y z w ∈ X, Loop_with_defs X m b s e K a T L R I1 J1 I2 J2 → a w (m (s e u) (R x y u)) z ≠ e → p) → p
L1756Axiom. (
binop_on_1) We take the following as an axiom:
L1758Definition. We define
binop_table_2 to be
λx_0_0 x_0_1 x_1_0 x_1_1 i j ⇒ ((x_0_0,x_0_1),(x_1_0,x_1_1)) i j of type
set → set → set → set → set → set → set.
L1805Axiom. (
Z2_Loop) We take the following as an axiom:
L1816Definition. We define
binop_table_3 to be
λx_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 i j ⇒ ((x_0_0,x_0_1,x_0_2),(x_1_0,x_1_1,x_1_2),(x_2_0,x_2_1,x_2_2)) i j of type
set → set → set → set → set → set → set → set → set → set → set → set.
L1826Axiom. (
binop_table_3_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 0 = x_0_0
L1835Axiom. (
binop_table_3_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 1 = x_0_1
L1844Axiom. (
binop_table_3_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 0 2 = x_0_2
L1853Axiom. (
binop_table_3_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 0 = x_1_0
L1862Axiom. (
binop_table_3_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 1 = x_1_1
L1871Axiom. (
binop_table_3_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 1 2 = x_1_2
L1880Axiom. (
binop_table_3_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 0 = x_2_0
L1889Axiom. (
binop_table_3_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 1 = x_2_1
L1898Axiom. (
binop_table_3_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2, binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 2 2 = x_2_2
L1907Axiom. (
binop_table_on_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2 ∈ 3, binop_on 3 (binop_table_3 x_0_0 x_0_1 x_0_2 x_1_0 x_1_1 x_1_2 x_2_0 x_2_1 x_2_2)
L1916Definition. We define
binop_table_4 to be
λx_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 i j ⇒ ((x_0_0,x_0_1,x_0_2,x_0_3),(x_1_0,x_1_1,x_1_2,x_1_3),(x_2_0,x_2_1,x_2_2,x_2_3),(x_3_0,x_3_1,x_3_2,x_3_3)) i j of type
set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set.
L1928Axiom. (
binop_table_4_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 0 = x_0_0
L1939Axiom. (
binop_table_4_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 1 = x_0_1
L1950Axiom. (
binop_table_4_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 2 = x_0_2
L1961Axiom. (
binop_table_4_0_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 0 3 = x_0_3
L1972Axiom. (
binop_table_4_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 0 = x_1_0
L1983Axiom. (
binop_table_4_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 1 = x_1_1
L1994Axiom. (
binop_table_4_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 2 = x_1_2
L2005Axiom. (
binop_table_4_1_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 1 3 = x_1_3
L2016Axiom. (
binop_table_4_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 0 = x_2_0
L2027Axiom. (
binop_table_4_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 1 = x_2_1
L2038Axiom. (
binop_table_4_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 2 = x_2_2
L2049Axiom. (
binop_table_4_2_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 2 3 = x_2_3
L2060Axiom. (
binop_table_4_3_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 0 = x_3_0
L2071Axiom. (
binop_table_4_3_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 1 = x_3_1
L2082Axiom. (
binop_table_4_3_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 2 = x_3_2
L2093Axiom. (
binop_table_4_3_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3, binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 3 3 = x_3_3
L2104Axiom. (
binop_table_on_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3 ∈ 4, binop_on 4 (binop_table_4 x_0_0 x_0_1 x_0_2 x_0_3 x_1_0 x_1_1 x_1_2 x_1_3 x_2_0 x_2_1 x_2_2 x_2_3 x_3_0 x_3_1 x_3_2 x_3_3)
L2115Definition. We define
binop_table_5 to be
λx_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 i j ⇒ ((x_0_0,x_0_1,x_0_2,x_0_3,x_0_4),(x_1_0,x_1_1,x_1_2,x_1_3,x_1_4),(x_2_0,x_2_1,x_2_2,x_2_3,x_2_4),(x_3_0,x_3_1,x_3_2,x_3_3,x_3_4),(x_4_0,x_4_1,x_4_2,x_4_3,x_4_4)) i j of type
set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set → set.
L2129Axiom. (
binop_table_5_0_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 0 = x_0_0
L2142Axiom. (
binop_table_5_0_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 1 = x_0_1
L2155Axiom. (
binop_table_5_0_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 2 = x_0_2
L2168Axiom. (
binop_table_5_0_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 3 = x_0_3
L2181Axiom. (
binop_table_5_0_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 0 4 = x_0_4
L2194Axiom. (
binop_table_5_1_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 0 = x_1_0
L2207Axiom. (
binop_table_5_1_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 1 = x_1_1
L2220Axiom. (
binop_table_5_1_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 2 = x_1_2
L2233Axiom. (
binop_table_5_1_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 3 = x_1_3
L2246Axiom. (
binop_table_5_1_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 1 4 = x_1_4
L2259Axiom. (
binop_table_5_2_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 0 = x_2_0
L2272Axiom. (
binop_table_5_2_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 1 = x_2_1
L2285Axiom. (
binop_table_5_2_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 2 = x_2_2
L2298Axiom. (
binop_table_5_2_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 3 = x_2_3
L2311Axiom. (
binop_table_5_2_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 2 4 = x_2_4
L2324Axiom. (
binop_table_5_3_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 0 = x_3_0
L2337Axiom. (
binop_table_5_3_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 1 = x_3_1
L2350Axiom. (
binop_table_5_3_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 2 = x_3_2
L2363Axiom. (
binop_table_5_3_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 3 = x_3_3
L2376Axiom. (
binop_table_5_3_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 3 4 = x_3_4
L2389Axiom. (
binop_table_5_4_0) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 0 = x_4_0
L2402Axiom. (
binop_table_5_4_1) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 1 = x_4_1
L2415Axiom. (
binop_table_5_4_2) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 2 = x_4_2
L2428Axiom. (
binop_table_5_4_3) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 3 = x_4_3
L2441Axiom. (
binop_table_5_4_4) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 4 4 = x_4_4
L2454Axiom. (
binop_table_on_5) We take the following as an axiom:
∀x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 ∈ 5, binop_on 5 (binop_table_5 x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4)
Beginning of Section Combinators
L2471Let Ap : set → set → set ≝ λW Z : set ⇒ Inj1 (W + Z)
End of Section Combinators
L2508Axiom. (
setprod_I) We take the following as an axiom:
∀X Y, ∀u ∈ (λ_ ∈ X ⇒ Y), u ∈ X ⨯ Y
L2510Axiom. (
setprod_E) We take the following as an axiom:
∀X Y, ∀u ∈ X ⨯ Y, u ∈ (λ_ ∈ X ⇒ Y)
L2512Axiom. (
ap0_setprod) We take the following as an axiom:
∀X Y, ∀z ∈ X ⨯ Y, z 0 ∈ X
L2514Axiom. (
ap1_setprod) We take the following as an axiom:
∀X Y, ∀z ∈ X ⨯ Y, z 1 ∈ Y
L2518Axiom. (
lam_setexp) We take the following as an axiom:
∀X Y, ∀F : set → set, (∀x ∈ X, F x ∈ Y) → (λx ∈ X ⇒ F x) ∈ YX
L2520Axiom. (
ap_setexp) We take the following as an axiom:
∀X Y, ∀f ∈ YX, ∀x ∈ X, f x ∈ Y
L2522Axiom. (
setexp_ext) We take the following as an axiom:
∀X Y, ∀f g ∈ YX, (∀x ∈ X, f x = g x) → f = g
L2524Axiom. (
setexp_eta) We take the following as an axiom:
∀X Y, ∀f ∈ YX, (λx ∈ X ⇒ f x) = f
L2526Axiom. (
mul_nat_1R) We take the following as an axiom:
L2528Axiom. (
mul_nat_1L) We take the following as an axiom:
L2530Axiom. (
exp_nat_p) We take the following as an axiom:
L2532Axiom. (
exp_nat_1) We take the following as an axiom:
L2545Axiom. (
add_nat_leL) We take the following as an axiom:
L2547Axiom. (
add_nat_leR) We take the following as an axiom:
L2553Axiom. (
mul_nat_ltL) We take the following as an axiom:
L2555Axiom. (
mul_nat_ltR) We take the following as an axiom:
L2557Axiom. (
mul_nat_leL) We take the following as an axiom:
L2559Axiom. (
mul_nat_leR) We take the following as an axiom:
L2579Axiom. (
SetAdjoinI1) We take the following as an axiom:
L2581Axiom. (
SetAdjoinI2) We take the following as an axiom:
L2583Axiom. (
SetAdjoinE) We take the following as an axiom:
∀X y, ∀z ∈ SetAdjoin X y, ∀p : prop, (z ∈ X → p) → (z = y → p) → p
L2585Axiom. (
PNoEq__I) We take the following as an axiom:
L2587Axiom. (
PNoEq__E) We take the following as an axiom:
∀alpha, ∀p q : set → prop, ∀r : prop, ((∀beta ∈ alpha, p beta ↔ q beta) → r) → PNoEq_ alpha p q → r
L2591Axiom. (
PNoLt__I) We take the following as an axiom:
L2594Axiom. (
PNoLt__E) We take the following as an axiom:
L2613Axiom. (
PNo_downc_I) We take the following as an axiom:
L2619Axiom. (
PNo_downc_E) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ∀p : set → prop, ∀r : prop, (∀beta, ordinal beta → ∀q : set → prop, L beta q → PNoLe alpha p beta q → r) → PNo_downc L alpha p → r
L2625Axiom. (
PNo_upc_I) We take the following as an axiom:
L2631Axiom. (
PNo_upc_E) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ∀p : set → prop, ∀r : prop, (∀beta, ordinal beta → ∀q : set → prop, R beta q → PNoLe beta q alpha p → r) → PNo_upc R alpha p → r
L2637Axiom. (
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
L2639Axiom. (
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
L2641Axiom. (
PNoLe_downc) We take the following as an axiom:
L2645Axiom. (
PNoLe_upc) We take the following as an axiom:
L2649Definition. 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.
Beginning of Section TaggedSets
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L2676Axiom. (
SNoElts__I1) We take the following as an axiom:
L2678Axiom. (
SNoElts__I2) We take the following as an axiom:
L2680Axiom. (
SNoElts__E) We take the following as an axiom:
∀alpha, ∀p : set → prop, (∀beta ∈ alpha, p beta) → (∀beta ∈ alpha, p (beta ')) → ∀x ∈ SNoElts_ alpha, p x
L2685Axiom. (
SNoElts_mon) We take the following as an axiom:
L2687Axiom. (
SNo__I) We take the following as an axiom:
L2691Axiom. (
SNo__E) We take the following as an axiom:
L2695Axiom. (
PSNo_I1) We take the following as an axiom:
L2697Axiom. (
PSNo_I2) We take the following as an axiom:
L2699Axiom. (
PSNo_E) We take the following as an axiom:
∀alpha, ∀p q : set → prop, (∀beta ∈ alpha, p beta → q beta) → (∀beta ∈ alpha, ¬ p beta → q (beta ')) → ∀x ∈ PSNo alpha p, q x
End of Section TaggedSets
L2706Axiom. (
PNoEq_PSNo) We take the following as an axiom:
L2708Axiom. (
SNo_PSNo) We take the following as an axiom:
L2712Axiom. (
SNo_I) We take the following as an axiom:
L2714Axiom. (
SNo_E) We take the following as an axiom:
L2718Axiom. (
SNoLev_uniq) We take the following as an axiom:
L2720Axiom. (
SNoLev_prop) We take the following as an axiom:
L2726Axiom. (
SNoLev_) We take the following as an axiom:
L2730Axiom. (
SNoLev_PSNo) We take the following as an axiom:
L2732Axiom. (
SNo_Subq) We take the following as an axiom:
L2734Axiom. (
SNoEq_I) We take the following as an axiom:
L2736Axiom. (
SNoEq_E) We take the following as an axiom:
L2738Axiom. (
SNoEq_E') We take the following as an axiom:
L2740Axiom. (
SNoEq_E1) We take the following as an axiom:
L2742Axiom. (
SNoEq_E2) We take the following as an axiom:
L2746Axiom. (
SNo_eq) We take the following as an axiom:
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt.
L2750Axiom. (
SNoLtI) We take the following as an axiom:
L2752Axiom. (
SNoLtE) We take the following as an axiom:
L2754Axiom. (
SNoLtE') We take the following as an axiom:
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
L2759Axiom. (
SNoLeI) We take the following as an axiom:
L2761Axiom. (
SNoLeE) We take the following as an axiom:
L2763Axiom. (
SNoLeE') We take the following as an axiom:
L2765Axiom. (
SNoLtLe) We take the following as an axiom:
L2767Axiom. (
SNoLeE_or) We take the following as an axiom:
L2769Axiom. (
SNoEq_ref_) We take the following as an axiom:
L2771Axiom. (
SNoEq_sym_) We take the following as an axiom:
L2773Axiom. (
SNoEq_tra_) We take the following as an axiom:
L2775Axiom. (
SNoLtE3) We take the following as an axiom:
L2782Axiom. (
SNoLtI2) We take the following as an axiom:
L2788Axiom. (
SNoLtI3) We take the following as an axiom:
L2794Axiom. (
SNoLt_irref) We take the following as an axiom:
L2805Axiom. (
SNoLt_tra) We take the following as an axiom:
L2807Axiom. (
SNoLe_ref) We take the following as an axiom:
L2811Axiom. (
SNoLtLe_tra) We take the following as an axiom:
L2813Axiom. (
SNoLeLt_tra) We take the following as an axiom:
L2815Axiom. (
SNoLe_tra) We take the following as an axiom:
L2817Axiom. (
SNoLtLe_or) We take the following as an axiom: