Primitive. The name
Eps_i is a term of type
(set → prop) → set.
L2Axiom. (
Eps_i_ax) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
L4Definition. We define
True to be
∀p : prop, p → p of type
prop.
L6Definition. We define
False to be
∀p : prop, p of type
prop.
L7Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop.
Notation. We use
¬ as a prefix operator with priority 700 corresponding to applying term
not.
L12Definition. We define
and to be
λA B : prop ⇒ ∀p : prop, (A → B → p) → p 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.
L17Definition. We define
or to be
λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p 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.
L22Definition. We define
iff to be
λA B : prop ⇒ and (A → B) (B → A) 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
L30Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
L31Definition. 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 FE
L40Axiom. (
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
Beginning of Section Ex
L45Definition. 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.
L50Axiom. (
prop_ext) We take the following as an axiom:
∀p q : prop, iff p q → p = q
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.
L54Definition. We define
Subq to be
λA B ⇒ ∀x ∈ A, x ∈ B 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.
L56Axiom. (
set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
L58Axiom. (
In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X
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.
Primitive. The name
Empty is a term of type
set.
L64Axiom. (
EmptyAx) We take the following as an axiom:
Primitive. The name
⋃ is a term of type
set → set.
L68Axiom. (
UnionEq) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Primitive. The name
𝒫 is a term of type
set → set.
L73Axiom. (
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).
L78Axiom. (
ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x
L80Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U, x ⊆ U of type
set → prop.
L82Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type
set → prop.
L84Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type
set → prop.
L85Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set, X ∈ U → ∀F : set → set, (∀x : set, x ∈ X → F x ∈ U) → {F x|x ∈ X} ∈ U of type
set → prop.
Primitive. The name
UnivOf is a term of type
set → set.
L93Axiom. (
UnivOf_In) We take the following as an axiom:
L99Axiom. (
UnivOf_Min) We take the following as an axiom:
L104Axiom. (
FalseE) We take the following as an axiom:
L106Axiom. (
TrueI) We take the following as an axiom:
L108Axiom. (
notI) We take the following as an axiom:
L110Axiom. (
notE) We take the following as an axiom:
L112Axiom. (
andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
L114Axiom. (
andEL) We take the following as an axiom:
L116Axiom. (
andER) We take the following as an axiom:
L118Axiom. (
orIL) We take the following as an axiom:
L120Axiom. (
orIR) We take the following as an axiom:
L122Axiom. (
orE) We take the following as an axiom:
∀A B C : prop, (A → C) → (B → C) → A ∨ B → C
Beginning of Section PropN
L126Variable P1 P2 P3 : prop
L128Axiom. (
and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
L130Axiom. (
and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
L131Axiom. (
or3I1) We take the following as an axiom:
L132Axiom. (
or3I2) We take the following as an axiom:
L133Axiom. (
or3I3) We take the following as an axiom:
L134Axiom. (
or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
L137Axiom. (
and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
L139Axiom. (
and4E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 → (∀p : prop, (P1 → P2 → P3 → P4 → p) → p)
L140Axiom. (
or4I1) We take the following as an axiom:
L141Axiom. (
or4I2) We take the following as an axiom:
L142Axiom. (
or4I3) We take the following as an axiom:
L143Axiom. (
or4I4) We take the following as an axiom:
L144Axiom. (
or4E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 ∨ P4 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → p)
L147Axiom. (
and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
L149Axiom. (
and5E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → p) → p)
L150Axiom. (
or5I1) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L151Axiom. (
or5I2) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L152Axiom. (
or5I3) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L153Axiom. (
or5I4) We take the following as an axiom:
P4 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L154Axiom. (
or5I5) We take the following as an axiom:
P5 → P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5
L155Axiom. (
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)
L158Axiom. (
and6I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
L160Axiom. (
and6E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → p) → p)
L163Axiom. (
and7I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
L165Axiom. (
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
L168Axiom. (
iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
L170Axiom. (
iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
L171Axiom. (
iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
L172Axiom. (
iff_ref) We take the following as an axiom:
L173Axiom. (
neq_i_sym) We take the following as an axiom:
L175Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop.
Notation. We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn.
L181Axiom. (
Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
L183Axiom. (
pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
L185Axiom. (
prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
L186Axiom. (
pred_ext_2) We take the following as an axiom:
∀P Q : set → prop, P ⊆ Q → Q ⊆ P → P = Q
L187Axiom. (
Subq_ref) We take the following as an axiom:
L189Axiom. (
Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
L190Axiom. (
Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X
L191Axiom. (
EmptyE) We take the following as an axiom:
L193Axiom. (
Subq_Empty) We take the following as an axiom:
L195Axiom. (
Empty_eq) We take the following as an axiom:
L196Axiom. (
UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
L198Axiom. (
UnionE) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
L199Axiom. (
UnionE_impred) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
L200Axiom. (
Union_Empty) We take the following as an axiom:
L202Axiom. (
PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
L204Axiom. (
PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
L205Axiom. (
Power_Subq) We take the following as an axiom:
∀X Y : set, X ⊆ Y → 𝒫 X ⊆ 𝒫 Y
L210Axiom. (
xm) We take the following as an axiom:
L212Axiom. (
dneg) We take the following as an axiom:
L213Axiom. (
imp_not_or) We take the following as an axiom:
∀p q : prop, (p → q) → ¬ p ∨ q
Primitive. The name
exactly1of2 is a term of type
prop → prop → prop.
L223Axiom. (
exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p
Primitive. The name
exactly1of3 is a term of type
prop → prop → prop → prop.
L245Axiom. (
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
L263Axiom. (
ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
L265Axiom. (
ReplE) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
L267Axiom. (
ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p
L269Axiom. (
Repl_Empty) We take the following as an axiom:
L271Axiom. (
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}
L273Axiom. (
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}
Primitive. The name
If_i is a term of type
prop → set → set → set.
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.
L283Axiom. (
If_i_0) We take the following as an axiom:
L286Axiom. (
If_i_1) We take the following as an axiom:
L289Axiom. (
If_i_or) We take the following as an axiom:
L291Axiom. (
If_i_eta) We take the following as an axiom:
Primitive. The name
UPair is a term of type
set → set → set.
Notation.
{x,y} is notation for
UPair x y.
L298Axiom. (
UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
L301Axiom. (
UPairI1) We take the following as an axiom:
L303Axiom. (
UPairI2) We take the following as an axiom:
L305Axiom. (
UPair_com) We take the following as an axiom:
Primitive. The name
Sing is a term of type
set → set.
Notation.
{x} is notation for
Sing x.
L311Axiom. (
SingI) We take the following as an axiom:
L313Axiom. (
SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
Primitive. The name
binunion is a term of type
set → set → set.
Notation. We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion.
L320Axiom. (
binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
L322Axiom. (
binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
L324Axiom. (
binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
L326Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ {y} of type
set → set → set.
Notation. We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty 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.
L332Axiom. (
Repl_UPair) We take the following as an axiom:
∀F : set → set, ∀x y : set, {F z|z ∈ {x,y}} = {F x,F y}
L334Axiom. (
Repl_Sing) We take the following as an axiom:
∀F : set → set, ∀x : set, {F z|z ∈ {x}} = {F x}
L336Axiom. (
Repl_restr) We take the following as an axiom:
∀X : set, ∀F G : set → set, (∀x : set, x ∈ X → F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}
L338Definition. We define
famunion to be
λX F ⇒ ⋃ {F x|x ∈ X} of type
set → (set → set) → set.
Notation. We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion.
L344Axiom. (
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
L346Axiom. (
famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
L348Axiom. (
famunionE_impred) 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
L354Axiom. (
Power_Sing) We take the following as an axiom:
Primitive. The name
Sep is a term of type
set → (set → prop) → set.
Notation.
{x ∈ A | B} is notation for
Sep A (λ x . B).
L362Axiom. (
SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
L364Axiom. (
SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
L365Axiom. (
SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
L366Axiom. (
SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
L367Axiom. (
Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
L369Axiom. (
Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
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).
L375Axiom. (
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}
L377Axiom. (
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
L379Axiom. (
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
Primitive. The name
ReplSep2 is a term of type
set → (set → set) → (set → set → prop) → (set → set → set) → set.
L384Axiom. (
ReplSep2I) We take the following as an axiom:
∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀x ∈ A, ∀y ∈ B x, P x y → F x y ∈ ReplSep2 A B P F
L386Axiom. (
ReplSep2E_impred) We take the following as an axiom:
∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀r ∈ ReplSep2 A B P F, ∀p : prop, (∀x ∈ A, ∀y ∈ B x, P x y → r = F x y → p) → p
L388Axiom. (
ReplSep2E) We take the following as an axiom:
∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀r ∈ ReplSep2 A B P F, ∃x ∈ A, ∃y ∈ B x, P x y ∧ r = F x y
L390Axiom. (
binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
L392Axiom. (
binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
L400Axiom. (
binunion_nIn_I) We take the following as an axiom:
∀X Y z : set, z ∉ X → z ∉ Y → z ∉ X ∪ Y
L401Axiom. (
binunion_nIn_E) We take the following as an axiom:
∀X Y z : set, z ∉ X ∪ Y → z ∉ X ∧ z ∉ Y
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.
L408Axiom. (
binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
L410Axiom. (
binintersectE) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
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.
L434Axiom. (
setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
L436Axiom. (
setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
L437Axiom. (
setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
L438Axiom. (
setminusE2) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∉ Y
L452Axiom. (
In_irref) We take the following as an axiom:
L454Axiom. (
In_no2cycle) We take the following as an axiom:
L455Axiom. (
In_no3cycle) We take the following as an axiom:
Primitive. The name
ordsucc is a term of type
set → set.
L459Axiom. (
ordsuccI1) We take the following as an axiom:
L461Axiom. (
ordsuccI2) We take the following as an axiom:
L462Axiom. (
ordsuccE) We take the following as an axiom:
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc.
L468Axiom. (
ordsucc_inj) We take the following as an axiom:
L471Axiom. (
In_0_1) We take the following as an axiom:
L473Axiom. (
In_0_2) We take the following as an axiom:
L474Axiom. (
In_1_2) We take the following as an axiom:
L475Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop, p 0 → (∀x : set, p x → p (ordsucc x)) → p n of type
set → prop.
L477Axiom. (
nat_0) We take the following as an axiom:
L479Axiom. (
nat_ordsucc) We take the following as an axiom:
L480Axiom. (
nat_1) We take the following as an axiom:
L481Axiom. (
nat_2) We take the following as an axiom:
L482Axiom. (
nat_3) We take the following as an axiom:
L483Axiom. (
nat_4) We take the following as an axiom:
L484Axiom. (
nat_5) We take the following as an axiom:
L485Axiom. (
nat_6) We take the following as an axiom:
L488Axiom. (
nat_ind) We take the following as an axiom:
L489Axiom. (
nat_inv) We take the following as an axiom:
L491Axiom. (
nat_p_trans) We take the following as an axiom:
L492Axiom. (
nat_trans) We take the following as an axiom:
L496Axiom. (
In_0_3) We take the following as an axiom:
L498Axiom. (
In_1_3) We take the following as an axiom:
L499Axiom. (
In_2_3) We take the following as an axiom:
L500Axiom. (
In_0_4) We take the following as an axiom:
L501Axiom. (
In_1_4) We take the following as an axiom:
L502Axiom. (
In_2_4) We take the following as an axiom:
L503Axiom. (
In_3_4) We take the following as an axiom:
L504Axiom. (
In_0_5) We take the following as an axiom:
L505Axiom. (
In_1_5) We take the following as an axiom:
L506Axiom. (
In_2_5) We take the following as an axiom:
L507Axiom. (
In_3_5) We take the following as an axiom:
L508Axiom. (
In_4_5) We take the following as an axiom:
L509Axiom. (
In_0_6) We take the following as an axiom:
L510Axiom. (
In_1_6) We take the following as an axiom:
L511Axiom. (
In_2_6) We take the following as an axiom:
L512Axiom. (
In_3_6) We take the following as an axiom:
L513Axiom. (
In_4_6) We take the following as an axiom:
L514Axiom. (
In_5_6) We take the following as an axiom:
L515Axiom. (
cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
L517Axiom. (
cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
L518Axiom. (
cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
L519Axiom. (
cases_4) We take the following as an axiom:
∀i ∈ 4, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p i
L520Axiom. (
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
L521Axiom. (
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
L522Axiom. (
neq_0_1) We take the following as an axiom:
L524Axiom. (
neq_0_2) We take the following as an axiom:
L525Axiom. (
neq_1_2) We take the following as an axiom:
L526Axiom. (
neq_1_0) We take the following as an axiom:
L527Axiom. (
neq_2_0) We take the following as an axiom:
L528Axiom. (
neq_2_1) We take the following as an axiom:
L529Axiom. (
neq_3_0) We take the following as an axiom:
L530Axiom. (
neq_3_1) We take the following as an axiom:
L531Axiom. (
neq_3_2) We take the following as an axiom:
L532Axiom. (
neq_4_0) We take the following as an axiom:
L533Axiom. (
neq_4_1) We take the following as an axiom:
L534Axiom. (
neq_4_2) We take the following as an axiom:
L535Axiom. (
neq_4_3) We take the following as an axiom:
L536Axiom. (
neq_5_0) We take the following as an axiom:
L537Axiom. (
neq_5_1) We take the following as an axiom:
L538Axiom. (
neq_5_2) We take the following as an axiom:
L539Axiom. (
neq_5_3) We take the following as an axiom:
L540Axiom. (
neq_5_4) We take the following as an axiom:
L541Axiom. (
ZF_closed_I) We take the following as an axiom:
L547Axiom. (
ZF_closed_E) We take the following as an axiom:
L579Axiom. (
omega_nat_p) We take the following as an axiom:
L581Axiom. (
nat_p_omega) We take the following as an axiom:
L601Axiom. (
ordinal_1) We take the following as an axiom:
L603Axiom. (
ordinal_2) We take the following as an axiom:
L635Axiom. (
ordinal_Sep) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, (∀beta ∈ alpha, ∀gamma ∈ beta, p beta → p gamma) → ordinal {beta ∈ alpha|p beta}
L637Definition. We define
inj to be
λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type
set → set → (set → set) → prop.
L643Definition. We define
surj to be
λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type
set → set → (set → set) → prop.
L649Definition. We define
bij to be
λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type
set → set → (set → set) → prop.
L657Axiom. (
bijI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → bij X Y f
L663Axiom. (
bijE) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, ((∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → p) → p
Primitive. The name
inv is a term of type
set → (set → set) → set → set.
L675Axiom. (
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
L677Axiom. (
inj_linv) We take the following as an axiom:
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
L679Axiom. (
bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
L681Axiom. (
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))
L683Axiom. (
bij_id) We take the following as an axiom:
L685Axiom. (
bij_inj) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → inj X Y f
L687Axiom. (
bij_surj) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → surj X Y f
L689Axiom. (
inj_surj_bij) We take the following as an axiom:
∀X Y, ∀f : set → set, inj X Y f → surj X Y f → bij X Y f
L691Axiom. (
surj_inv_inj) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀y ∈ Y, ∃x ∈ X, f x = y) → inj Y X (inv X f)
L693Definition. We define
atleastp to be
λX Y : set ⇒ ∃f : set → set, inj X Y f of type
set → set → prop.
L696Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set, bij X Y f of type
set → set → prop.
L699Axiom. (
equip_ref) We take the following as an axiom:
L701Axiom. (
equip_sym) We take the following as an axiom:
L702Axiom. (
equip_tra) We take the following as an axiom:
L706Axiom. (
KnasterTarski_set) We take the following as an axiom:
∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y
L711Axiom. (
image_In_Power) We take the following as an axiom:
∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B
L716Axiom. (
f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
L718Axiom. (
f_eq_i_i) We take the following as an axiom:
∀f : set → set → set, ∀x y z w, x = y → z = w → f x z = f y w
L719Axiom. (
eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
L720Definition. We define
nSubq to be
λX Y ⇒ ¬ Subq X Y of type
set → set → prop.
Notation. We use
⊈ as an infix operator with priority 502 and no associativity corresponding to applying term
nSubq.
L726Axiom. (
Sing_inv) We take the following as an axiom:
∀x Y, {x} = Y → x ∈ Y ∧ ∀y ∈ Y, y = x
L730Axiom. (
inv_Repl_eq) We take the following as an axiom:
∀X, ∀f g : set → set, (∀x ∈ X, f (g x) = x) → {f y|y ∈ {g x|x ∈ X}} = X
L731Axiom. (
invol_Repl_eq) We take the following as an axiom:
∀X, ∀f : set → set, (∀x ∈ X, f (f x) = x) → {f y|y ∈ {f x|x ∈ X}} = X
L732Axiom. (
Eps_i_set_R) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀x ∈ X, P x → Eps_i (λx ⇒ x ∈ X ∧ P x) ∈ X ∧ P (Eps_i (λx ⇒ x ∈ X ∧ P x))
L734Axiom. (
exandE_i) We take the following as an axiom:
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
L736Axiom. (
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
L738Axiom. (
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
L740Axiom. (
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
L742Axiom. (
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
L744Axiom. (
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
Beginning of Section Descr_ii
L748Variable P : (set → set) → prop
Primitive. The name
Descr_ii is a term of type
set → set.
L753Hypothesis Pex : ∃f : set → set, P f
L755Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
L762Variable P : (set → set → set) → prop
Primitive. The name
Descr_iii is a term of type
set → set → set.
L767Hypothesis Pex : ∃f : set → set → set, P f
L769Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_iio
L776Variable P : (set → set → prop) → prop
Primitive. The name
Descr_iio is a term of type
set → set → prop.
L781Hypothesis Pex : ∃f : set → set → prop, P f
L783Hypothesis Puniq : ∀f g : set → set → prop, P f → P g → f = g
End of Section Descr_iio
Beginning of Section Descr_Vo1
Primitive. The name
Descr_Vo1 is a term of type
Vo 1.
L795Hypothesis Pex : ∃f : Vo 1, P f
L797Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section Descr_Vo2
Primitive. The name
Descr_Vo2 is a term of type
Vo 2.
L809Hypothesis Pex : ∃f : Vo 2, P f
L811Hypothesis Puniq : ∀f g : Vo 2, P f → P g → f = g
End of Section Descr_Vo2
Beginning of Section If_ii
L820Variable f g : set → set
Primitive. The name
If_ii is a term of type
set → set.
L824Axiom. (
If_ii_1) We take the following as an axiom:
L826Axiom. (
If_ii_0) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
L834Variable f g : set → set → set
Primitive. The name
If_iii is a term of type
set → set → set.
L838Axiom. (
If_iii_1) We take the following as an axiom:
L840Axiom. (
If_iii_0) We take the following as an axiom:
End of Section If_iii
Beginning of Section If_Vo1
Primitive. The name
If_Vo1 is a term of type
Vo 1.
L852Axiom. (
If_Vo1_1) We take the following as an axiom:
L854Axiom. (
If_Vo1_0) We take the following as an axiom:
End of Section If_Vo1
Beginning of Section If_iio
L862Variable f g : set → set → prop
Primitive. The name
If_iio is a term of type
set → set → prop.
L866Axiom. (
If_iio_1) We take the following as an axiom:
L868Axiom. (
If_iio_0) We take the following as an axiom:
End of Section If_iio
Beginning of Section If_Vo2
Primitive. The name
If_Vo2 is a term of type
Vo 2.
L880Axiom. (
If_Vo2_1) We take the following as an axiom:
L882Axiom. (
If_Vo2_0) We take the following as an axiom:
End of Section If_Vo2
Beginning of Section EpsilonRec_i
L888Variable F : set → (set → set) → set
Primitive. The name
In_rec_i is a term of type
set → set.
L893Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
L895Axiom. (
In_rec_i_eq) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L901Variable F : set → (set → (set → set)) → (set → set)
Primitive. The name
In_rec_ii is a term of type
set → (set → set).
L906Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
L914Variable F : set → (set → (set → set → set)) → (set → set → set)
Primitive. The name
In_rec_iii is a term of type
set → (set → set → set).
L919Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_iii
Beginning of Section EpsilonRec_iio
L927Variable F : set → (set → (set → set → prop)) → (set → set → prop)
Primitive. The name
In_rec_iio is a term of type
set → (set → set → prop).
L932Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → prop), (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_iio
Beginning of Section EpsilonRec_Vo1
L940Variable F : set → (set → Vo 1) → Vo 1
Primitive. The name
In_rec_Vo1 is a term of type
set → Vo 1.
L945Hypothesis Fr : ∀X : set, ∀g h : set → Vo 1, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_Vo1
Beginning of Section EpsilonRec_Vo2
L953Variable F : set → (set → Vo 2) → Vo 2
Primitive. The name
In_rec_Vo2 is a term of type
set → Vo 2.
L958Hypothesis Fr : ∀X : set, ∀g h : set → Vo 2, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_Vo2
Beginning of Section If_Vo3
Primitive. The name
If_Vo3 is a term of type
Vo 3.
L972Axiom. (
If_Vo3_1) We take the following as an axiom:
L974Axiom. (
If_Vo3_0) We take the following as an axiom:
End of Section If_Vo3
Beginning of Section Descr_Vo3
Primitive. The name
Descr_Vo3 is a term of type
Vo 3.
L985Hypothesis Pex : ∃f : Vo 3, P f
L987Hypothesis Puniq : ∀f g : Vo 3, P f → P g → f = g
End of Section Descr_Vo3
Beginning of Section EpsilonRec_Vo3
L994Variable F : set → (set → Vo 3) → Vo 3
Primitive. The name
In_rec_Vo3 is a term of type
set → Vo 3.
L999Hypothesis Fr : ∀X : set, ∀g h : set → Vo 3, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_Vo3
Beginning of Section If_Vo4
Primitive. The name
If_Vo4 is a term of type
Vo 4.
L1013Axiom. (
If_Vo4_1) We take the following as an axiom:
L1015Axiom. (
If_Vo4_0) We take the following as an axiom:
End of Section If_Vo4
Beginning of Section Descr_Vo4
Primitive. The name
Descr_Vo4 is a term of type
Vo 4.
L1025Hypothesis Pex : ∃f : Vo 4, P f
L1027Hypothesis Puniq : ∀f g : Vo 4, P f → P g → f = g
End of Section Descr_Vo4
Beginning of Section EpsilonRec_Vo4
L1034Variable F : set → (set → Vo 4) → Vo 4
Primitive. The name
In_rec_Vo4 is a term of type
set → Vo 4.
L1039Hypothesis Fr : ∀X : set, ∀g h : set → Vo 4, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_Vo4
L1045Definition. We define
bigintersect to be
λ(D : (set → prop) → prop)(x : set) ⇒ ∀P : set → prop, D P → P x.
L1047Definition. We define
reflexive to be
λR ⇒ ∀x : set, R x x of type
(set → set → prop) → prop.
L1049Definition. We define
irreflexive to be
λR ⇒ ∀x : set, ¬ R x x of type
(set → set → prop) → prop.
L1050Definition. We define
symmetric to be
λR ⇒ ∀x y : set, R x y → R y x of type
(set → set → prop) → prop.
L1051Definition. We define
antisymmetric to be
λR ⇒ ∀x y : set, R x y → R y x → x = y of type
(set → set → prop) → prop.
L1052Definition. We define
transitive to be
λR ⇒ ∀x y z : set, R x y → R y z → R x z of type
(set → set → prop) → prop.
L1055Definition. We define
linear to be
λR ⇒ ∀x y : set, R x y ∨ R y x of type
(set → set → prop) → prop.
L1056Definition. We define
trichotomous_or to be
λR ⇒ ∀x y : set, R x y ∨ x = y ∨ R y x of type
(set → set → prop) → prop.
L1061Axiom. (
per_sym) We take the following as an axiom:
L1063Axiom. (
per_tra) We take the following as an axiom:
L1065Axiom. (
per_stra1) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R y x → R y z → R x z
L1067Axiom. (
per_stra2) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R x y → R z y → R x z
L1069Axiom. (
per_stra3) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R y x → R z y → R x z
L1071Axiom. (
per_ref1) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y : set, R x y → R x x
L1073Axiom. (
per_ref2) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y : set, R x y → R y y
L1078Definition. We define
reflclos to be
λR x y ⇒ R x y ∨ x = y of type
(set → set → prop) → (set → set → prop).
Beginning of Section Zermelo1908
Primitive. The name
ZermeloWO is a term of type
set → set → prop.
L1102Axiom. (
ZermeloWO_wo) We take the following as an axiom:
∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y → ZermeloWO x y
L1109Axiom. (
Zermelo_WO) We take the following as an axiom:
∃r : set → set → prop, totalorder r ∧ (∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y → r x y)
End of Section Zermelo1908
L1119Axiom. (
eq_imp_or) We take the following as an axiom:
(λx y : prop ⇒ (x → y)) = (λx y : prop ⇒ (¬ x ∨ y))
L1123Axiom. (
Empty_or_ex) We take the following as an axiom:
L1125Axiom. (
nIn_0_0) We take the following as an axiom:
L1127Axiom. (
nIn_1_0) We take the following as an axiom:
L1128Axiom. (
nIn_2_0) We take the following as an axiom:
L1129Axiom. (
nIn_1_1) We take the following as an axiom:
L1130Axiom. (
nIn_2_2) We take the following as an axiom:
L1131Axiom. (
Subq_0_0) We take the following as an axiom:
L1132Axiom. (
Subq_0_1) We take the following as an axiom:
L1133Axiom. (
Subq_0_2) We take the following as an axiom:
L1134Axiom. (
nSubq_1_0) We take the following as an axiom:
L1135Axiom. (
Subq_1_1) We take the following as an axiom:
L1136Axiom. (
Subq_1_2) We take the following as an axiom:
L1137Axiom. (
nSubq_2_0) We take the following as an axiom:
L1138Axiom. (
nSubq_2_1) We take the following as an axiom:
L1139Axiom. (
Subq_2_2) We take the following as an axiom:
L1140Axiom. (
In_0_7) We take the following as an axiom:
L1141Axiom. (
In_1_7) We take the following as an axiom:
L1142Axiom. (
In_2_7) We take the following as an axiom:
L1143Axiom. (
In_3_7) We take the following as an axiom:
L1144Axiom. (
In_4_7) We take the following as an axiom:
L1145Axiom. (
In_5_7) We take the following as an axiom:
L1146Axiom. (
In_6_7) We take the following as an axiom:
L1147Axiom. (
In_0_8) We take the following as an axiom:
L1148Axiom. (
In_1_8) We take the following as an axiom:
L1149Axiom. (
In_2_8) We take the following as an axiom:
L1150Axiom. (
In_3_8) We take the following as an axiom:
L1151Axiom. (
In_4_8) We take the following as an axiom:
L1152Axiom. (
In_5_8) We take the following as an axiom:
L1153Axiom. (
In_6_8) We take the following as an axiom:
L1154Axiom. (
In_7_8) We take the following as an axiom:
L1155Axiom. (
In_0_9) We take the following as an axiom:
L1156Axiom. (
In_1_9) We take the following as an axiom:
L1157Axiom. (
In_2_9) We take the following as an axiom:
L1158Axiom. (
In_3_9) We take the following as an axiom:
L1159Axiom. (
In_4_9) We take the following as an axiom:
L1160Axiom. (
In_5_9) We take the following as an axiom:
L1161Axiom. (
In_6_9) We take the following as an axiom:
L1162Axiom. (
In_7_9) We take the following as an axiom:
L1163Axiom. (
In_8_9) We take the following as an axiom:
Beginning of Section NatRec
L1168Variable f : set → set → set
L1169Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
L1172Axiom. (
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
Beginning of Section NatArith
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat.
L1186Axiom. (
add_nat_0R) We take the following as an axiom:
L1188Axiom. (
add_nat_SR) We take the following as an axiom:
L1190Axiom. (
add_nat_p) We take the following as an axiom:
L1194Axiom. (
add_nat_0L) We take the following as an axiom:
L1196Axiom. (
add_nat_SL) We take the following as an axiom:
L1198Axiom. (
add_nat_com) We take the following as an axiom:
L1200Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type
set → set → set.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat.
L1204Axiom. (
mul_nat_0R) We take the following as an axiom:
L1206Axiom. (
mul_nat_SR) We take the following as an axiom:
L1208Axiom. (
mul_nat_p) We take the following as an axiom:
L1210Axiom. (
mul_nat_0L) We take the following as an axiom:
L1212Axiom. (
mul_nat_SL) We take the following as an axiom:
L1214Axiom. (
mul_nat_com) We take the following as an axiom:
L1237Definition. 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.
End of Section NatArith
L1252Axiom. (
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
L1254Axiom. (
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
L1255Axiom. (
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
L1256Axiom. (
nIn_2_1) We take the following as an axiom:
L1258Axiom. (
neq_6_0) We take the following as an axiom:
L1259Axiom. (
neq_6_1) We take the following as an axiom:
L1260Axiom. (
neq_6_2) We take the following as an axiom:
L1261Axiom. (
neq_6_3) We take the following as an axiom:
L1262Axiom. (
neq_6_4) We take the following as an axiom:
L1263Axiom. (
neq_6_5) We take the following as an axiom:
L1264Axiom. (
neq_7_0) We take the following as an axiom:
L1265Axiom. (
neq_7_1) We take the following as an axiom:
L1266Axiom. (
neq_7_2) We take the following as an axiom:
L1267Axiom. (
neq_7_3) We take the following as an axiom:
L1268Axiom. (
neq_7_4) We take the following as an axiom:
L1269Axiom. (
neq_7_5) We take the following as an axiom:
L1270Axiom. (
neq_7_6) We take the following as an axiom:
L1271Axiom. (
neq_8_0) We take the following as an axiom:
L1272Axiom. (
neq_8_1) We take the following as an axiom:
L1273Axiom. (
neq_8_2) We take the following as an axiom:
L1274Axiom. (
neq_8_3) We take the following as an axiom:
L1275Axiom. (
neq_8_4) We take the following as an axiom:
L1276Axiom. (
neq_8_5) We take the following as an axiom:
L1277Axiom. (
neq_8_6) We take the following as an axiom:
L1278Axiom. (
neq_8_7) We take the following as an axiom:
L1279Axiom. (
neq_9_0) We take the following as an axiom:
L1280Axiom. (
neq_9_1) We take the following as an axiom:
L1281Axiom. (
neq_9_2) We take the following as an axiom:
L1282Axiom. (
neq_9_3) We take the following as an axiom:
L1283Axiom. (
neq_9_4) We take the following as an axiom:
L1284Axiom. (
neq_9_5) We take the following as an axiom:
L1285Axiom. (
neq_9_6) We take the following as an axiom:
L1286Axiom. (
neq_9_7) We take the following as an axiom:
L1287Axiom. (
neq_9_8) We take the following as an axiom:
L1290Axiom. (
eq_1_Sing0) We take the following as an axiom:
L1294Axiom. (
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
L1308Axiom. (
Inj1_eq) We take the following as an axiom:
L1310Axiom. (
Inj1I1) We take the following as an axiom:
L1311Axiom. (
Inj1I2) We take the following as an axiom:
L1312Axiom. (
Inj1E) We take the following as an axiom:
L1313Axiom. (
Inj1NE1) We take the following as an axiom:
L1314Axiom. (
Inj1NE2) We take the following as an axiom:
L1315Definition. We define
Inj0 to be
λX ⇒ {Inj1 x|x ∈ X} of type
set → set.
L1318Axiom. (
Inj0I) We take the following as an axiom:
L1320Axiom. (
Inj0E) We take the following as an axiom:
L1324Axiom. (
Unj_eq) We take the following as an axiom:
L1326Axiom. (
Unj_Inj1_eq) We take the following as an axiom:
L1327Axiom. (
Inj1_inj) We take the following as an axiom:
L1328Axiom. (
Unj_Inj0_eq) We take the following as an axiom:
L1329Axiom. (
Inj0_inj) We take the following as an axiom:
L1330Axiom. (
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.
L1338Axiom. (
Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
L1340Axiom. (
Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
L1346Axiom. (
setsum_0_0) We take the following as an axiom:
L1349Axiom. (
setsum_mon) We take the following as an axiom:
∀X Y W Z, X ⊆ W → Y ⊆ Z → X + Y ⊆ W + Z
Beginning of Section pair_setsum
L1364Axiom. (
pair_0_0) We take the following as an axiom:
L1366Axiom. (
pair_1_0_1) We take the following as an axiom:
L1367Axiom. (
pair_1_1_2) We take the following as an axiom:
L1375Axiom. (
pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
L1376Axiom. (
pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
L1377Axiom. (
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)
L1378Axiom. (
pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
L1379Axiom. (
pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
L1380Axiom. (
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)
L1381Axiom. (
pairSubq) We take the following as an axiom:
∀X Y W Z, X ⊆ W → Y ⊆ Z → pair X Y ⊆ pair W Z
L1382Axiom. (
proj0I) We take the following as an axiom:
L1383Axiom. (
proj0E) We take the following as an axiom:
L1384Axiom. (
proj1I) We take the following as an axiom:
L1385Axiom. (
proj1E) We take the following as an axiom:
L1388Axiom. (
pair_inj) We take the following as an axiom:
∀x y w z : set, pair x y = pair w z → x = w ∧ y = z
L1390Definition. We define
Sigma to be
λX Y ⇒ ⋃x ∈ X{pair x y|y ∈ Y x} of type
set → (set → set) → set.
Notation. We use
∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma.
L1397Axiom. (
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
L1403Axiom. (
proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X
L1405Axiom. (
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)
L1407Axiom. (
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
L1409Axiom. (
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
L1411Axiom. (
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
L1413Axiom. (
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
L1415Axiom. (
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
L1418Axiom. (
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
L1420Axiom. (
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
L1422Axiom. (
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
L1424Definition. We define
setprod to be
λX Y : set ⇒ ∑x ∈ X, Y of type
set → set → set.
Notation. We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod.
L1429Axiom. (
pair_setprod) We take the following as an axiom:
∀X Y : set, ∀(x ∈ X)(y ∈ Y), pair x y ∈ X ⨯ Y
L1435Axiom. (
pair_setprod_E0) We take the following as an axiom:
∀X Y x y : set, pair x y ∈ X ⨯ Y → x ∈ X
L1437Axiom. (
pair_setprod_E1) We take the following as an axiom:
∀X Y x y : set, pair x y ∈ X ⨯ Y → y ∈ Y
L1439Let lam : set → (set → set) → set ≝ Sigma
L1442Definition. We define
ap to be
λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type
set → set → set.
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
Sigma 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.
L1448Axiom. (
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
L1450Axiom. (
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
L1452Axiom. (
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
L1454Axiom. (
apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
L1456Axiom. (
apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
L1458Axiom. (
apEq) We take the following as an axiom:
∀f x y, y ∈ f x ↔ pair x y ∈ f
L1460Axiom. (
beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
L1462Axiom. (
beta0) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∉ X → (λx ∈ X ⇒ F x) x = 0
L1464Axiom. (
proj0_ap_0) We take the following as an axiom:
L1466Axiom. (
proj1_ap_1) We take the following as an axiom:
L1468Axiom. (
pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
L1470Axiom. (
pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
L1472Axiom. (
pair_ap_n2) We take the following as an axiom:
∀x y i : set, i ∉ 2 → (pair x y) i = 0
L1474Axiom. (
ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
L1476Axiom. (
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))
L1478Definition. We define
pair_p to be
λu : set ⇒ pair (u 0) (u 1) = u of type
set → prop.
L1481Axiom. (
pair_p_I) We take the following as an axiom:
L1483Axiom. (
pair_p_I2) We take the following as an axiom:
L1487Definition. We define
tuple_p to be
λn u ⇒ ∀z ∈ u, ∃i ∈ n, ∃x : set, z = pair i x of type
set → set → prop.
L1494Axiom. (
tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
L1496Definition. We define
Pi to be
λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type
set → (set → set) → set.
Notation. We use
∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi.
L1501Axiom. (
PiI) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x
L1504Axiom. (
PiE) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (∀u ∈ f, pair_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)
L1507Axiom. (
PiEq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ Pi X Y ↔ (∀u ∈ f, pair_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)
L1510Axiom. (
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)
L1513Axiom. (
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
L1515Axiom. (
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
L1517Axiom. (
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
L1519Axiom. (
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
L1521Definition. We define
setexp to be
λX Y : set ⇒ ∏y ∈ Y, X of type
set → set → set.
Notation. We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp.
L1528Axiom. (
lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
L1530Axiom. (
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)
L1532Axiom. (
tuple_2_inj) We take the following as an axiom:
∀x y w z : set, (x,y) = (w,z) → x = w ∧ y = z
Beginning of Section Tuples
L1536Variable x0 x1 : set
End of Section Tuples
L1543Definition. We define
Sep2 to be
λX Y R ⇒ {u ∈ ∑x ∈ X, Y x|R (u 0) (u 1)} of type
set → (set → set) → (set → set → prop) → set.
L1546Axiom. (
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
L1549Axiom. (
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
L1552Axiom. (
Sep2E') 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 ∧ y ∈ Y x ∧ R x y
L1555Axiom. (
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
L1558Axiom. (
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
L1561Axiom. (
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
L1564Definition. We define
set_of_pairs to be
λX ⇒ ∀x ∈ X, ∃y z, x = (y,z) of type
set → prop.
L1574Axiom. (
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'
L1578Axiom. (
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)
L1580Axiom. (
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)
L1582Axiom. (
lam_eta) We take the following as an axiom:
∀X, ∀F : set → set, (λx ∈ X ⇒ (λx ∈ X ⇒ F x) x) = (λx ∈ X ⇒ F x)
L1584Axiom. (
tuple_2_eta) We take the following as an axiom:
L1586Definition. We define
lam2 to be
λX Y F ⇒ λx ∈ X ⇒ λy ∈ Y x ⇒ F x y of type
set → (set → set) → (set → set → set) → set.
L1589Axiom. (
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
L1591Axiom. (
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
L1595Definition. We define
encode_u to be
lam of type
set → (set → set) → set.
L1597Definition. We define
decode_u to be
ap of type
set → set → set.
L1598Definition. We define
encode_b to be
λX F ⇒ lam2 X (λ_ ⇒ X) F of type
set → (set → set → set) → set.
L1600Definition. We define
decode_b to be
λF x y ⇒ F x y of type
set → set → set → set.
L1601Definition. We define
encode_p to be
λX P ⇒ Sep X P of type
set → (set → prop) → set.
L1603Definition. We define
decode_p to be
λP x ⇒ x ∈ P of type
set → set → prop.
L1604Definition. We define
encode_r to be
λX R ⇒ Sep2 X (λ_ ⇒ X) R of type
set → (set → set → prop) → set.
L1606Definition. We define
decode_r to be
λR x y ⇒ (x,y) ∈ R of type
set → set → set → prop.
L1607Definition. We define
encode_c to be
λX C ⇒ Sep (𝒫 X) (λU ⇒ (C (λx ⇒ x ∈ U))) of type
set → ((set → prop) → prop) → set.
L1609Definition. We define
decode_c to be
λC U ⇒ ∃V, (∀x, U x ↔ x ∈ V) ∧ V ∈ C of type
set → (set → prop) → prop.
L1628Axiom. (
encode_c_ext) We take the following as an axiom:
∀X, ∀C C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → encode_c X C = encode_c X C'
L1630Axiom. (
setprod_mon) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ Y ⨯ W
L1632Axiom. (
setprod_mon0) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z : set, X ⨯ Z ⊆ Y ⨯ Z
L1634Axiom. (
setprod_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ X ⨯ W
L1638Axiom. (
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
L1640Axiom. (
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}
L1646Axiom. (
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
L1648Axiom. (
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
L1651Axiom. (
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
L1653Axiom. (
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
L1657Axiom. (
setexp_2_eq) We take the following as an axiom:
L1659Axiom. (
setexp_0_dom_mon) We take the following as an axiom:
∀A : set, 0 ∈ A → ∀X Y : set, X ⊆ Y → AX ⊆ AY
L1661Axiom. (
setexp_0_mon) We take the following as an axiom:
∀X Y A B : set, 0 ∈ B → A ⊆ B → X ⊆ Y → AX ⊆ BY
L1665Axiom. (
tupleI0) We take the following as an axiom:
L1667Axiom. (
tupleI1) We take the following as an axiom:
L1669Axiom. (
tupleE) We take the following as an axiom:
L1671Axiom. (
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
L1673Axiom. (
tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
L1675Axiom. (
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
L1677Axiom. (
apI2) We take the following as an axiom:
∀f x y, (x,y) ∈ f → y ∈ f x
L1679Axiom. (
apE2) We take the following as an axiom:
∀f x y, y ∈ f x → (x,y) ∈ f
L1681Axiom. (
ap_const_0) We take the following as an axiom:
L1687Axiom. (
tuple_3_eta) We take the following as an axiom:
L1689Axiom. (
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)
Beginning of Section Tuples
L1693Variable x0 x1 x2 : set
L1724Axiom. (
tuple_6_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 0 = x0
L1725Axiom. (
tuple_6_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 1 = x1
L1727Axiom. (
tuple_6_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 2 = x2
L1729Axiom. (
tuple_6_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 3 = x3
L1731Axiom. (
tuple_6_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 4 = x4
L1733Axiom. (
tuple_6_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5) 5 = x5
L1737Axiom. (
tuple_7_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 0 = x0
L1738Axiom. (
tuple_7_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 1 = x1
L1740Axiom. (
tuple_7_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 2 = x2
L1742Axiom. (
tuple_7_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 3 = x3
L1744Axiom. (
tuple_7_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 4 = x4
L1746Axiom. (
tuple_7_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 5 = x5
L1748Axiom. (
tuple_7_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6) 6 = x6
L1752Axiom. (
tuple_8_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 0 = x0
L1754Axiom. (
tuple_8_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 1 = x1
L1756Axiom. (
tuple_8_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 2 = x2
L1758Axiom. (
tuple_8_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 3 = x3
L1760Axiom. (
tuple_8_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 4 = x4
L1762Axiom. (
tuple_8_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 5 = x5
L1764Axiom. (
tuple_8_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 6 = x6
L1766Axiom. (
tuple_8_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7) 7 = x7
L1770Axiom. (
tuple_9_0_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 0 = x0
L1771Axiom. (
tuple_9_1_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 1 = x1
L1773Axiom. (
tuple_9_2_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 2 = x2
L1775Axiom. (
tuple_9_3_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 3 = x3
L1777Axiom. (
tuple_9_4_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 4 = x4
L1779Axiom. (
tuple_9_5_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 5 = x5
L1781Axiom. (
tuple_9_6_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 6 = x6
L1783Axiom. (
tuple_9_7_eq) We take the following as an axiom:
(x0,x1,x2,x3,x4,x5,x6,x7,x8) 7 = x7
L1785Axiom. (
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
End of Section pair_setsum
Notation. We use
∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma.
Notation. We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod.
Notation. We use
∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi.
Notation. We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp.
L1803Axiom. (
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
L1805Axiom. (
tuple_3_bij_3) We take the following as an axiom:
∀x y z, x ∈ 3 → y ∈ 3 → z ∈ 3 → x ≠ y → x ≠ z → y ≠ z → bij 3 3 (λi ⇒ (x,y,z) i)
L1807Axiom. (
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
L1809Axiom. (
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)
L1811Axiom. (
iff_refl) We take the following as an axiom:
L1813Axiom. (
iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
L1815Axiom. (
iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
L1825Axiom. (
eq_or_nand) We take the following as an axiom:
Primitive. The name
EpsR_i_i_1 is a term of type
(set → set → prop) → set.
Primitive. The name
EpsR_i_i_2 is a term of type
(set → set → prop) → set.
L1833Axiom. (
EpsR_i_i_12) We take the following as an axiom:
Primitive. The name
DescrR_i_io_1 is a term of type
(set → (set → prop) → prop) → set.
Primitive. The name
DescrR_i_io_2 is a term of type
(set → (set → prop) → prop) → set → prop.
L1843Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type
set → (set → prop) → (set → prop) → prop.
L1850Axiom. (
PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
L1852Axiom. (
PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
L1854Axiom. (
PNoEq_tra_) We take the following as an axiom:
L1858Definition. We define
PNoLt_ to be
λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type
set → (set → prop) → (set → prop) → prop.
L1861Axiom. (
PNoLt_E_) We take the following as an axiom:
L1864Axiom. (
PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
L1866Axiom. (
PNoLt_mon_) We take the following as an axiom:
L1871Axiom. (
PNoLt_tra_) We take the following as an axiom:
Primitive. The name
PNoLt is a term of type
set → (set → prop) → set → (set → prop) → prop.
L1876Axiom. (
PNoLtI1) We take the following as an axiom:
L1879Axiom. (
PNoLtI2) We take the following as an axiom:
L1882Axiom. (
PNoLtI3) We take the following as an axiom:
L1885Axiom. (
PNoLtE) We take the following as an axiom:
L1893Axiom. (
PNoLtE2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoLt alpha p alpha q → PNoLt_ alpha p q
L1896Axiom. (
PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
L1902Axiom. (
PNoLtEq_tra) We take the following as an axiom:
L1904Axiom. (
PNoEqLt_tra) We take the following as an axiom:
L1906Axiom. (
PNoLt_tra) We take the following as an axiom:
L1908Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop) → set → (set → prop) → prop.
L1911Axiom. (
PNoLeI1) We take the following as an axiom:
L1914Axiom. (
PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
L1917Axiom. (
PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
L1923Axiom. (
PNoLtLe_tra) We take the following as an axiom:
L1925Axiom. (
PNoLeLt_tra) We take the following as an axiom:
L1927Axiom. (
PNoEqLe_tra) We take the following as an axiom:
L1929Axiom. (
PNoLeEq_tra) We take the following as an axiom:
L1931Axiom. (
PNoLe_tra) We take the following as an axiom:
L1933Definition. We define
PNo_downc to be
λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
L1936Definition. We define
PNo_upc to be
λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
L1939Axiom. (
PNoLe_downc) We take the following as an axiom:
L1943Axiom. (
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
L1945Axiom. (
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
L1947Axiom. (
PNoLe_upc) We take the following as an axiom:
L1951Definition. 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.
L1994Axiom. (
PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
L1996Axiom. (
PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
L2004Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop, L beta p → beta ∈ alpha of type
set → (set → (set → prop) → prop) → prop.
L2096Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
Primitive. The name
PNo_bd is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
Primitive. The name
PNo_pred is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
L2128Axiom. (
PNo_bd_pred) We take the following as an axiom:
L2135Axiom. (
PNo_bd_ord) We take the following as an axiom:
L2157Axiom. (
PNo_bd_In) We take the following as an axiom:
L2164Definition. We define
PNoCutL to be
λalpha p beta q ⇒ beta ∈ alpha ∧ PNoLt beta q alpha p of type
set → (set → prop) → set → (set → prop) → prop.
L2167Definition. We define
PNoCutR to be
λalpha p beta q ⇒ beta ∈ alpha ∧ PNoLt alpha p beta q of type
set → (set → prop) → set → (set → prop) → prop.
Beginning of Section TaggedSets
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L2202Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type
set → set.
L2204Axiom. (
SNoElts_mon) We take the following as an axiom:
L2213Axiom. (
PNoEq_PSNo) We take the following as an axiom:
L2215Axiom. (
SNo_PSNo) We take the following as an axiom:
Primitive. The name
SNo is a term of type
set → prop.
L2222Axiom. (
SNo_SNo) We take the following as an axiom:
Primitive. The name
SNoLev is a term of type
set → set.
L2229Axiom. (
SNoLev_uniq) We take the following as an axiom:
L2231Axiom. (
SNoLev_prop) We take the following as an axiom:
L2235Axiom. (
SNoLev_) We take the following as an axiom:
L2239Axiom. (
SNoLev_PSNo) We take the following as an axiom:
L2241Axiom. (
SNo_Subq) We take the following as an axiom:
L2243Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type
set → set → set → prop.
L2246Axiom. (
SNoEq_I) We take the following as an axiom:
L2248Axiom. (
SNoEq_E) We take the following as an axiom:
L2250Axiom. (
SNoEq_E1) We take the following as an axiom:
L2252Axiom. (
SNoEq_E2) We take the following as an axiom:
L2256Axiom. (
SNo_eq) We take the following as an axiom:
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
L2269Definition. We define
SNo_pair to be
λx y ⇒ x ∪ {u ''|u ∈ y} of type
set → set → set.
L2275Axiom. (
SNo_pair_0) We take the following as an axiom:
End of Section TaggedSets
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
L2289Axiom. (
SNoLtLe) We take the following as an axiom:
L2291Axiom. (
SNoLeE) We take the following as an axiom:
L2293Axiom. (
SNoEq_ref_) We take the following as an axiom:
L2295Axiom. (
SNoEq_sym_) We take the following as an axiom:
L2297Axiom. (
SNoEq_tra_) We take the following as an axiom:
L2299Axiom. (
SNoLtE) We take the following as an axiom:
L2306Axiom. (
SNoLtI2) We take the following as an axiom:
L2314Axiom. (
SNoLtI3) We take the following as an axiom:
L2320Axiom. (
SNoLt_irref) We take the following as an axiom:
L2330Axiom. (
SNoLt_tra) We take the following as an axiom:
L2332Axiom. (
SNoLe_ref) We take the following as an axiom:
L2336Axiom. (
SNoLtLe_tra) We take the following as an axiom:
L2338Axiom. (
SNoLeLt_tra) We take the following as an axiom:
L2340Axiom. (
SNoLe_tra) We take the following as an axiom:
L2342Axiom. (
SNoLtLe_or) We take the following as an axiom:
L2355Definition. We define
SNoCutP to be
λL R ⇒ (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y) of type
set → set → prop.
L2378Axiom. (
SNoCutP_L_0) We take the following as an axiom:
L2380Axiom. (
SNoCutP_0_R) We take the following as an axiom:
L2381Axiom. (
SNoCutP_0_0) We take the following as an axiom:
L2382Axiom. (
SNoCut_0_0) We take the following as an axiom:
L2389Axiom. (
SNoS_E) We take the following as an axiom:
Beginning of Section TaggedSets2
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L2396Axiom. (
SNoS_I) We take the following as an axiom:
L2398Axiom. (
SNoS_I2) We take the following as an axiom:
L2400Axiom. (
SNoS_Subq) We take the following as an axiom:
L2404Axiom. (
SNoS_E2) We take the following as an axiom:
L2409Axiom. (
SNoS_In_neq) We take the following as an axiom:
L2411Axiom. (
SNoS_SNoLev) We take the following as an axiom:
L2418Axiom. (
SNoL_E) We take the following as an axiom:
L2423Axiom. (
SNoR_E) We take the following as an axiom:
L2428Axiom. (
SNoL_SNoS) We take the following as an axiom:
L2430Axiom. (
SNoR_SNoS) We take the following as an axiom:
L2431Axiom. (
SNoL_SNoS_) We take the following as an axiom:
L2432Axiom. (
SNoR_SNoS_) We take the following as an axiom:
L2433Axiom. (
SNoL_I) We take the following as an axiom:
L2435Axiom. (
SNoR_I) We take the following as an axiom:
L2437Axiom. (
SNo_eta) We take the following as an axiom:
L2452Axiom. (
SNoCut_Le) We take the following as an axiom:
L2457Axiom. (
SNoCut_ext) We take the following as an axiom:
L2489Axiom. (
SNo_0) We take the following as an axiom:
L2491Axiom. (
SNoLev_0) We take the following as an axiom:
L2492Axiom. (
SNoL_0) We take the following as an axiom:
L2493Axiom. (
SNoR_0) We take the following as an axiom:
L2494Axiom. (
SNoL_1) We take the following as an axiom:
L2495Axiom. (
SNoR_1) We take the following as an axiom:
L2530Axiom. (
eps_0_1) We take the following as an axiom:
L2531Axiom. (
SNo__eps_) We take the following as an axiom:
L2532Axiom. (
SNo_eps_) We take the following as an axiom:
L2533Axiom. (
SNoLev_eps_) We take the following as an axiom:
L2536Axiom. (
SNo_eps_pos) We take the following as an axiom:
End of Section TaggedSets2
L2540Axiom. (
ordinal_SNo) We take the following as an axiom:
L2552Axiom. (
SNo_etaE) We take the following as an axiom:
L2561Axiom. (
SNo_ind) We take the following as an axiom:
∀P : set → prop, (∀L R, SNoCutP L R → (∀x ∈ L, P x) → (∀y ∈ R, P y) → P (SNoCut L R)) → ∀z, SNo z → P z
Beginning of Section SurrealRecI
L2572Variable F : set → (set → set) → set
Primitive. The name
SNo_rec_i is a term of type
set → set.
L2577Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecI
Beginning of Section SurrealRecII
L2587Variable F : set → (set → (set → set)) → (set → set)
Primitive. The name
SNo_rec_ii is a term of type
set → (set → set).
L2592Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecII
Beginning of Section SurrealRec2
L2602Variable F : set → set → (set → set → set) → set
Primitive. The name
SNo_rec2 is a term of type
set → set → set.
L2613Axiom. (
SNo_rec2_eq) We take the following as an axiom:
End of Section SurrealRec2
L2638Axiom. (
SNoLev_ind) We take the following as an axiom:
L2643Axiom. (
SNoLev_ind2) We take the following as an axiom:
L2651Axiom. (
SNoLev_ind3) We take the following as an axiom:
∀P : set → set → set → prop, (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), P u y z) → (∀v ∈ SNoS_ (SNoLev y), P x v z) → (∀w ∈ SNoS_ (SNoLev z), P x y w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w) → P x y z) → ∀x y z, SNo x → SNo y → SNo z → P x y z
L2663Axiom. (
SNo_1) We take the following as an axiom:
L2665Axiom. (
SNo_2) We take the following as an axiom:
L2666Axiom. (
SNo_omega) We take the following as an axiom:
L2667Axiom. (
SNoLt_0_1) We take the following as an axiom:
L2668Axiom. (
SNoLt_0_2) We take the following as an axiom:
L2669Axiom. (
SNoLt_1_2) We take the following as an axiom:
L2672Axiom. (
restr_SNo_) We take the following as an axiom:
L2673Axiom. (
restr_SNo) We take the following as an axiom:
L2675Axiom. (
restr_SNoEq) We take the following as an axiom:
Primitive. The name
pack_e is a term of type
set → set → set.
L2684Axiom. (
pack_e_0_eq) We take the following as an axiom:
L2688Axiom. (
pack_e_1_eq) We take the following as an axiom:
L2692Axiom. (
pack_e_inj) We take the following as an axiom:
L2694Definition. We define
struct_e to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀c : set, c ∈ X → q (pack_e X c)) → q S of type
set → prop.
Primitive. The name
unpack_e_i is a term of type
set → (set → set → set) → set.
Primitive. The name
unpack_e_o is a term of type
set → (set → set → prop) → prop.
Primitive. The name
pack_u is a term of type
set → (set → set) → set.
L2717Axiom. (
pack_u_0_eq) We take the following as an axiom:
∀S X, ∀F : set → set, S = pack_u X F → X = S 0
L2721Axiom. (
pack_u_1_eq) We take the following as an axiom:
L2725Axiom. (
pack_u_inj) We take the following as an axiom:
L2727Axiom. (
pack_u_ext) We take the following as an axiom:
L2731Definition. We define
struct_u to be
λS ⇒ ∀q : set → prop, (∀X, ∀F : set → set, (∀x ∈ X, F x ∈ X) → q (pack_u X F)) → q S of type
set → prop.
Primitive. The name
unpack_u_i is a term of type
set → (set → (set → set) → set) → set.
L2742Axiom. (
unpack_u_i_eq) We take the following as an axiom:
∀Phi : set → (set → set) → set, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_i (pack_u X F) Phi = Phi X F
Primitive. The name
unpack_u_o is a term of type
set → (set → (set → set) → prop) → prop.
L2751Axiom. (
unpack_u_o_eq) We take the following as an axiom:
∀Phi : set → (set → set) → prop, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_o (pack_u X F) Phi = Phi X F
Primitive. The name
pack_b is a term of type
set → (set → set → set) → set.
L2760Axiom. (
pack_b_0_eq) We take the following as an axiom:
∀S X, ∀F : set → set → set, S = pack_b X F → X = S 0
L2764Axiom. (
pack_b_1_eq) We take the following as an axiom:
L2768Axiom. (
pack_b_inj) We take the following as an axiom:
∀X X', ∀F F' : set → set → set, pack_b X F = pack_b X' F' → X = X' ∧ ∀x y ∈ X, F x y = F' x y
L2770Axiom. (
pack_b_ext) We take the following as an axiom:
∀X, ∀F F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → pack_b X F = pack_b X F'
L2774Definition. We define
struct_b to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀F : set → set → set, (∀x y ∈ X, F x y ∈ X) → q (pack_b X F)) → q S of type
set → prop.
Primitive. The name
unpack_b_i is a term of type
set → (set → (set → set → set) → set) → set.
L2785Axiom. (
unpack_b_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → set, ∀X, ∀F : set → set → set, (∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F) → unpack_b_i (pack_b X F) Phi = Phi X F
Primitive. The name
unpack_b_o is a term of type
set → (set → (set → set → set) → prop) → prop.
L2794Axiom. (
unpack_b_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → prop, ∀X, ∀F : set → set → set, (∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F) → unpack_b_o (pack_b X F) Phi = Phi X F
Primitive. The name
pack_p is a term of type
set → (set → prop) → set.
L2803Axiom. (
pack_p_0_eq) We take the following as an axiom:
∀S X, ∀P : set → prop, S = pack_p X P → X = S 0
L2807Axiom. (
pack_p_1_eq) We take the following as an axiom:
L2811Axiom. (
pack_p_inj) We take the following as an axiom:
L2813Axiom. (
pack_p_ext) We take the following as an axiom:
L2817Definition. We define
struct_p to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀P : set → prop, q (pack_p X P)) → q S of type
set → prop.
Primitive. The name
unpack_p_i is a term of type
set → (set → (set → prop) → set) → set.
L2826Axiom. (
unpack_p_i_eq) We take the following as an axiom:
∀Phi : set → (set → prop) → set, ∀X, ∀P : set → prop, (∀P' : set → prop, (∀x ∈ X, P x ↔ P' x) → Phi X P' = Phi X P) → unpack_p_i (pack_p X P) Phi = Phi X P
Primitive. The name
unpack_p_o is a term of type
set → (set → (set → prop) → prop) → prop.
L2835Axiom. (
unpack_p_o_eq) We take the following as an axiom:
∀Phi : set → (set → prop) → prop, ∀X, ∀P : set → prop, (∀P' : set → prop, (∀x ∈ X, P x ↔ P' x) → Phi X P' = Phi X P) → unpack_p_o (pack_p X P) Phi = Phi X P
Primitive. The name
pack_r is a term of type
set → (set → set → prop) → set.
L2844Axiom. (
pack_r_0_eq) We take the following as an axiom:
∀S X, ∀R : set → set → prop, S = pack_r X R → X = S 0
L2846Axiom. (
pack_r_0_eq2) We take the following as an axiom:
∀X, ∀R : set → set → prop, X = pack_r X R 0
L2848Axiom. (
pack_r_1_eq) We take the following as an axiom:
L2852Axiom. (
pack_r_inj) We take the following as an axiom:
∀X X', ∀R R' : set → set → prop, pack_r X R = pack_r X' R' → X = X' ∧ ∀x y ∈ X, R x y = R' x y
L2854Axiom. (
pack_r_ext) We take the following as an axiom:
∀X, ∀R R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → pack_r X R = pack_r X R'
L2858Definition. We define
struct_r to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀R : set → set → prop, q (pack_r X R)) → q S of type
set → prop.
Primitive. The name
unpack_r_i is a term of type
set → (set → (set → set → prop) → set) → set.
L2867Axiom. (
unpack_r_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → prop) → set, ∀X, ∀R : set → set → prop, (∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X R' = Phi X R) → unpack_r_i (pack_r X R) Phi = Phi X R
Primitive. The name
unpack_r_o is a term of type
set → (set → (set → set → prop) → prop) → prop.
L2876Axiom. (
unpack_r_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → prop) → prop, ∀X, ∀R : set → set → prop, (∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X R' = Phi X R) → unpack_r_o (pack_r X R) Phi = Phi X R
Primitive. The name
pack_c is a term of type
set → ((set → prop) → prop) → set.
L2885Axiom. (
pack_c_0_eq) We take the following as an axiom:
∀S X, ∀C : (set → prop) → prop, S = pack_c X C → X = S 0
L2887Axiom. (
pack_c_0_eq2) We take the following as an axiom:
∀X, ∀C : (set → prop) → prop, X = pack_c X C 0
L2889Axiom. (
pack_c_1_eq) We take the following as an axiom:
∀S X, ∀C : (set → prop) → prop, S = pack_c X C → ∀U : set → prop, (∀x, U x → x ∈ X) → C U = decode_c (S 1) U
L2891Axiom. (
pack_c_1_eq2) We take the following as an axiom:
∀X, ∀C : (set → prop) → prop, ∀U : set → prop, (∀x, U x → x ∈ X) → C U = decode_c (pack_c X C 1) U
L2893Axiom. (
pack_c_inj) We take the following as an axiom:
∀X X', ∀C C' : (set → prop) → prop, pack_c X C = pack_c X' C' → X = X' ∧ ∀U : set → prop, (∀x, U x → x ∈ X) → C U = C' U
L2895Axiom. (
pack_c_ext) We take the following as an axiom:
∀X, ∀C C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → pack_c X C = pack_c X C'
L2899Definition. We define
struct_c to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀C : (set → prop) → prop, q (pack_c X C)) → q S of type
set → prop.
Primitive. The name
unpack_c_i is a term of type
set → (set → ((set → prop) → prop) → set) → set.
L2908Axiom. (
unpack_c_i_eq) We take the following as an axiom:
∀Phi : set → ((set → prop) → prop) → set, ∀X, ∀C : (set → prop) → prop, (∀C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → Phi X C' = Phi X C) → unpack_c_i (pack_c X C) Phi = Phi X C
Primitive. The name
unpack_c_o is a term of type
set → (set → ((set → prop) → prop) → prop) → prop.
L2917Axiom. (
unpack_c_o_eq) We take the following as an axiom:
∀Phi : set → ((set → prop) → prop) → prop, ∀X, ∀C : (set → prop) → prop, (∀C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → Phi X C' = Phi X C) → unpack_c_o (pack_c X C) Phi = Phi X C
Primitive. The name
canonical_elt is a term of type
(set → set → prop) → set → set.
Primitive. The name
quotient is a term of type
(set → set → prop) → set → prop.
L2932Axiom. (
quotient_prop1) We take the following as an axiom:
∀R : set → set → prop, ∀x : set, quotient R x → R x x
Primitive. The name
canonical_elt_def is a term of type
(set → set → prop) → (set → set) → set → set.
Primitive. The name
quotient_def is a term of type
(set → set → prop) → (set → set) → set → prop.
Beginning of Section explicit_Nats
L2973Variable S : set → set
L2977Axiom. (
explicit_Nats_I) We take the following as an axiom:
(base ∈ N) → (∀m ∈ N, S m ∈ N) → (∀m ∈ N, S m ≠ base) → (∀m n ∈ N, S m = S n → m = n) → (∀p : set → prop, p base → (∀m, p m → p (S m)) → (∀m ∈ N, p m)) → explicit_Nats
L2985Axiom. (
explicit_Nats_E) We take the following as an axiom:
∀q : prop, (explicit_Nats → (base ∈ N) → (∀m ∈ N, S m ∈ N) → (∀m ∈ N, S m ≠ base) → (∀m n ∈ N, S m = S n → m = n) → (∀p : set → prop, p base → (∀m, p m → p (S m)) → (∀m ∈ N, p m)) → q) → explicit_Nats → q
End of Section explicit_Nats
Beginning of Section explicit_Nats_zero
L3025Variable S : set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
explicit_Nats_zero_plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
explicit_Nats_zero_mult.
End of Section explicit_Nats_zero
Beginning of Section explicit_Nats_one
L3052Variable S : set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
explicit_Nats_one_plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
explicit_Nats_one_mult.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
explicit_Nats_one_exp.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
explicit_Nats_one_lt.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
explicit_Nats_one_le.
End of Section explicit_Nats_one
Beginning of Section explicit_Nats_transfer
L3095Variable S : set → set
L3097Variable base' : set
L3098Variable S' : set → set
L3099Variable f : set → set
End of Section explicit_Nats_transfer
Beginning of Section AssocComm
L3109Variable plus : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
L3112Axiom. (
AssocComm_identities) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → ∀p : prop, ((∀x y z ∈ R, x + y + z = y + x + z) → (∀x y z ∈ R, x + y + z = z + x + y) → (∀x y z w ∈ R, (x + y) + (z + w) = (x + z) + (y + w)) → (∀x y z w ∈ R, x + y + z + w = w + x + y + z) → (∀x y z w ∈ R, x + y + z + w = z + w + x + y) → p) → p
End of Section AssocComm
Beginning of Section Group1
Beginning of Section Group1Explicit
L3133Variable op : set → set → set
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
L3136Definition. We define
explicit_Group to be
(∀a b ∈ G, a * b ∈ G) ∧ (∀a b c ∈ G, a * (b * c) = (a * b) * c) ∧ ∃e ∈ G, (∀a ∈ G, e * a = a ∧ a * e = a) ∧ (∀a ∈ G, ∃b ∈ G, a * b = e ∧ b * a = e) of type
prop.
Notation. We use
- as a postfix operator with priority 340 corresponding to applying term
explicit_Group_inverse.
End of Section Group1Explicit
Beginning of Section Group1Explicit2
L3189Variable op : set → set → set
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
Beginning of Section Group1Explicit2RepIndep
L3194Variable op' : set → set → set
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
op'.
L3197Hypothesis Hopop' : ∀a b ∈ G, a * b = a ⨯ b
End of Section Group1Explicit2RepIndep
End of Section Group1Explicit2
Beginning of Section Group1Explicit3RepIndep
L3223Variable op : set → set → set
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
L3226Variable op' : set → set → set
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
op'.
L3229Hypothesis Hopop' : ∀a b ∈ G, a * b = a ⨯ b
End of Section Group1Explicit3RepIndep
End of Section Group1
L3248Axiom. (
GroupI) We take the following as an axiom:
L3250Axiom. (
GroupE) We take the following as an axiom:
Beginning of Section Group2
L3261Variable op : set → set → set
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
Notation. We use
- as a postfix operator with priority 340 corresponding to applying term
explicit_Group_inverse G op.
End of Section Group2
Beginning of Section Group3
L3291Variable op op' : set → set → set
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
Notation. We use
- as a postfix operator with priority 340 corresponding to applying term
explicit_Group_inverse G op.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
op'.
Notation. We use
:-: as a postfix operator with priority 340 corresponding to applying term
explicit_Group_inverse G op'.
L3299Hypothesis Hopop' : ∀a b ∈ G, a * b = a ⨯ b
End of Section Group3
Notation. We use
≤ as an infix operator with priority 400 and no associativity corresponding to applying term
subgroup.
L3335Axiom. (
subgroup_E) We take the following as an axiom:
∀H G, H ≤ G → ∀q : set → set → prop, (∀H G, ∀op : set → set → set, (∀a b ∈ G, op a b ∈ G) → Group (pack_b H op) → H ⊆ G → q (pack_b H op) (pack_b G op)) → q H G
Beginning of Section Group4
L3351Let G ≝ {f ∈ AA|bij A A (λx ⇒ f x)}
L3353Let op ≝ λf g : set ⇒ λx ∈ A ⇒ g (f x)
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
op.
L3365Let H ≝ {f ∈ AA|bij A A (λx ⇒ f x) ∧ ∀x ∈ B, f x = x}
End of Section Group4
L3371Definition. We define
symgroup to be
λA ⇒ pack_b {f ∈ AA|bij A A (λx ⇒ f x)} (λf g ⇒ λx ∈ A ⇒ g (f x)) of type
set → set.
L3410Definition. We define
Group_carrier to be
λGs ⇒ Gs 0 of type
set → set.
L3412Definition. We define
Group_op to be
λGs ⇒ decode_b (Gs 1) of type
set → set → set → set.
Beginning of Section Group2
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
Group_op Gs.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
Group_op Gs'.
End of Section Group2
Beginning of Section explicit_Rng
L3442Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3449Axiom. (
explicit_Rng_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → explicit_Rng
L3461Axiom. (
explicit_Rng_E) We take the following as an axiom:
∀q : prop, (explicit_Rng → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → q) → explicit_Rng → q
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Rng_minus.
End of Section explicit_Rng
Beginning of Section explicit_Ring
L3501Variable zero one : set
L3503Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3510Axiom. (
explicit_Ring_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x * one = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → explicit_Ring
L3526Axiom. (
explicit_Ring_E) We take the following as an axiom:
∀q : prop, (explicit_Ring → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x * one = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → q) → explicit_Ring → q
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Rng_minus R zero plus mult.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
explicit_Ring_exp_nat.
End of Section explicit_Ring
Beginning of Section explicit_Ring_RepIndep2
L3590Variable zero one : set
L3592Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3596Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 355 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L3600Hypothesis Hpp' : ∀a b ∈ R, a + b = a + b
L3602Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_Ring_RepIndep2
Beginning of Section explicit_CRing
L3611Variable zero one : set
L3613Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3620Axiom. (
explicit_CRing_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → explicit_CRing
L3635Axiom. (
explicit_CRing_E) We take the following as an axiom:
∀q : prop, (explicit_CRing → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → q) → explicit_CRing → q
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Rng_minus R zero plus mult.
End of Section explicit_CRing
Beginning of Section explicit_CRing_RepIndep2
L3690Variable zero one : set
L3692Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3696Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 355 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L3700Hypothesis Hpp' : ∀a b ∈ R, a + b = a + b
L3702Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_CRing_RepIndep2
Primitive. The name
pack_b_b_e is a term of type
set → (set → set → set) → (set → set → set) → set → set.
L3710Definition. We define
struct_b_b_e to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀f : set → set → set, (∀x y ∈ X, f x y ∈ X) → ∀g : set → set → set, (∀x y ∈ X, g x y ∈ X) → ∀c : set, c ∈ X → q (pack_b_b_e X f g c)) → q S of type
set → prop.
Primitive. The name
unpack_b_b_e_i is a term of type
set → (set → (set → set → set) → (set → set → set) → set → set) → set.
Primitive. The name
unpack_b_b_e_o is a term of type
set → (set → (set → set → set) → (set → set → set) → set → prop) → prop.
L3718Axiom. (
unpack_b_b_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀c : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → Phi X f' g' c = Phi X f g c) → unpack_b_b_e_o (pack_b_b_e X f g c) Phi = Phi X f g c
Primitive. The name
pack_b_b_e_e is a term of type
set → (set → set → set) → (set → set → set) → set → set → set.
L3736Definition. We define
struct_b_b_e_e to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀f : set → set → set, (∀x y ∈ X, f x y ∈ X) → ∀g : set → set → set, (∀x y ∈ X, g x y ∈ X) → ∀c : set, c ∈ X → ∀d : set, d ∈ X → q (pack_b_b_e_e X f g c d)) → q S of type
set → prop.
Primitive. The name
unpack_b_b_e_e_i is a term of type
set → (set → (set → set → set) → (set → set → set) → set → set → set) → set.
Primitive. The name
unpack_b_b_e_e_o is a term of type
set → (set → (set → set → set) → (set → set → set) → set → set → prop) → prop.
L3744Axiom. (
unpack_b_b_e_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → set → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → Phi X f' g' c d = Phi X f g c d) → unpack_b_b_e_e_o (pack_b_b_e_e X f g c d) Phi = Phi X f g c d
Beginning of Section explicit_Reals
L3778Variable zero one : set
L3780Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L3787Axiom. (
explicit_Field_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x ≠ zero → ∃y ∈ R, x * y = one) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → explicit_Field
L3803Axiom. (
explicit_Field_E) We take the following as an axiom:
∀q : prop, (explicit_Field → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x ≠ zero → ∃y ∈ R, x * y = one) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → q) → explicit_Field → q
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Field_minus.
L3849Variable leq : set → set → prop
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
leq.
L3887Definition. We define
lt to be
λx y ⇒ x ≤ y ∧ x ≠ y of type
set → set → prop.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
lt.
L3895Let Npos ≝ {n ∈ N|n ≠ zero}
End of Section explicit_Reals
L3969Definition. We define
CRing_carrier to be
λRs ⇒ Rs 0 of type
set → set.
L3973Definition. We define
CRing_zero to be
λRs ⇒ Rs 3 of type
set → set.
L3974Definition. We define
CRing_one to be
λRs ⇒ Rs 4 of type
set → set.
Beginning of Section CRing
L3979Hypothesis HRs : CRing Rs
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
CRing_plus Rs.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
CRing_mult Rs.
L3986Axiom. (
CRing_eta) We take the following as an axiom:
L4000Axiom. (
CRing_one_L) We take the following as an axiom:
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
CRing_omega_exp.
End of Section CRing
Beginning of Section explicit_Reals
L4024Variable zero one : set
L4026Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Field_minus R zero one plus mult.
L4032Variable leq : set → set → prop
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
leq.
L4038Let Npos ≝ {n ∈ N|n ≠ zero}
Beginning of Section explicit_Reals_Q_min_props
L4072Let Npos' ≝ {n ∈ N'|n ≠ zero}
End of Section explicit_Reals_Q_min_props
End of Section explicit_Reals
Beginning of Section explicit_Field_transfer
L4099Variable zero one : set
L4101Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L4107Variable zero' one' : set
L4109Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L4113Variable f : set → set
End of Section explicit_Field_transfer
Beginning of Section explicit_Field_RepIndep2
L4129Variable zero one : set
L4131Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L4135Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 355 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L4139Hypothesis Hpp' : ∀a b ∈ R, a + b = a + b
L4141Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_Field_RepIndep2
Beginning of Section explicit_OrderedField_transfer
L4158Variable zero one : set
L4160Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L4164Variable leq : set → set → prop
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
leq.
L4171Variable zero' one' : set
L4173Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L4177Variable leq' : set → set → prop
L4179Variable f : set → set
End of Section explicit_OrderedField_transfer
L4192Definition. We define
Field_carrier to be
λFs ⇒ Fs 0 of type
set → set.
L4196Definition. We define
Field_zero to be
λFs ⇒ Fs 3 of type
set → set.
L4197Definition. We define
Field_one to be
λFs ⇒ Fs 4 of type
set → set.
Primitive. The name
Field_minus is a term of type
set → set → set.
Beginning of Section Field
L4205Hypothesis HFs : Field Fs
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
Field_plus Fs.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
Field_mult Fs.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
Field_minus Fs.
L4213Axiom. (
Field_eta) We take the following as an axiom:
L4227Axiom. (
Field_one_L) We take the following as an axiom:
Primitive. The name
Field_div is a term of type
set → set → set.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
Field_div.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
CRing_omega_exp Fs.
L4266Axiom. (
Field_dist_R) We take the following as an axiom:
∀x y z ∈ F, (x + y) * z = x * z + y * z
End of Section Field
Beginning of Section Field2
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
Field_plus Fs.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
Field_mult Fs.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
Field_plus Fs'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
Field_mult Fs'.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
Field_minus Fs.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
Field_minus Fs'.
Primitive. The name
subfield is a term of type
prop.
L4296Axiom. (
subfield_I) We take the following as an axiom:
L4302Axiom. (
subfield_E) We take the following as an axiom:
subfield → ∀p : prop, (Field Fs → Field Fs' → F ⊆ F' → zero = zero' → one = one' → (∀a b ∈ F, a + b = a + b) → (∀a b ∈ F, a * b = a ⨯ b) → p) → p
Primitive. The name
Field_Hom is a term of type
set → prop.
L4312Axiom. (
Field_Hom_I) We take the following as an axiom:
∀g, Field Fs → Field Fs' → g ∈ F'F → g zero = zero' → g one = one' → (∀a b ∈ F, g (a + b) = g a + g b) → (∀a b ∈ F, g (a * b) = g a ⨯ g b) → Field_Hom g
L4321Axiom. (
Field_Hom_E) We take the following as an axiom:
End of Section Field2
L4367Axiom. (
radical_field_extension_E) We take the following as an axiom:
∀Fs Fs', radical_field_extension Fs Fs' → ∀p : prop, (Field Fs → Field Fs' → subfield Fs Fs' → ∀r ∈ omega, ∀Fseq, Fseq 0 = Fs → Fseq r = Fs' → (∀i ∈ ordsucc r, Field (Fseq i)) → (∀i ∈ ordsucc r, ∀j ∈ ordsucc i, subfield (Fseq j) (Fseq i)) → (∀i ∈ r, ∃a ∈ Field_carrier (Fseq (ordsucc i)), ∃n ∈ omega, CRing_omega_exp (Fseq (ordsucc i)) a n ∈ Field_carrier (Fseq i) ∧ Field_extension_by_1 (Fseq i) (Fseq (ordsucc i)) a) → p) → p
L4396Definition. We define
lam_comp to be
λA f g ⇒ λx ∈ A ⇒ f (g x) of type
set → set → set → set.
L4398Definition. We define
lam_id to be
λA ⇒ λx ∈ A ⇒ x of type
set → set.
Beginning of Section explicit_Reals_transfer
L4417Variable zero one : set
L4419Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L4423Variable leq : set → set → prop
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
leq.
L4430Variable zero' one' : set
L4432Variable plus' mult' : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L4436Variable leq' : set → set → prop
L4438Variable f : set → set
End of Section explicit_Reals_transfer
Beginning of Section explicit_Complex
L4455Variable Re Im : set → set
L4457Variable zero one i : set
L4458Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
End of Section explicit_Complex
Beginning of Section RealsToComplex
L4484Variable zero one : set
L4486Variable plus mult : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
explicit_Field_minus R zero one plus mult.
L4492Variable leq : set → set → prop
L4494Variable pa : set → set → set
L4498Let Re : set → set ≝ λz ⇒ Eps_i (λx ⇒ x ∈ R ∧ ∃y ∈ R, z = pa x y)
L4500Let Im : set → set ≝ λz ⇒ Eps_i (λy ⇒ y ∈ R ∧ z = pa (Re z) y)
L4501Let Re' : set → set ≝ λz ⇒ pa (Re z) zero
L4502Let Im' : set → set ≝ λz ⇒ pa (Im z) zero
L4503Let R' ≝ {z ∈ C|Re' z = z}
L4505Let zero' : set ≝ pa zero zero
L4507Let one' : set ≝ pa one zero
L4508Let i' : set ≝ pa zero one
L4509Let plus' : set → set → set ≝ λz w ⇒ pa (Re z + Re w) (Im z + Im w)
L4510Let mult' : set → set → set ≝ λz w ⇒ pa (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w)
End of Section RealsToComplex
Beginning of Section SurrealArithmetic
Primitive. The name
minus_SNo is a term of type
set → set.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
L4558Axiom. (
minus_SNo_0) We take the following as an axiom:
L4559Axiom. (
SNo_momega) We take the following as an axiom:
Primitive. The name
add_SNo is a term of type
set → set → set.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
L4571Axiom. (
add_SNo_eq) We take the following as an axiom:
L4582Axiom. (
SNo_add_SNo) We take the following as an axiom:
L4586Axiom. (
add_SNo_Lt1) We take the following as an axiom:
L4588Axiom. (
add_SNo_Le1) We take the following as an axiom:
L4590Axiom. (
add_SNo_Lt2) We take the following as an axiom:
L4592Axiom. (
add_SNo_Le2) We take the following as an axiom:
L4598Axiom. (
add_SNo_Lt3) We take the following as an axiom:
L4600Axiom. (
add_SNo_Le3) We take the following as an axiom:
L4608Axiom. (
add_SNo_com) We take the following as an axiom:
L4610Axiom. (
add_SNo_0L) We take the following as an axiom:
L4612Axiom. (
add_SNo_0R) We take the following as an axiom:
Primitive. The name
mul_SNo is a term of type
set → set → set.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
L4717Axiom. (
mul_SNo_eq) We take the following as an axiom:
L4726Axiom. (
mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
L4747Axiom. (
mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p
L4757Axiom. (
SNo_mul_SNo) We take the following as an axiom:
L4759Axiom. (
mul_SNo_eq_3) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
L4780Axiom. (
mul_SNo_Lt) We take the following as an axiom:
L4783Axiom. (
mul_SNo_Le) We take the following as an axiom:
L4810Axiom. (
mul_SNo_com) We take the following as an axiom:
L4843Axiom. (
real_I) We take the following as an axiom:
L4850Axiom. (
real_E) We take the following as an axiom:
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat.
End of Section SurrealArithmetic
L4888Axiom. (
CSNo_I) We take the following as an axiom:
L4890Axiom. (
CSNo_E) We take the following as an axiom:
L4894Axiom. (
SNo_CSNo) We take the following as an axiom:
Beginning of Section Complex
L4910Axiom. (
CSNo_Re1) We take the following as an axiom:
L4912Axiom. (
CSNo_Re2) We take the following as an axiom:
∀x y, SNo x → SNo y → Re (pa x y) = x
L4913Axiom. (
CSNo_Im1) We take the following as an axiom:
∀z, CSNo z → SNo (Im z) ∧ z = pa (Re z) (Im z)
L4914Axiom. (
CSNo_Im2) We take the following as an axiom:
∀x y, SNo x → SNo y → Im (pa x y) = y
L4915Axiom. (
CSNo_ReR) We take the following as an axiom:
L4916Axiom. (
CSNo_ImR) We take the following as an axiom:
L4917Axiom. (
CSNo_ReIm) We take the following as an axiom:
∀z, CSNo z → z = pa (Re z) (Im z)
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
L4923Definition. We define
minus_CSNo to be
λz ⇒ pa (- Re z) (- Im z) of type
set → set.
L4925Definition. We define
add_CSNo to be
λz w ⇒ pa (Re z + Re w) (Im z + Im w) of type
set → set → set.
L4926Definition. We define
mul_CSNo to be
λz w ⇒ pa (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w) of type
set → set → set.
L4930Axiom. (
SNo_Re) We take the following as an axiom:
L4932Axiom. (
SNo_Im) We take the following as an axiom:
L4934Axiom. (
Re_0) We take the following as an axiom:
L4936Axiom. (
Im_0) We take the following as an axiom:
L4938Axiom. (
Re_1) We take the following as an axiom:
L4940Axiom. (
Im_1) We take the following as an axiom:
L4942Axiom. (
Re_i) We take the following as an axiom:
L4944Axiom. (
Im_i) We take the following as an axiom:
L4950Axiom. (
add_CSNo_0L) We take the following as an axiom:
L4952Axiom. (
add_CSNo_0R) We take the following as an axiom:
End of Section Complex
Beginning of Section Complex
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_CSNo.
End of Section Complex
Beginning of Section Int
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
L4999Axiom. (
int_add_SNo) We take the following as an axiom:
L5000Axiom. (
int_mul_SNo) We take the following as an axiom:
End of Section Int
Primitive. The name
pack_b_b_r_e_e is a term of type
set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → set.
L5014Axiom. (
pack_b_b_r_e_e_0_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → X = S 0
L5016Axiom. (
pack_b_b_r_e_e_0_eq2) We take the following as an axiom:
∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, X = pack_b_b_r_e_e X f g R c d 0
L5018Axiom. (
pack_b_b_r_e_e_1_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → ∀x y ∈ X, f x y = decode_b (S 1) x y
L5022Axiom. (
pack_b_b_r_e_e_2_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → ∀x y ∈ X, g x y = decode_b (S 2) x y
L5026Axiom. (
pack_b_b_r_e_e_3_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → ∀x y ∈ X, R x y = decode_r (S 3) x y
L5030Axiom. (
pack_b_b_r_e_e_4_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → c = S 4
L5032Axiom. (
pack_b_b_r_e_e_4_eq2) We take the following as an axiom:
∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, c = pack_b_b_r_e_e X f g R c d 4
L5034Axiom. (
pack_b_b_r_e_e_5_eq) We take the following as an axiom:
∀S X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, S = pack_b_b_r_e_e X f g R c d → d = S 5
L5036Axiom. (
pack_b_b_r_e_e_5_eq2) We take the following as an axiom:
∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, d = pack_b_b_r_e_e X f g R c d 5
L5038Axiom. (
pack_b_b_r_e_e_inj) We take the following as an axiom:
∀X X', ∀f f' : set → set → set, ∀g g' : set → set → set, ∀R R' : set → set → prop, ∀c c' : set, ∀d d' : set, pack_b_b_r_e_e X f g R c d = pack_b_b_r_e_e X' f' g' R' c' d' → X = X' ∧ (∀x y ∈ X, f x y = f' x y) ∧ (∀x y ∈ X, g x y = g' x y) ∧ (∀x y ∈ X, R x y = R' x y) ∧ c = c' ∧ d = d'
L5040Axiom. (
pack_b_b_r_e_e_ext) We take the following as an axiom:
∀X, ∀f f' : set → set → set, ∀g g' : set → set → set, ∀R R' : set → set → prop, ∀c, ∀d, (∀x y ∈ X, f x y = f' x y) → (∀x y ∈ X, g x y = g' x y) → (∀x y ∈ X, R x y ↔ R' x y) → pack_b_b_r_e_e X f g R c d = pack_b_b_r_e_e X f' g' R' c d
L5046Definition. We define
struct_b_b_r_e_e to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀f : set → set → set, (∀x y ∈ X, f x y ∈ X) → ∀g : set → set → set, (∀x y ∈ X, g x y ∈ X) → ∀R : set → set → prop, ∀c : set, c ∈ X → ∀d : set, d ∈ X → q (pack_b_b_r_e_e X f g R c d)) → q S of type
set → prop.
Primitive. The name
unpack_b_b_r_e_e_i is a term of type
set → (set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → set) → set.
L5063Axiom. (
unpack_b_b_r_e_e_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → set, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → ∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X f' g' R' c d = Phi X f g R c d) → unpack_b_b_r_e_e_i (pack_b_b_r_e_e X f g R c d) Phi = Phi X f g R c d
Primitive. The name
unpack_b_b_r_e_e_o is a term of type
set → (set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → prop) → prop.
L5072Axiom. (
unpack_b_b_r_e_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → ∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X f' g' R' c d = Phi X f g R c d) → unpack_b_b_r_e_e_o (pack_b_b_r_e_e X f g R c d) Phi = Phi X f g R c d
Beginning of Section explicit_OrderedField_RepIndep2
L5085Variable zero one : set
L5087Variable plus mult : set → set → set
L5088Variable leq : set → set → prop
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L5092Variable plus' mult' : set → set → set
L5094Variable leq' : set → set → prop
Notation. We use
+ as an infix operator with priority 355 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L5097Hypothesis Hpp' : ∀a b ∈ R, a + b = a + b
L5099Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
L5100Hypothesis Hll' : ∀a b ∈ R, leq a b ↔ leq' a b
End of Section explicit_OrderedField_RepIndep2
Beginning of Section explicit_Reals_RepIndep2
L5115Variable zero one : set
L5117Variable plus mult : set → set → set
L5118Variable leq : set → set → prop
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
plus.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult.
L5122Variable plus' mult' : set → set → set
L5124Variable leq' : set → set → prop
Notation. We use
+ as an infix operator with priority 355 and which associates to the right corresponding to applying term
plus'.
Notation. We use
⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term
mult'.
L5127Hypothesis Hpp' : ∀a b ∈ R, a + b = a + b
L5129Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
L5130Hypothesis Hll' : ∀a b ∈ R, leq a b ↔ leq' a b
End of Section explicit_Reals_RepIndep2
Beginning of Section RealsStruct
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
RealsStruct_plus Rs.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
RealsStruct_mult Rs.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
RealsStruct_leq Rs.
L5180Definition. We define
RealsStruct_lt to be
λx y ⇒ x ≤ y ∧ x ≠ y of type
set → set → prop.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
RealsStruct_lt.
L5256Axiom. (
RealsStruct_Arch) We take the following as an axiom:
∀x y ∈ R, zero < x → zero ≤ y → ∃n ∈ N, y ≤ n * x
L5258Axiom. (
RealsStruct_Compl) We take the following as an axiom:
∀a b ∈ RN, (∀n ∈ N, a n ≤ b n ∧ a n ≤ a (n + one) ∧ b (n + one) ≤ b n) → ∃x ∈ R, ∀n ∈ N, a n ≤ x ∧ x ≤ b n
L5293Axiom. (
RealsStruct_Z_props) We take the following as an axiom:
∀p : prop, ((∀n ∈ Npos, - n ∈ Z) → zero ∈ Z → Npos ⊆ Z → Z ⊆ R → (∀n ∈ Z, ∀q : prop, (- n ∈ Npos → q) → (n = zero → q) → (n ∈ Npos → q) → q) → one ∈ Z → - one ∈ Z → (∀m ∈ Z, - m ∈ Z) → (∀n m ∈ Z, n + m ∈ Z) → (∀n m ∈ Z, n * m ∈ Z) → p) → p
L5312Axiom. (
RealsStruct_Q_props) We take the following as an axiom:
∀p : prop, (Q ⊆ R → (∀x ∈ Q, ∀q : prop, (x ∈ R → ∀n ∈ Z, ∀m ∈ Npos, m * x = n → q) → q) → (∀x ∈ R, ∀n ∈ Z, ∀m ∈ Npos, m * x = n → x ∈ Q) → p) → p
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
Field_div (Field_of_RealsStruct Rs).
End of Section RealsStruct
Beginning of Section MetaCat
L5367Variable Obj : set → prop
L5369Variable Hom : set → set → set → prop
L5370Variable id : set → set
L5371Variable comp : set → set → set → set → set → set
L5372Definition. We define
idT to be
∀X : set, Obj X → Hom X X (id X) of type
prop.
L5374Definition. We define
compT to be
∀X Y Z : set, ∀f g : set, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom X Z (comp X Y Z g f) of type
prop.
L5379Definition. We define
idL to be
∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f of type
prop.
L5383Definition. We define
idR to be
∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f of type
prop.
L5387Definition. We define
compAssoc to be
∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f) of type
prop.
Primitive. The name
MetaCat is a term of type
prop.
L5396Axiom. (
MetaCat_I) We take the following as an axiom:
idT → compT → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f) → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f) → (∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f)) → MetaCat
L5403Axiom. (
MetaCat_E) We take the following as an axiom:
MetaCat → ∀p : prop, (idT → compT → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f) → (∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f) → (∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f)) → p) → p
End of Section MetaCat
Beginning of Section MetaCatOp
L5416Variable Obj : set → prop
L5418Variable Hom : set → set → set → prop
L5419Variable id : set → set
L5420Variable comp : set → set → set → set → set → set
L5421Axiom. (
MetaCatOp) We take the following as an axiom:
MetaCat Obj Hom id comp → MetaCat Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f)
End of Section MetaCatOp
Beginning of Section LimsCoLims
L5429Variable Obj : set → prop
L5431Variable Hom : set → set → set → prop
L5432Variable id : set → set
L5433Variable comp : set → set → set → set → set → set
L5434Definition. We define
monic to be
λX Y f ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ ∀Z : set, Obj Z → ∀g h : set, Hom Z X g → Hom Z X h → comp Z X Y f g = comp Z X Y f h → g = h of type
set → set → set → prop.
L5442Definition. We define
terminal_p to be
λY h ⇒ Obj Y ∧ ∀X : set, Obj X → Hom X Y (h X) ∧ ∀h' : set, Hom X Y h' → h' = h X of type
set → (set → set) → prop.
L5448Definition. We define
initial_p to be
λY h ⇒ Obj Y ∧ ∀X : set, Obj X → Hom Y X (h X) ∧ ∀h' : set, Hom Y X h' → h' = h X of type
set → (set → set) → prop.
L5454Definition. We define
product_p to be
λX Y Z pi0 pi1 pair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom Z X pi0 ∧ Hom Z Y pi1 ∧ ∀W : set, Obj W → ∀h k : set, Hom W X h → Hom W Y k → Hom W Z (pair W h k) ∧ comp W Z X pi0 (pair W h k) = h ∧ comp W Z Y pi1 (pair W h k) = k ∧ ∀u : set, Hom W Z u → comp W Z X pi0 u = h → comp W Z Y pi1 u = k → u = pair W h k of type
set → set → set → set → set → (set → set → set → set) → prop.
L5470Definition. We define
product_constr_p to be
λprod pi0 pi1 pair ⇒ ∀X Y : set, Obj X → Obj Y → product_p X Y (prod X Y) (pi0 X Y) (pi1 X Y) (pair X Y) of type
(set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → prop.
L5474Definition. We define
coproduct_p to be
λX Y Z i0 i1 comb ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom X Z i0 ∧ Hom Y Z i1 ∧ ∀W : set, Obj W → ∀h k : set, Hom X W h → Hom Y W k → Hom Z W (comb W h k) ∧ comp X Z W (comb W h k) i0 = h ∧ comp Y Z W (comb W h k) i1 = k ∧ ∀hk : set, Hom Z W hk → comp X Z W hk i0 = h → comp Y Z W hk i1 = k → hk = comb W h k of type
set → set → set → set → set → (set → set → set → set) → prop.
L5490Definition. We define
coproduct_constr_p to be
λcoprod i0 i1 copair ⇒ ∀X Y : set, Obj X → Obj Y → coproduct_p X Y (coprod X Y) (i0 X Y) (i1 X Y) (copair X Y) of type
(set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → prop.
L5494Definition. We define
equalizer_p to be
λX Y f g Q q fac ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ Hom X Y g ∧ Obj Q ∧ Hom Q X q ∧ comp Q X Y f q = comp Q X Y g q ∧ ∀W : set, Obj W → ∀h : set, Hom W X h → comp W X Y f h = comp W X Y g h → Hom W Q (fac W h) ∧ comp W Q X q (fac W h) = h ∧ ∀u : set, Hom W Q u → comp W Q X q u = h → u = fac W h of type
set → set → set → set → set → set → (set → set → set) → prop.
L5510Definition. We define
equalizer_constr_p to be
λquot canonmap fac ⇒ ∀X Y : set, Obj X → Obj Y → ∀f g : set, Hom X Y f → Hom X Y g → equalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type
(set → set → set → set → set) → (set → set → set → set → set) → (set → set → set → set → set → set → set) → prop.
L5514Definition. We define
coequalizer_p to be
λX Y f g Q q fac ⇒ Obj X ∧ Obj Y ∧ Hom X Y f ∧ Hom X Y g ∧ Obj Q ∧ Hom Y Q q ∧ comp X Y Q q f = comp X Y Q q g ∧ ∀W : set, Obj W → ∀h : set, Hom Y W h → comp X Y W h f = comp X Y W h g → Hom Q W (fac W h) ∧ comp Y Q W (fac W h) q = h ∧ ∀u : set, Hom Q W u → comp Y Q W u q = h → u = fac W h of type
set → set → set → set → set → set → (set → set → set) → prop.
L5530Definition. We define
coequalizer_constr_p to be
λquot canonmap fac ⇒ ∀X Y : set, Obj X → Obj Y → ∀f g : set, Hom X Y f → Hom X Y g → coequalizer_p X Y f g (quot X Y f g) (canonmap X Y f g) (fac X Y f g) of type
(set → set → set → set → set) → (set → set → set → set → set) → (set → set → set → set → set → set → set) → prop.
L5534Definition. We define
pullback_p to be
λX Y Z f g P pi0 pi1 pair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom X Z f ∧ Hom Y Z g ∧ Obj P ∧ Hom P X pi0 ∧ Hom P Y pi1 ∧ comp P X Z f pi0 = comp P Y Z g pi1 ∧ ∀W : set, Obj W → ∀h : set, Hom W X h → ∀k : set, Hom W Y k → comp W X Z f h = comp W Y Z g k → Hom W P (pair W h k) ∧ comp W P X pi0 (pair W h k) = h ∧ comp W P Y pi1 (pair W h k) = k ∧ ∀u : set, Hom W P u → comp W P X pi0 u = h → comp W P Y pi1 u = k → u = pair W h k of type
set → set → set → set → set → set → set → set → (set → set → set → set) → prop.
L5557Definition. We define
pullback_constr_p to be
λpb pi0 pi1 pair ⇒ ∀X Y Z : set, Obj X → Obj Y → Obj Z → ∀f g : set, Hom X Z f → Hom Y Z g → pullback_p X Y Z f g (pb X Y Z f g) (pi0 X Y Z f g) (pi1 X Y Z f g) (pair X Y Z f g) 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) → prop.
L5563Definition. We define
pushout_p to be
λX Y Z f g P i0 i1 copair ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom Z X f ∧ Hom Z Y g ∧ Obj P ∧ Hom X P i0 ∧ Hom Y P i1 ∧ comp Z X P i0 f = comp Z Y P i1 g ∧ ∀W : set, Obj W → ∀h : set, Hom X W h → ∀k : set, Hom Y W k → comp Z X W h f = comp Z Y W k g → Hom P W (copair W h k) ∧ comp X P W (copair W h k) i0 = h ∧ comp Y P W (copair W h k) i1 = k ∧ ∀u : set, Hom P W u → comp X P W u i0 = h → comp Y P W u i1 = k → u = copair W h k of type
set → set → set → set → set → set → set → set → (set → set → set → set) → prop.
L5586Definition. We define
pushout_constr_p to be
λpo i0 i1 copair ⇒ ∀X Y Z : set, Obj X → Obj Y → Obj Z → ∀f g : set, Hom Z X f → Hom Z Y g → pushout_p X Y Z f g (po X Y Z f g) (i0 X Y Z f g) (i1 X Y Z f g) (copair X Y Z f g) 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) → prop.
L5592Definition. We define
exponent_p to be
λprod pi0 pi1 pair X Y Z a lm ⇒ Obj X ∧ Obj Y ∧ Obj Z ∧ Hom (prod Z X) Y a ∧ ∀W : set, Obj W → ∀f : set, Hom (prod W X) Y f → Hom W Z (lm W f) ∧ comp (prod W X) (prod Z X) Y a (pair Z X (prod W X) (comp (prod W X) W Z (lm W f) (pi0 W X)) (pi1 W X)) = f ∧ ∀g : set, Hom W Z g → comp (prod W X) (prod Z X) Y a (pair Z X (prod W X) (comp (prod W X) W Z g (pi0 W X)) (pi1 W X)) = f → g = lm W f of type
(set → set → set) → (set → set → set) → (set → set → set) → (set → set → set → set → set → set) → set → set → set → set → (set → set → set) → prop.
L5604Definition. We define
product_exponent_constr_p to be
λprod pi0 pi1 pair exp a lm ⇒ product_constr_p prod pi0 pi1 pair ∧ ∀X Y : set, Obj X → Obj Y → exponent_p prod pi0 pi1 pair X Y (exp X Y) (a X Y) (lm X Y) 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) → prop.
L5610Definition. We define
subobject_classifier_p to be
λone uniqa Omega tru ch constr_p ⇒ terminal_p one uniqa ∧ Obj Omega ∧ Hom one Omega tru ∧ ∀X Y : set, ∀m : set, monic X Y m → Hom Y Omega (ch X Y m) ∧ pullback_p one Y Omega tru (ch X Y m) X (uniqa X) m (constr_p X Y m) of type
set → (set → set) → set → set → (set → set → set → set) → (set → set → set → set → set → set → set) → prop.
L5619Definition. We define
nno_p to be
λone uniqa N zer suc rec ⇒ terminal_p one uniqa ∧ Obj N ∧ Hom one N zer ∧ Hom N N suc ∧ ∀X : set, ∀x : set, ∀f : set, Obj X → Hom one X x → Hom X X f → Hom N X (rec X x f) ∧ comp one N X (rec X x f) zer = x ∧ comp N N X (rec X x f) suc = comp N X X f (rec X x f) ∧ ∀u : set, Hom N X u → comp one N X u zer = x → comp N N X u suc = comp N X X f u → u = rec X x f of type
set → (set → set) → set → set → set → (set → set → set → set) → prop.
End of Section LimsCoLims
Beginning of Section LimsCoLims2
L5639Variable Obj : set → prop
L5641Variable Hom : set → set → set → prop
L5642Variable id : set → set
L5643Variable comp : set → set → set → set → set → set
L5644Axiom. (
product_coproduct_Op) We take the following as an axiom:
∀X Y Z : set, ∀pi0 pi1 : set, ∀pair : set → set → set → set, product_p Obj Hom id comp X Y Z pi0 pi1 pair → coproduct_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z pi0 pi1 pair
L5649Axiom. (
product_coproduct_constr_Op) We take the following as an axiom:
∀prod : set → set → set, ∀pi0 pi1 : set → set → set, ∀pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair → coproduct_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) prod pi0 pi1 pair
L5654Axiom. (
coproduct_product_Op) We take the following as an axiom:
∀X Y Z : set, ∀i0 i1 : set, ∀copair : set → set → set → set, coproduct_p Obj Hom id comp X Y Z i0 i1 copair → product_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z i0 i1 copair
L5659Axiom. (
coproduct_product_constr_Op) We take the following as an axiom:
∀coprod : set → set → set, ∀i0 i1 : set → set → set, ∀copair : set → set → set → set → set → set, coproduct_constr_p Obj Hom id comp coprod i0 i1 copair → product_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) coprod i0 i1 copair
L5664Axiom. (
equalizer_coequalizer_Op) We take the following as an axiom:
∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : set → set → set, equalizer_p Obj Hom id comp X Y f g Q q fac → coequalizer_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) Y X f g Q q fac
L5669Axiom. (
equalizer_coequalizer_constr_Op) We take the following as an axiom:
∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac → coequalizer_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) (λX Y f g ⇒ quot Y X f g) (λX Y f g ⇒ canonmap Y X f g) (λX Y f g ⇒ fac Y X f g)
L5676Axiom. (
coequalizer_equalizer_Op) We take the following as an axiom:
∀X Y : set, ∀f g : set, ∀Q : set, ∀q : set, ∀fac : set → set → set, coequalizer_p Obj Hom id comp X Y f g Q q fac → equalizer_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) Y X f g Q q fac
L5681Axiom. (
coequalizer_equalizer_constr_Op) We take the following as an axiom:
∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, coequalizer_constr_p Obj Hom id comp quot canonmap fac → equalizer_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) (λX Y f g ⇒ quot Y X f g) (λX Y f g ⇒ canonmap Y X f g) (λX Y f g ⇒ fac Y X f g)
L5688Axiom. (
pullback_pushout_Op) We take the following as an axiom:
∀X Y Z : set, ∀f g : set, ∀P : set, ∀pi0 pi1 : set, ∀pair : set → set → set → set, pullback_p Obj Hom id comp X Y Z f g P pi0 pi1 pair → pushout_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z f g P pi0 pi1 pair
L5693Axiom. (
pullback_pushout_constr_Op) We take the following as an axiom:
∀pb : set → set → set → set → set → set, ∀pi0 pi1 : set → set → set → set → set → set, ∀pair : set → set → set → set → set → set → set → set → set, pullback_constr_p Obj Hom id comp pb pi0 pi1 pair → pushout_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) pb pi0 pi1 pair
L5698Axiom. (
pushout_pullback_Op) We take the following as an axiom:
∀X Y Z : set, ∀f g : set, ∀P : set, ∀i0 i1 : set, ∀copair : set → set → set → set, pushout_p Obj Hom id comp X Y Z f g P i0 i1 copair → pullback_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) X Y Z f g P i0 i1 copair
L5703Axiom. (
pushout_pullback_constr_Op) We take the following as an axiom:
∀po : set → set → set → set → set → set, ∀i0 i1 : set → set → set → set → set → set, ∀copair : set → set → set → set → set → set → set → set → set, pushout_constr_p Obj Hom id comp po i0 i1 copair → pullback_constr_p Obj (λX Y ⇒ Hom Y X) id (λX Y Z f g ⇒ comp Z Y X g f) po i0 i1 copair
L5708Axiom. (
product_equalizer_pullback_constr) We take the following as an axiom:
MetaCat Obj Hom id comp → ∀quot : set → set → set → set → set, ∀canonmap : set → set → set → set → set, ∀fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac → ∀prod : set → set → set, ∀pi0 : set → set → set, ∀pi1 : set → set → set, ∀pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair → pullback_constr_p Obj Hom id comp (λX Y Z f g ⇒ quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) (λX Y Z f g ⇒ comp (quot (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y))) (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)))) (λX Y Z f g W h k ⇒ fac (prod X Y) Z (comp (prod X Y) X Z f (pi0 X Y)) (comp (prod X Y) Y Z g (pi1 X Y)) W (pair X Y W h k))
L5727Axiom. (
product_equalizer_pullback_constr_ex) We take the following as an axiom:
MetaCat Obj Hom id comp → (∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p Obj Hom id comp quot canonmap fac) → (∃prod : set → set → set, ∃pi0 : set → set → set, ∃pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p Obj Hom id comp prod pi0 pi1 pair) → ∃pb : set → set → set → set → set → set, ∃pi0 : set → set → set → set → set → set, ∃pi1 : set → set → set → set → set → set, ∃pair : set → set → set → set → set → set → set → set → set, pullback_constr_p Obj Hom id comp pb pi0 pi1 pair
End of Section LimsCoLims2
Beginning of Section LimsCoLims3
L5750Variable Obj : set → prop
L5752Variable Hom : set → set → set → prop
L5753Variable id : set → set
L5754Variable comp : set → set → set → set → set → set
L5755Axiom. (
coproduct_coequalizer_pushout_constr_ex) We take the following as an axiom:
MetaCat Obj Hom id comp → (∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p Obj Hom id comp quot canonmap fac) → (∃coprod : set → set → set, ∃i0 : set → set → set, ∃i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p Obj Hom id comp coprod i0 i1 copair) → ∃po : set → set → set → set → set → set, ∃i0 : set → set → set → set → set → set, ∃i1 : set → set → set → set → set → set, ∃copair : set → set → set → set → set → set → set → set → set, pushout_constr_p Obj Hom id comp po i0 i1 copair
End of Section LimsCoLims3
L5776Definition. We define
SetHom to be
λX Y f ⇒ f ∈ YX of type
set → set → set → prop.
Beginning of Section MetaFunctor
L5781Variable Obj : set → prop
L5783Variable Hom : set → set → set → prop
L5784Variable id : set → set
L5785Variable comp : set → set → set → set → set → set
L5786Variable Obj' : set → prop
L5787Variable Hom' : set → set → set → prop
L5788Variable id' : set → set
L5789Variable comp' : set → set → set → set → set → set
L5790Variable F0 : set → set
L5792Variable F1 : set → set → set → set
Primitive. The name
MetaFunctor is a term of type
prop.
L5796Axiom. (
MetaFunctorI) We take the following as an axiom:
(∀X, Obj X → Obj' (F0 X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) → (∀X, Obj X → F1 X X (id X) = id' (F0 X)) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)) → MetaFunctor
L5803Axiom. (
MetaFunctorE) We take the following as an axiom:
MetaFunctor → ∀p : prop, ((∀X, Obj X → Obj' (F0 X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) → (∀X, Obj X → F1 X X (id X) = id' (F0 X)) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)) → p) → p
End of Section MetaFunctor
Beginning of Section IdFunctor
L5833Variable Obj : set → prop
L5835Variable Hom : set → set → set → prop
L5836Variable id : set → set
L5837Variable comp : set → set → set → set → set → set
End of Section IdFunctor
Beginning of Section CompFunctors
L5847Variable Obj : set → prop
L5849Variable Hom : set → set → set → prop
L5850Variable id : set → set
L5851Variable comp : set → set → set → set → set → set
L5852Variable Obj' : set → prop
L5853Variable Hom' : set → set → set → prop
L5854Variable id' : set → set
L5855Variable comp' : set → set → set → set → set → set
L5856Variable Obj'' : set → prop
L5857Variable Hom'' : set → set → set → prop
L5858Variable id'' : set → set
L5859Variable comp'' : set → set → set → set → set → set
L5860Variable F0 : set → set
L5861Variable F1 : set → set → set → set
L5862Variable G0 : set → set
L5863Variable G1 : set → set → set → set
L5864Axiom. (
MetaCat_CompFunctors) We take the following as an axiom:
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1 → MetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 → MetaFunctor Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f))
End of Section CompFunctors
Beginning of Section MetaNatTrans
L5878Variable Obj : set → prop
L5880Variable Hom : set → set → set → prop
L5881Variable id : set → set
L5882Variable comp : set → set → set → set → set → set
L5883Variable Obj' : set → prop
L5884Variable Hom' : set → set → set → prop
L5885Variable id' : set → set
L5886Variable comp' : set → set → set → set → set → set
L5887Variable F0 : set → set
L5889Variable F1 : set → set → set → set
L5890Variable G0 : set → set
L5891Variable G1 : set → set → set → set
L5892Variable eta : set → set
L5897Axiom. (
MetaNatTransI) We take the following as an axiom:
(∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)) → MetaNatTrans
L5904Axiom. (
MetaNatTransE) We take the following as an axiom:
MetaNatTrans → ∀p : prop, ((∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) → (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)) → p) → p
End of Section MetaNatTrans
Beginning of Section CompFunctorNatTrans
L5937Variable Obj : set → prop
L5939Variable Hom : set → set → set → prop
L5940Variable id : set → set
L5941Variable comp : set → set → set → set → set → set
L5942Variable Obj' : set → prop
L5943Variable Hom' : set → set → set → prop
L5944Variable id' : set → set
L5945Variable comp' : set → set → set → set → set → set
L5946Variable Obj'' : set → prop
L5947Variable Hom'' : set → set → set → prop
L5948Variable id'' : set → set
L5949Variable comp'' : set → set → set → set → set → set
L5950Variable F0 : set → set
L5951Variable F1 : set → set → set → set
L5952Variable G0 : set → set
L5953Variable G1 : set → set → set → set
L5954Variable H0 : set → set
L5955Variable H1 : set → set → set → set
L5956Variable eta : set → set
L5957Axiom. (
MetaCat_CompFunctorNatTrans) We take the following as an axiom:
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1 → MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1 → MetaNatTrans Obj Hom id comp Obj' Hom' id' comp' F0 F1 G0 G1 eta → MetaFunctor Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' H0 H1 → MetaNatTrans Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ H0 (F0 X)) (λX Y f ⇒ H1 (F0 X) (F0 Y) (F1 X Y f)) (λX ⇒ H0 (G0 X)) (λX Y f ⇒ H1 (G0 X) (G0 Y) (G1 X Y f)) (λX ⇒ H1 (F0 X) (G0 X) (eta X))
End of Section CompFunctorNatTrans
Beginning of Section CompNatTransFunctor
L5981Variable Obj : set → prop
L5983Variable Hom : set → set → set → prop
L5984Variable id : set → set
L5985Variable comp : set → set → set → set → set → set
L5986Variable Obj' : set → prop
L5987Variable Hom' : set → set → set → prop
L5988Variable id' : set → set
L5989Variable comp' : set → set → set → set → set → set
L5990Variable Obj'' : set → prop
L5991Variable Hom'' : set → set → set → prop
L5992Variable id'' : set → set
L5993Variable comp'' : set → set → set → set → set → set
L5994Variable F0 : set → set
L5995Variable F1 : set → set → set → set
L5996Variable G0 : set → set
L5997Variable G1 : set → set → set → set
L5998Variable H0 : set → set
L5999Variable H1 : set → set → set → set
L6000Variable eta : set → set
L6001Axiom. (
MetaCat_CompNatTransFunctor) We take the following as an axiom:
MetaNatTrans Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' F0 F1 G0 G1 eta → MetaFunctor Obj Hom id comp Obj' Hom' id' comp' H0 H1 → MetaNatTrans Obj Hom id comp Obj'' Hom'' id'' comp'' (λX ⇒ F0 (H0 X)) (λX Y f ⇒ F1 (H0 X) (H0 Y) (H1 X Y f)) (λX ⇒ G0 (H0 X)) (λX Y f ⇒ G1 (H0 X) (H0 Y) (H1 X Y f)) (λX ⇒ eta (H0 X))
End of Section CompNatTransFunctor
Beginning of Section MetaMonad
L6023Variable Obj : set → prop
L6025Variable Hom : set → set → set → prop
L6026Variable id : set → set
L6027Variable comp : set → set → set → set → set → set
L6028Variable T0 : set → set
L6030Variable T1 : set → set → set → set
L6031Variable eta : set → set
L6032Variable mu : set → set
Primitive. The name
MetaMonad is a term of type
prop.
L6039Axiom. (
MetaMonadI) We take the following as an axiom:
(∀X, Obj X → comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X))) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) → MetaMonad
L6045Axiom. (
MetaMonadE) We take the following as an axiom:
MetaMonad → (∀p : prop, ((∀X, Obj X → comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X))) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X)) → (∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X)) → p) → p)
End of Section MetaMonad
Beginning of Section MetaAdjunction
L6071Variable Obj : set → prop
L6073Variable Hom : set → set → set → prop
L6074Variable id : set → set
L6075Variable comp : set → set → set → set → set → set
L6076Variable Obj' : set → prop
L6077Variable Hom' : set → set → set → prop
L6078Variable id' : set → set
L6079Variable comp' : set → set → set → set → set → set
L6080Variable F0 : set → set
L6082Variable F1 : set → set → set → set
L6083Variable G0 : set → set
L6084Variable G1 : set → set → set → set
L6085Variable eta : set → set
L6086Variable eps : set → set
L6093Axiom. (
MetaAdjunctionI) We take the following as an axiom:
(∀X, Obj X → comp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) → (∀Y, Obj' Y → comp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) → MetaAdjunction
L6098Axiom. (
MetaAdjunctionE) We take the following as an axiom:
MetaAdjunction → ∀p : prop, ((∀X, Obj X → comp' (F0 X) (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) (F1 X (G0 (F0 X)) (eta X)) = id' (F0 X)) → (∀Y, Obj' Y → comp (G0 Y) (G0 (F0 (G0 Y))) (G0 Y) (G1 (F0 (G0 Y)) Y (eps Y)) (eta (G0 Y)) = id (G0 Y)) → p) → p
L6123Axiom. (
MetaAdjunctionMonad) We take the following as an axiom:
MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1 → MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1 → MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta → MetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps → MetaAdjunction → MetaMonad Obj Hom id comp (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta (λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)))
End of Section MetaAdjunction
Beginning of Section MetaCatConcrete
L6139Variable Obj : set → prop
L6141Variable U : set → set
L6142Variable Hom : set → set → set → prop
L6143Axiom. (
MetaCatConcrete) We take the following as an axiom:
(∀X Y f, Obj X → Obj Y → Hom X Y f → f ∈ U YU X) → (∀X, Obj X → Hom X X (lam_id (U X))) → (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom X Z (lam_comp (U X) g f)) → MetaCat Obj Hom (λX ⇒ lam_id (U X)) (λX Y Z g f ⇒ lam_comp (U X) g f)
End of Section MetaCatConcrete
L6155Axiom. (
MetaCatSet) We take the following as an axiom:
L6164Axiom. (
MetaCatSet_initial_gen) We take the following as an axiom:
∀Obj : set → prop, Obj 0 → ∃Y : set, ∃uniqa : set → set, initial_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Y uniqa
L6180Axiom. (
MetaCatSet_coproduct_gen) We take the following as an axiom:
∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setsum X Y)) → ∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair
L6188Axiom. (
MetaCatSet_coproduct) We take the following as an axiom:
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p (λ_ ⇒ True) SetHom (λX ⇒ λx ∈ X ⇒ x) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) coprod i0 i1 copair
L6193Axiom. (
MetaCatSet_product_gen) We take the following as an axiom:
∀Obj : set → prop, (∀X, Obj X → ∀Y, Obj Y → Obj (setprod X Y)) → ∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p Obj SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair
L6201Axiom. (
MetaCatSet_product) We take the following as an axiom:
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p (λ_ ⇒ True) SetHom (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) prod pi0 pi1 pair
L6208Definition. We define
famunion_closed to be
λU : set ⇒ ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → famunion X F ∈ U of type
set → prop.
L6212Axiom. (
ZF_closed_0) We take the following as an axiom:
Primitive. The name
Hom_struct_e is a term of type
set → set → set → prop.
Primitive. The name
Hom_struct_u is a term of type
set → set → set → prop.
Primitive. The name
Hom_struct_b is a term of type
set → set → set → prop.
Primitive. The name
Hom_struct_p is a term of type
set → set → set → prop.
Primitive. The name
Hom_struct_r is a term of type
set → set → set → prop.
Primitive. The name
Hom_struct_c is a term of type
set → set → set → prop.
Beginning of Section MetaCatStruct
L6341Variable Obj : set → prop
End of Section MetaCatStruct
L6420Definition. We define
struct_comp to be
λX Y Z f g ⇒ lam_comp (X 0) f g of type
set → set → set → set → set → set.