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)
L3Definition. We define
True to be
∀p : prop, p → p of type
prop.
L4Definition. We define
False to be
∀p : prop, p of type
prop.
L5Definition. 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.
L8Definition. 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.
L11Definition. 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.
L14Definition. 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
L19Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
L20Definition. 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
L27Axiom. (
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
L31Definition. 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.
L35Axiom. (
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.
L37Definition. 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.
L38Axiom. (
set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
L39Axiom. (
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.
L42Axiom. (
EmptyAx) We take the following as an axiom:
Primitive. The name
⋃ is a term of type
set → set.
L45Axiom. (
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.
L48Axiom. (
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).
L51Axiom. (
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
L52Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U, x ⊆ U of type
set → prop.
L53Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type
set → prop.
L54Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type
set → prop.
L55Definition. 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.
L58Axiom. (
UnivOf_In) We take the following as an axiom:
L61Axiom. (
UnivOf_Min) We take the following as an axiom:
L62Axiom. (
FalseE) We take the following as an axiom:
L63Axiom. (
TrueI) We take the following as an axiom:
L64Axiom. (
andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
L65Axiom. (
andEL) We take the following as an axiom:
L66Axiom. (
andER) We take the following as an axiom:
L67Axiom. (
orIL) We take the following as an axiom:
L68Axiom. (
orIR) We take the following as an axiom:
Beginning of Section PropN
L70Variable P1 P2 P3 : prop
L71Axiom. (
and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
L72Axiom. (
and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
L73Axiom. (
or3I1) We take the following as an axiom:
L74Axiom. (
or3I2) We take the following as an axiom:
L75Axiom. (
or3I3) We take the following as an axiom:
L76Axiom. (
or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
L78Axiom. (
and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
L80Axiom. (
and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
L84Axiom. (
iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
L85Axiom. (
iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
L86Axiom. (
iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
L87Axiom. (
iff_refl) We take the following as an axiom:
L88Axiom. (
iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
L89Axiom. (
iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
L90Axiom. (
eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
L91Axiom. (
f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
L92Axiom. (
neq_i_sym) We take the following as an axiom:
L93Definition. 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.
L96Axiom. (
Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
L97Axiom. (
pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
L98Axiom. (
prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
L99Axiom. (
Subq_ref) We take the following as an axiom:
L100Axiom. (
Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
L101Axiom. (
Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X
L102Axiom. (
EmptyE) We take the following as an axiom:
L103Axiom. (
Subq_Empty) We take the following as an axiom:
L105Axiom. (
Empty_eq) We take the following as an axiom:
L106Axiom. (
UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
L107Axiom. (
UnionE) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
L108Axiom. (
UnionE_impred) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
L109Axiom. (
PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
L110Axiom. (
PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
L113Axiom. (
xm) We take the following as an axiom:
L114Axiom. (
dneg) We take the following as an axiom:
L116Axiom. (
eq_or_nand) We take the following as an axiom:
Primitive. The name
exactly1of2 is a term of type
prop → prop → prop.
L121Axiom. (
exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p
L123Axiom. (
ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
L124Axiom. (
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
L125Axiom. (
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
L126Axiom. (
ReplE') We take the following as an axiom:
∀X, ∀f : set → set, ∀p : set → prop, (∀x ∈ X, p (f x)) → ∀y ∈ {f x|x ∈ X}, p y
L127Axiom. (
Repl_Empty) We take the following as an axiom:
L128Axiom. (
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}
L129Axiom. (
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}
L130Axiom. (
Repl_inv_eq) We take the following as an axiom:
∀P : set → prop, ∀f g : set → set, (∀x, P x → g (f x) = x) → ∀X, (∀x ∈ X, P x) → {g y|y ∈ {f x|x ∈ X}} = X
L131Axiom. (
Repl_invol_eq) We take the following as an axiom:
∀P : set → prop, ∀f : set → set, (∀x, P x → f (f x) = x) → ∀X, (∀x ∈ X, P x) → {f y|y ∈ {f x|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.
L136Axiom. (
If_i_0) We take the following as an axiom:
L137Axiom. (
If_i_1) We take the following as an axiom:
L138Axiom. (
If_i_or) 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.
L142Axiom. (
UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
L143Axiom. (
UPairI1) We take the following as an axiom:
L144Axiom. (
UPairI2) 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.
L148Axiom. (
SingI) We take the following as an axiom:
L149Axiom. (
SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
L150Axiom. (
Sing_inj) We take the following as an axiom:
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.
L155Axiom. (
binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
L156Axiom. (
binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
L157Axiom. (
binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
L158Axiom. (
binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)
L159Axiom. (
binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
L161Axiom. (
binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
L168Definition. 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.
Primitive. The name
famunion is a term 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.
L175Axiom. (
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
L176Axiom. (
famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
L177Axiom. (
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
Beginning of Section SepSec
L183Variable P : set → prop
L184Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)
Primitive. The name
Sep is a term of type
set.
End of Section SepSec
Notation.
{x ∈ A | B} is notation for
Sep A (λ x . B).
L190Axiom. (
SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
L191Axiom. (
SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
L192Axiom. (
SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
L193Axiom. (
SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
L194Axiom. (
Sep_Empty) We take the following as an axiom:
L195Axiom. (
Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
L196Axiom. (
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).
L200Axiom. (
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}
L201Axiom. (
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
L202Axiom. (
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
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.
L207Axiom. (
binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
L208Axiom. (
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.
L221Axiom. (
setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
L222Axiom. (
setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
L223Axiom. (
setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
L224Axiom. (
setminusE2) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∉ Y
L229Axiom. (
In_irref) We take the following as an axiom:
L230Axiom. (
In_no2cycle) We take the following as an axiom:
Primitive. The name
ordsucc is a term of type
set → set.
L233Axiom. (
ordsuccI1) We take the following as an axiom:
L234Axiom. (
ordsuccI2) We take the following as an axiom:
L235Axiom. (
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.
L239Axiom. (
ordsucc_inj) We take the following as an axiom:
L241Axiom. (
In_0_1) We take the following as an axiom:
L242Axiom. (
In_0_2) We take the following as an axiom:
L243Axiom. (
In_1_2) We take the following as an axiom:
L244Axiom. (
In_1_3) We take the following as an axiom:
L245Axiom. (
In_2_3) We take the following as an axiom:
L246Axiom. (
In_1_4) We take the following as an axiom:
L247Axiom. (
In_2_4) We take the following as an axiom:
L248Axiom. (
In_3_4) We take the following as an axiom:
L249Axiom. (
In_1_5) We take the following as an axiom:
L250Axiom. (
In_2_5) We take the following as an axiom:
L251Axiom. (
In_3_5) We take the following as an axiom:
L252Axiom. (
In_4_5) We take the following as an axiom:
L253Axiom. (
In_1_6) We take the following as an axiom:
L254Axiom. (
In_1_7) We take the following as an axiom:
L255Axiom. (
In_1_8) We take the following as an axiom:
L256Definition. 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.
L257Axiom. (
nat_0) We take the following as an axiom:
L258Axiom. (
nat_ordsucc) We take the following as an axiom:
L259Axiom. (
nat_1) We take the following as an axiom:
L260Axiom. (
nat_2) We take the following as an axiom:
L261Axiom. (
nat_3) We take the following as an axiom:
L262Axiom. (
nat_4) We take the following as an axiom:
L263Axiom. (
nat_5) We take the following as an axiom:
L264Axiom. (
nat_6) We take the following as an axiom:
L265Axiom. (
nat_7) We take the following as an axiom:
L266Axiom. (
nat_8) We take the following as an axiom:
L269Axiom. (
nat_ind) We take the following as an axiom:
L271Axiom. (
nat_inv) We take the following as an axiom:
L273Axiom. (
nat_p_trans) We take the following as an axiom:
L274Axiom. (
nat_trans) We take the following as an axiom:
L277Axiom. (
cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
L278Axiom. (
cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
L279Axiom. (
cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
L280Axiom. (
neq_0_1) We take the following as an axiom:
L281Axiom. (
neq_1_0) We take the following as an axiom:
L282Axiom. (
neq_0_2) We take the following as an axiom:
L283Axiom. (
neq_2_0) We take the following as an axiom:
L284Axiom. (
neq_1_2) We take the following as an axiom:
L285Axiom. (
neq_1_3) We take the following as an axiom:
L286Axiom. (
neq_2_3) We take the following as an axiom:
L287Axiom. (
neq_2_4) We take the following as an axiom:
L288Axiom. (
neq_3_4) We take the following as an axiom:
L289Axiom. (
ZF_closed_E) We take the following as an axiom:
Primitive. The name
ω is a term of type
set.
L301Axiom. (
omega_nat_p) We take the following as an axiom:
L302Axiom. (
nat_p_omega) We take the following as an axiom:
L311Axiom. (
ordinal_1) We take the following as an axiom:
L312Axiom. (
ordinal_2) We take the following as an axiom:
L328Axiom. (
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
L330Definition. 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.
L331Definition. 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.
L332Axiom. (
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
L333Axiom. (
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.
L336Axiom. (
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
L337Axiom. (
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
L338Axiom. (
bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
L339Axiom. (
bij_id) We take the following as an axiom:
L340Axiom. (
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))
L341Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set, bij X Y f of type
set → set → prop.
L342Axiom. (
equip_ref) We take the following as an axiom:
L343Axiom. (
equip_sym) We take the following as an axiom:
L344Axiom. (
equip_tra) We take the following as an axiom:
Beginning of Section SchroederBernstein
L347Axiom. (
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
L348Axiom. (
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
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
L357Definition. We define
finite to be
λX ⇒ ∃n ∈ ω, equip X n of type
set → prop.
L358Axiom. (
finite_ind) We take the following as an axiom:
L363Axiom. (
Subq_finite) We take the following as an axiom:
L365Axiom. (
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
L366Axiom. (
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
L367Axiom. (
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
L368Axiom. (
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
Beginning of Section Descr_ii
L370Variable P : (set → set) → prop
Primitive. The name
Descr_ii is a term of type
set → set.
L373Hypothesis Pex : ∃f : set → set, P f
L374Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
L378Variable P : (set → set → set) → prop
Primitive. The name
Descr_iii is a term of type
set → set → set.
L381Hypothesis Pex : ∃f : set → set → set, P f
L382Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Primitive. The name
Descr_Vo1 is a term of type
Vo 1.
L389Hypothesis Pex : ∃f : Vo 1, P f
L390Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
L395Variable f g : set → set
Primitive. The name
If_ii is a term of type
set → set.
L398Axiom. (
If_ii_1) We take the following as an axiom:
L399Axiom. (
If_ii_0) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
L403Variable f g : set → set → set
Primitive. The name
If_iii is a term of type
set → set → set.
L406Axiom. (
If_iii_1) We take the following as an axiom:
L407Axiom. (
If_iii_0) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
L410Variable F : set → (set → set) → set
L411Definition. We define
In_rec_i_G to be
λX Y ⇒ ∀R : set → set → prop, (∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type
set → set → prop.
Primitive. The name
In_rec_i is a term of type
set → set.
L416Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
L420Axiom. (
In_rec_i_eq) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L423Variable F : set → (set → (set → set)) → (set → set)
L424Definition. We define
In_rec_G_ii to be
λX Y ⇒ ∀R : set → (set → set) → prop, (∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type
set → (set → set) → prop.
Primitive. The name
In_rec_ii is a term of type
set → (set → set).
L429Hypothesis 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
L436Variable F : set → (set → (set → set → set)) → (set → set → set)
L437Definition. We define
In_rec_G_iii to be
λX Y ⇒ ∀R : set → (set → set → set) → prop, (∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type
set → (set → set → set) → prop.
Primitive. The name
In_rec_iii is a term of type
set → (set → set → set).
L442Hypothesis 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 NatRec
L450Variable f : set → set → set
L451Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
L453Axiom. (
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.
L460Axiom. (
add_nat_0R) We take the following as an axiom:
L461Axiom. (
add_nat_SR) We take the following as an axiom:
L462Axiom. (
add_nat_p) We take the following as an axiom:
L464Axiom. (
add_nat_0L) We take the following as an axiom:
L465Axiom. (
add_nat_SL) We take the following as an axiom:
L466Axiom. (
add_nat_com) We take the following as an axiom:
L468Definition. 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.
L470Axiom. (
mul_nat_0R) We take the following as an axiom:
L471Axiom. (
mul_nat_SR) We take the following as an axiom:
L472Axiom. (
mul_nat_p) We take the following as an axiom:
End of Section NatArith
L475Axiom. (
Inj1_eq) We take the following as an axiom:
L476Axiom. (
Inj1I1) We take the following as an axiom:
L477Axiom. (
Inj1I2) We take the following as an axiom:
L478Axiom. (
Inj1E) We take the following as an axiom:
L479Axiom. (
Inj1NE1) We take the following as an axiom:
L480Axiom. (
Inj1NE2) We take the following as an axiom:
L481Definition. We define
Inj0 to be
λX ⇒ {Inj1 x|x ∈ X} of type
set → set.
L482Axiom. (
Inj0I) We take the following as an axiom:
L483Axiom. (
Inj0E) We take the following as an axiom:
L485Axiom. (
Unj_eq) We take the following as an axiom:
L486Axiom. (
Unj_Inj1_eq) We take the following as an axiom:
L487Axiom. (
Inj1_inj) We take the following as an axiom:
L488Axiom. (
Unj_Inj0_eq) We take the following as an axiom:
L489Axiom. (
Inj0_inj) We take the following as an axiom:
L490Axiom. (
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.
L495Axiom. (
Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
L496Axiom. (
Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
L501Axiom. (
eq_1_Sing0) We take the following as an axiom:
L504Axiom. (
setsum_0_0) We take the following as an axiom:
Beginning of Section pair_setsum
L513Axiom. (
pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
L514Axiom. (
pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
L515Axiom. (
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)
L516Axiom. (
pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
L517Axiom. (
pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
L518Axiom. (
proj0I) We take the following as an axiom:
L519Axiom. (
proj0E) We take the following as an axiom:
L520Axiom. (
proj1I) We take the following as an axiom:
L521Axiom. (
proj1E) We take the following as an axiom:
L524Definition. 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.
L527Axiom. (
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
L530Axiom. (
proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X
L531Axiom. (
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)
L532Axiom. (
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
L533Axiom. (
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
L534Definition. 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.
L537Let lam : set → (set → set) → set ≝ Sigma
L538Definition. 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.
L541Axiom. (
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
L542Axiom. (
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
L543Axiom. (
apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
L544Axiom. (
apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
L545Axiom. (
beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
L546Axiom. (
proj0_ap_0) We take the following as an axiom:
L547Axiom. (
proj1_ap_1) We take the following as an axiom:
L548Axiom. (
pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
L549Axiom. (
pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
L550Axiom. (
ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
L551Axiom. (
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))
L552Definition. We define
pair_p to be
λu : set ⇒ pair (u 0) (u 1) = u of type
set → prop.
L553Axiom. (
pair_p_I) We take the following as an axiom:
L555Axiom. (
tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
L556Definition. 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.
L559Axiom. (
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
L560Axiom. (
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)
L561Axiom. (
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
L562Definition. 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.
L566Axiom. (
lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
Beginning of Section Tuples
End of Section Tuples
L572Axiom. (
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}
L573Axiom. (
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
L574Axiom. (
tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
End of Section pair_setsum