Surreal Numbers as Sets
From Parts 1 and 2
Object . The name
Eps_i is a term of type
(set → prop ) → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop , ∀x : set , P x → P (Eps_i P )
Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
Definition. 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 .
Definition. 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 .
Definition. 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 .
Definition. 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
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop , Q x y → Q y x of type
A → A → prop .
Definition. 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
Variable A B : SType
Axiom. (
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
Variable A : SType
Definition. 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 .
Axiom. (
prop_ext ) We take the following as an axiom:
∀p q : prop , iff p q → p = q
Object . 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 .
Definition. 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 .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y → Y ⊆ X → X = Y
Axiom. (
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 .
Object . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Object . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Object . The name
𝒫 is a term of type
set → set .
Axiom. (
PowerEq ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X ↔ Y ⊆ X
Object . The name
Repl is a term of type
set → (set → set ) → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (
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
Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U → ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U → 𝒫 X ∈ U of type
set → prop .
Definition. 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 .
Object . The name
UnivOf is a term of type
set → set .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Axiom. (
FalseE ) We take the following as an axiom:
Axiom. (
TrueI ) We take the following as an axiom:
Axiom. (
andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B
Axiom. (
andEL ) We take the following as an axiom:
∀A B : prop , A ∧ B → A
Axiom. (
andER ) We take the following as an axiom:
∀A B : prop , A ∧ B → B
Axiom. (
orIL ) We take the following as an axiom:
∀A B : prop , A → A ∨ B
Axiom. (
orIR ) We take the following as an axiom:
∀A B : prop , B → A ∨ B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (
and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (
and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop , (P1 → P2 → P3 → p ) → p )
Axiom. (
or3I1 ) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
Axiom. (
or3I2 ) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
Axiom. (
or3I3 ) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
Axiom. (
or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop , (P1 → p ) → (P2 → p ) → (P3 → p ) → p )
Variable P4 : prop
Axiom. (
and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Variable P5 : prop
Axiom. (
and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
Axiom. (
not_or_and_demorgan ) We take the following as an axiom:
∀A B : prop , ¬ (A ∨ B ) → ¬ A ∧ ¬ B
Axiom. (
not_ex_all_demorgan_i ) We take the following as an axiom:
∀P : set → prop , (¬ ∃x, P x ) → ∀x, ¬ P x
Axiom. (
iffI ) We take the following as an axiom:
∀A B : prop , (A → B ) → (B → A ) → (A ↔ B )
Axiom. (
iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → A → B
Axiom. (
iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → B → A
Axiom. (
iff_refl ) We take the following as an axiom:
∀A : prop , A ↔ A
Axiom. (
iff_sym ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → (B ↔ A )
Axiom. (
iff_trans ) We take the following as an axiom:
∀A B C : prop , (A ↔ B ) → (B ↔ C ) → (A ↔ C )
Axiom. (
eq_i_tra ) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
Axiom. (
f_eq_i ) We take the following as an axiom:
∀f : set → set , ∀x y, x = y → f x = f y
Axiom. (
neq_i_sym ) We take the following as an axiom:
∀x y, x ≠ y → y ≠ x
Definition. 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 .
Axiom. (
Eps_i_ex ) We take the following as an axiom:
∀P : set → prop , (∃x, P x ) → P (Eps_i P )
Axiom. (
pred_ext ) We take the following as an axiom:
∀P Q : set → prop , (∀x, P x ↔ Q x ) → P = Q
Axiom. (
prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q ) → (q → p ) → p = q
Axiom. (
Subq_ref ) We take the following as an axiom:
∀X : set , X ⊆ X
Axiom. (
Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y → Y ⊆ Z → X ⊆ Z
Axiom. (
Subq_contra ) We take the following as an axiom:
∀X Y z : set , X ⊆ Y → z ∉ Y → z ∉ X
Axiom. (
EmptyE ) We take the following as an axiom:
Axiom. (
Subq_Empty ) We take the following as an axiom:
Axiom. (
Empty_eq ) We take the following as an axiom:
∀X : set , (∀x, x ∉ X ) → X = Empty
Axiom. (
UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y → Y ∈ X → x ∈ ⋃ X
Axiom. (
UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∃Y : set , x ∈ Y ∧ Y ∈ X
Axiom. (
UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∀p : prop , (∀Y : set , x ∈ Y → Y ∈ X → p ) → p
Axiom. (
PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X → Y ∈ 𝒫 X
Axiom. (
PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X → Y ⊆ X
Axiom. (
xm ) We take the following as an axiom:
∀P : prop , P ∨ ¬ P
Axiom. (
dneg ) We take the following as an axiom:
∀P : prop , ¬ ¬ P → P
Axiom. (
not_all_ex_demorgan_i ) We take the following as an axiom:
∀P : set → prop , ¬ (∀x, P x ) → ∃x, ¬ P x
Axiom. (
eq_or_nand ) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y ) )
Object . The name
exactly1of2 is a term of type
prop → prop → prop .
Axiom. (
exactly1of2_E ) We take the following as an axiom:
∀A B : prop , exactly1of2 A B → ∀p : prop , (A → ¬ B → p ) → (¬ A → B → p ) → p
Axiom. (
ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀x : set , x ∈ A → F x ∈ {F x |x ∈ A }
Axiom. (
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
Axiom. (
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
Axiom. (
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
Axiom. (
Repl_Empty ) We take the following as an axiom:
Axiom. (
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 }
Axiom. (
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 }
Axiom. (
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
Axiom. (
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
Object . 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 .
Axiom. (
If_i_correct ) We take the following as an axiom:
∀p : prop , ∀x y : set , p ∧ (if p then x else y ) = x ∨ ¬ p ∧ (if p then x else y ) = y
Axiom. (
If_i_0 ) We take the following as an axiom:
∀p : prop , ∀x y : set , ¬ p → (if p then x else y ) = y
Axiom. (
If_i_1 ) We take the following as an axiom:
∀p : prop , ∀x y : set , p → (if p then x else y ) = x
Axiom. (
If_i_or ) We take the following as an axiom:
∀p : prop , ∀x y : set , (if p then x else y ) = x ∨ (if p then x else y ) = y
Object . The name
UPair is a term of type
set → set → set .
Notation .
{x ,y } is notation for
UPair x y .
Axiom. (
UPairE ) We take the following as an axiom:
∀x y z : set , x ∈ {y ,z } → x = y ∨ x = z
Axiom. (
UPairI1 ) We take the following as an axiom:
∀y z : set , y ∈ {y ,z }
Axiom. (
UPairI2 ) We take the following as an axiom:
∀y z : set , z ∈ {y ,z }
Object . The name
Sing is a term of type
set → set .
Notation .
{x } is notation for
Sing x .
Axiom. (
SingI ) We take the following as an axiom:
∀x : set , x ∈ {x }
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ {x } → y = x
Object . 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 .
Axiom. (
binunionI1 ) We take the following as an axiom:
∀X Y z : set , z ∈ X → z ∈ X ∪ Y
Axiom. (
binunionI2 ) We take the following as an axiom:
∀X Y z : set , z ∈ Y → z ∈ X ∪ Y
Axiom. (
binunionE ) We take the following as an axiom:
∀X Y z : set , z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X → p ) → (z ∈ Y → p ) → (z ∈ X ∪ Y → p )
Axiom. (
binunion_asso ) We take the following as an axiom:
∀X Y Z : set , X ∪ (Y ∪ Z ) = (X ∪ Y ) ∪ Z
Axiom. (
binunion_com_Subq ) We take the following as an axiom:
∀X Y : set , X ∪ Y ⊆ Y ∪ X
Axiom. (
binunion_com ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X
Axiom. (
binunion_Subq_1 ) We take the following as an axiom:
∀X Y : set , X ⊆ X ∪ Y
Axiom. (
binunion_Subq_2 ) We take the following as an axiom:
∀X Y : set , Y ⊆ X ∪ Y
Axiom. (
binunion_Subq_min ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
Axiom. (
Subq_binunion_eq ) We take the following as an axiom:
∀X Y, (X ⊆ Y ) = (X ∪ Y = Y )
Definition. 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.
Object . 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 .
Axiom. (
famunionI ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀x y : set , x ∈ X → y ∈ F x → y ∈ ⋃x ∈ X F x
Axiom. (
famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∃x ∈ X , y ∈ F x
Axiom. (
famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∀p : prop , (∀x, x ∈ X → y ∈ F x → p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z )
Let F : set → set ≝ λx ⇒ if P x then x else z
Object . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ X → P x → x ∈ {x ∈ X |P x }
Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X ∧ P x
Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X
Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → P x
Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop , {x ∈ X |P x } ⊆ X
Axiom. (
Sep_In_Power ) We take the following as an axiom:
∀X : set , ∀P : set → prop , {x ∈ X |P x } ∈ 𝒫 X
Object . 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 ).
Axiom. (
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 }
Axiom. (
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
Axiom. (
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
Object . 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 .
Axiom. (
binintersectI ) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
Axiom. (
binintersectE ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
Axiom. (
binintersectE1 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
Axiom. (
binintersectE2 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
Axiom. (
binintersect_Subq_max ) We take the following as an axiom:
∀X Y Z : set , Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
Axiom. (
binintersect_com ) We take the following as an axiom:
∀X Y : set , X ∩ Y = Y ∩ X
Object . 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 .
Axiom. (
setminusI ) We take the following as an axiom:
∀X Y z, (z ∈ X ) → (z ∉ Y ) → z ∈ X ∖ Y
Axiom. (
setminusE ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y ) → z ∈ X ∧ z ∉ Y
Axiom. (
setminusE1 ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y ) → z ∈ X
Axiom. (
setminus_Subq ) We take the following as an axiom:
∀X Y : set , X ∖ Y ⊆ X
Axiom. (
setminus_Subq_contra ) We take the following as an axiom:
∀X Y Z : set , Z ⊆ Y → X ∖ Y ⊆ X ∖ Z
Axiom. (
In_irref ) We take the following as an axiom:
∀x, x ∉ x
Axiom. (
In_no2cycle ) We take the following as an axiom:
∀x y, x ∈ y → y ∈ x → False
Object . The name
ordsucc is a term of type
set → set .
Axiom. (
ordsuccI1 ) We take the following as an axiom:
Axiom. (
ordsuccI2 ) We take the following as an axiom:
Axiom. (
ordsuccE ) We take the following as an axiom:
∀x y : set , y ∈ ordsucc x → y ∈ x ∨ y = x
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (
ordsucc_inj ) We take the following as an axiom:
Axiom. (
In_0_1 ) We take the following as an axiom:
0 ∈ 1
Axiom. (
In_0_2 ) We take the following as an axiom:
0 ∈ 2
Axiom. (
In_1_2 ) We take the following as an axiom:
1 ∈ 2
Definition. 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 .
Axiom. (
nat_0 ) We take the following as an axiom:
Axiom. (
nat_ordsucc ) We take the following as an axiom:
Axiom. (
nat_1 ) We take the following as an axiom:
Axiom. (
nat_2 ) We take the following as an axiom:
Axiom. (
nat_ind ) We take the following as an axiom:
Axiom. (
nat_inv ) We take the following as an axiom:
Axiom. (
nat_complete_ind ) We take the following as an axiom:
∀p : set → prop , (∀n, nat_p n → (∀m ∈ n , p m ) → p n ) → ∀n, nat_p n → p n
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n , m ⊆ n
Axiom. (
cases_1 ) We take the following as an axiom:
∀i ∈ 1 , ∀p : set → prop , p 0 → p i
Axiom. (
cases_2 ) We take the following as an axiom:
∀i ∈ 2 , ∀p : set → prop , p 0 → p 1 → p i
Axiom. (
cases_3 ) We take the following as an axiom:
∀i ∈ 3 , ∀p : set → prop , p 0 → p 1 → p 2 → p i
Axiom. (
neq_0_1 ) We take the following as an axiom:
0 ≠ 1
Axiom. (
neq_1_0 ) We take the following as an axiom:
1 ≠ 0
Axiom. (
neq_0_2 ) We take the following as an axiom:
0 ≠ 2
Axiom. (
neq_2_0 ) We take the following as an axiom:
2 ≠ 0
Axiom. (
neq_1_2 ) We take the following as an axiom:
1 ≠ 2
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Axiom. (
ZF_Repl_closed ) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U , ∀F : set → set , (∀x ∈ X , F x ∈ U ) → {F x |x ∈ X } ∈ U
Object . The name
ω is a term of type
set .
Axiom. (
omega_nat_p ) We take the following as an axiom:
Axiom. (
nat_p_omega ) We take the following as an axiom:
Definition. We define
ordinal to be
λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha , TransSet beta of type
set → prop .
Axiom. (
ordinal_1 ) We take the following as an axiom:
Axiom. (
ordinal_2 ) We take the following as an axiom:
Axiom. (
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
Axiom. (
least_ordinal_ex ) We take the following as an axiom:
∀p : set → prop , (∃alpha, ordinal alpha ∧ p alpha ) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha , ¬ p beta
Definition. 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 .
Definition. 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 .
Axiom. (
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
Axiom. (
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
Object . The name
inv is a term of type
set → (set → set ) → set → set .
Axiom. (
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
Axiom. (
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
Axiom. (
bij_inv ) We take the following as an axiom:
∀X Y, ∀f : set → set , bij X Y f → bij Y X (inv X f )
Axiom. (
bij_id ) We take the following as an axiom:
Axiom. (
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 ) )
Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set , bij X Y f of type
set → set → prop .
Axiom. (
equip_ref ) We take the following as an axiom:
Axiom. (
equip_sym ) We take the following as an axiom:
Axiom. (
equip_tra ) We take the following as an axiom:
Beginning of Section SchroederBernstein
Axiom. (
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
Axiom. (
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
Axiom. (
image_monotone ) We take the following as an axiom:
∀f : set → set , ∀U V, U ⊆ V → {f x |x ∈ U } ⊆ {f x |x ∈ V }
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (
PigeonHole_nat_bij ) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set , (∀i ∈ n , f i ∈ n ) → (∀i j ∈ n , f i = f j → i = j ) → bij n n f
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃n ∈ ω , equip X n of type
set → prop .
Axiom. (
finite_ind ) We take the following as an axiom:
∀p : set → prop , p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y } ) ) → ∀X, finite X → p X
Axiom. (
Subq_finite ) We take the following as an axiom:
Axiom. (
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
Axiom. (
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
Axiom. (
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
Axiom. (
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
Variable P : (set → set ) → prop
Object . The name
Descr_ii is a term of type
set → set .
Hypothesis Pex : ∃f : set → set , P f
Hypothesis Puniq : ∀f g : set → set , P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set ) → prop
Object . The name
Descr_iii is a term of type
set → set → set .
Hypothesis Pex : ∃f : set → set → set , P f
Hypothesis Puniq : ∀f g : set → set → set , P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1 → prop
Object . The name
Descr_Vo1 is a term of type
Vo 1 .
Hypothesis Pex : ∃f : Vo 1 , P f
Hypothesis Puniq : ∀f g : Vo 1 , P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Object . The name
If_ii is a term of type
set → set .
Axiom. (
If_ii_1 ) We take the following as an axiom:
Axiom. (
If_ii_0 ) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Object . The name
If_iii is a term of type
set → set → set .
Axiom. (
If_iii_1 ) We take the following as an axiom:
Axiom. (
If_iii_0 ) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set ) → set
Object . The name
In_rec_i is a term of type
set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
Axiom. (
In_rec_i_eq ) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set ) ) → (set → set )
Object . The name
In_rec_ii is a term of type
set → (set → set ) .
Hypothesis 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
Variable F : set → (set → (set → set → set ) ) → (set → set → set )
Object . The name
In_rec_iii is a term of type
set → (set → set → set ) .
Hypothesis 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
Variable z : set
Variable f : set → set → set
Let F : set → (set → set ) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n ) (g (⋃ n ) ) else z
Axiom. (
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 .
Axiom. (
add_nat_0R ) We take the following as an axiom:
∀n : set , n + 0 = n
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Axiom. (
add_nat_1_1_2 ) We take the following as an axiom:
1 + 1 = 2
Definition. 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 .
Axiom. (
mul_nat_0R ) We take the following as an axiom:
∀n : set , n * 0 = 0
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Definition. We define
Inj1 to be
In_rec_i (λX f ⇒ {0 } ∪ {f x |x ∈ X } ) of type
set → set .
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
∀X y : set , y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X , y = Inj1 x
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ {Inj1 x |x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
∀X y : set , y ∈ Inj0 X → ∃x : set , x ∈ X ∧ y = Inj1 x
Definition. We define
Unj to be
In_rec_i (λX f ⇒ {f x |x ∈ X ∖ {0 } } ) of type
set → set .
Axiom. (
Unj_eq ) We take the following as an axiom:
∀X : set , Unj X = {Unj x |x ∈ X ∖ {0 } }
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
Definition. We define
setsum to be
λX Y ⇒ {Inj0 x |x ∈ X } ∪ {Inj1 y |y ∈ Y } of type
set → set → set .
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Axiom. (
Inj0_setsum ) We take the following as an axiom:
∀X Y x : set , x ∈ X → Inj0 x ∈ X + Y
Axiom. (
Inj1_setsum ) We take the following as an axiom:
∀X Y y : set , y ∈ Y → Inj1 y ∈ X + Y
Axiom. (
setsum_Inj_inv ) We take the following as an axiom:
∀X Y z : set , z ∈ X + Y → (∃x ∈ X , z = Inj0 x ) ∨ (∃y ∈ Y , z = Inj1 y )
Axiom. (
Subq_1_Sing0 ) We take the following as an axiom:
1 ⊆ {0 }
Axiom. (
setsum_0_0 ) We take the following as an axiom:
0 + 0 = 0
Axiom. (
setsum_1_0_1 ) We take the following as an axiom:
1 + 0 = 1
Axiom. (
setsum_1_1_2 ) We take the following as an axiom:
1 + 1 = 2
Beginning of Section pair_setsum
Definition. We define
proj0 to be
λZ ⇒ {Unj z |z ∈ Z , ∃x : set , Inj0 x = z } of type
set → set .
Definition. We define
proj1 to be
λZ ⇒ {Unj z |z ∈ Z , ∃y : set , Inj1 y = z } of type
set → set .
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Axiom. (
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 )
Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Axiom. (
proj0I ) We take the following as an axiom:
∀w u : set , pair 0 u ∈ w → u ∈ proj0 w
Axiom. (
proj0E ) We take the following as an axiom:
∀w u : set , u ∈ proj0 w → pair 0 u ∈ w
Axiom. (
proj1I ) We take the following as an axiom:
∀w u : set , pair 1 u ∈ w → u ∈ proj1 w
Axiom. (
proj1E ) We take the following as an axiom:
∀w u : set , u ∈ proj1 w → pair 1 u ∈ w
Axiom. (
proj0_pair_eq ) We take the following as an axiom:
∀X Y : set , proj0 (pair X Y ) = X
Axiom. (
proj1_pair_eq ) We take the following as an axiom:
∀X Y : set , proj1 (pair X Y ) = Y
Definition. 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 .
Axiom. (
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
Axiom. (
proj_Sigma_eta ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z ∈ (∑x ∈ X , Y x ) , pair (proj0 z ) (proj1 z ) = z
Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → proj0 z ∈ X
Axiom. (
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 )
Axiom. (
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
Axiom. (
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
Definition. 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 .
Let lam : set → (set → set ) → set ≝ Sigma
Definition. 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 ).
Axiom. (
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
Axiom. (
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
Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀x : set , x ∈ X → (λx ∈ X ⇒ F x ) x = F x
Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
Axiom. (
pair_ap_0 ) We take the following as an axiom:
∀x y : set , (pair x y ) 0 = x
Axiom. (
pair_ap_1 ) We take the following as an axiom:
∀x y : set , (pair x y ) 1 = y
Axiom. (
ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → (z 0 ) ∈ X
Axiom. (
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 ) )
Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 ) (u 1 ) = u of type
set → prop .
Axiom. (
pair_p_I ) We take the following as an axiom:
Axiom. (
tuple_pair ) We take the following as an axiom:
∀x y : set , pair x y = (x ,y )
Definition. 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 .
Axiom. (
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
Axiom. (
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 )
Axiom. (
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
Definition. 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 .
Axiom. (
pair_tuple_fun ) We take the following as an axiom:
pair = (λx y ⇒ (x ,y ) )
Axiom. (
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
Variable x0 x1 : set
Axiom. (
tuple_2_0_eq ) We take the following as an axiom:
(x0 ,x1 ) 0 = x0
Axiom. (
tuple_2_1_eq ) We take the following as an axiom:
(x0 ,x1 ) 1 = x1
End of Section Tuples
Axiom. (
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 }
Axiom. (
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
Axiom. (
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
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 .
Object . The name
DescrR_i_io_1 is a term of type
(set → (set → prop ) → prop ) → set .
Object . The name
DescrR_i_io_2 is a term of type
(set → (set → prop ) → prop ) → set → prop .
Axiom. (
DescrR_i_io_12 ) We take the following as an axiom:
∀R : set → (set → prop ) → prop , (∃x, (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) → R (DescrR_i_io_1 R ) (DescrR_i_io_2 R )
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop ) → (set → prop ) → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p p
Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoEq_ alpha q p
Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Definition. We define
PNoLt_ to be
λalpha p q ⇒ ∃beta ∈ alpha , PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type
set → (set → prop ) → (set → prop ) → prop .
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop , ¬ PNoLt_ alpha p p
Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Object . The name
PNoLt is a term of type
set → (set → prop ) → set → (set → prop ) → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop , alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop , ¬ PNoLt alpha p alpha p
Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop ) → set → (set → prop ) → prop .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoLe alpha p alpha q
Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoLe alpha p alpha p
Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Definition. We define
PNo_downc to be
λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , L beta q ∧ PNoLe alpha p beta q of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Definition. We define
PNo_upc to be
λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , R beta q ∧ PNoLe beta q alpha p of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , L alpha p → PNo_downc L alpha p
Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , R alpha p → PNo_upc R alpha p
Axiom. (
PNoLe_upc ) We take the following as an axiom:
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop , L gamma p → ∀delta, ordinal delta → ∀q : set → prop , R delta q → PNoLt gamma p delta q of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → prop .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha )
Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha )
Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop , L beta p → beta ∈ alpha of type
set → (set → (set → prop ) → prop ) → prop .
Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Object . The name
PNo_bd is a term of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set .
Object . The name
PNo_pred is a term of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Part 3
Beginning of Section TaggedSets
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1 }
Notation . We use ' as a postfix operator with priority 100 corresponding to applying term tag .
Proof:
We prove the intermediate claim L1 : 0 ∈ {1 } .
An
exact proof term for the current goal is
H1 1 (SingI 1 ) 0 In_0_1 .
An
exact proof term for the current goal is
SingE 1 0 L1 .
∎
Proof: Assume H1 .
Apply H1 to the current goal.
Assume H2 _ .
∎
Proof: Let y be given.
We prove the intermediate claim L1 : {1 } ∈ y ' .
We will prove {1 } ∈ y ∪ {{1 } } .
An
exact proof term for the current goal is
SingI {1 } .
An
exact proof term for the current goal is
ordinal_Hered (y ' ) H1 {1 } L1 .
∎
Proof: Let alpha and y be given.
Assume H1 H2 .
An
exact proof term for the current goal is
ordinal_Hered alpha H1 (y ' ) H2 .
∎
Proof: Let alpha and beta be given.
Assume Ha He .
Let gamma be given.
Assume Hc : gamma ∈ alpha .
We prove the intermediate
claim L1 :
gamma ∈ beta '.
rewrite the current goal using He (from right to left).
We will prove gamma ∈ alpha ∪ {{1 } } .
An exact proof term for the current goal is Hc .
An exact proof term for the current goal is H1 .
Assume H1 : gamma ∈ {{1 } } .
rewrite the current goal using
SingE {1 } gamma H1 (from right to left).
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb He .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let gamma be given.
Assume H2 : gamma ∈ alpha .
We prove the intermediate
claim L2 :
beta = gamma .
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let alpha and Y be given.
Assume H2 : alpha ∈ {y ' |y ∈ Y } .
Apply ReplE_impred Y (λy ⇒ y ' ) alpha H2 to the current goal.
Let y be given.
Assume H3 : y ∈ Y .
Assume H4 : alpha = y ' .
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1 .
∎
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ {beta ' |beta ∈ alpha } of type
set → set .
Proof: Let alpha and beta be given.
Let x be given.
Assume H2 : x ∈ alpha ∪ {gamma ' |gamma ∈ alpha } .
Apply binunionE alpha {gamma ' |gamma ∈ alpha } x H2 to the current goal.
Assume H3 : x ∈ alpha .
We will
prove x ∈ beta ∪ {gamma ' |gamma ∈ beta } .
Apply H1 to the current goal.
An exact proof term for the current goal is H3 .
Assume H3 : x ∈ {gamma ' |gamma ∈ alpha } .
We will
prove x ∈ beta ∪ {gamma ' |gamma ∈ beta } .
We will
prove x ∈ {gamma ' |gamma ∈ beta } .
Apply ReplE_impred alpha (λgamma ⇒ gamma ' ) x H3 to the current goal.
Let gamma be given.
Assume H4 : gamma ∈ alpha .
Assume H5 : x = gamma ' .
rewrite the current goal using H5 (from left to right).
We will
prove gamma ' ∈ {gamma ' |gamma ∈ beta } .
An
exact proof term for the current goal is
ReplI beta (λgamma ⇒ gamma ' ) gamma (H1 gamma H4 ) .
∎
Definition. We define
PSNo to be
λalpha p ⇒ {beta ∈ alpha |p beta } ∪ {beta ' |beta ∈ alpha , ¬ p beta } of type
set → (set → prop ) → set .
Proof: Let alpha be given.
Let p be given.
Let beta be given.
Apply iffI to the current goal.
An
exact proof term for the current goal is
SepE2 alpha p beta H2 .
Let gamma be given.
Assume Hc : gamma ∈ alpha .
Assume H3 : ¬ p gamma .
We will prove gamma ' ∈ alpha .
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb .
Apply SepI to the current goal.
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNo_PSNo ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let p be given.
Apply andI to the current goal.
Let u be given.
Apply SepE alpha p u H1 to the current goal.
Assume H2 : u ∈ alpha .
Assume H3 : p u .
We will
prove u ∈ alpha ∪ {beta ' |beta ∈ alpha } .
An exact proof term for the current goal is H2 .
Let beta be given.
We will
prove u ∈ alpha ∪ {beta ' |beta ∈ alpha } .
We will
prove u ∈ {beta ' |beta ∈ alpha } .
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
ReplI alpha (λbeta ⇒ beta ' ) beta H2 .
Let beta be given.
Apply xm (p beta ) to the current goal.
Apply SepE alpha p (beta ' ) H4 to the current goal.
Let gamma be given.
Assume H5 : gamma ∈ alpha .
Assume H6 : ¬ p gamma .
We prove the intermediate
claim Lgamma :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma H5 .
We prove the intermediate
claim L1 :
beta = gamma .
An
exact proof term for the current goal is
tagged_eqE_eq beta gamma Lbeta Lgamma H7 .
Apply H6 to the current goal.
We will prove p gamma .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H2 .
An
exact proof term for the current goal is
SepI alpha p beta H1 H2 .
An
exact proof term for the current goal is
ReplSepI alpha (λbeta ⇒ ¬ p beta ) (λbeta ⇒ beta ' ) beta H1 H2 .
Apply SepE alpha p beta H4 to the current goal.
An exact proof term for the current goal is H2 H6 .
Let gamma be given.
Assume H5 : gamma ∈ alpha .
Assume H6 : ¬ p gamma .
rewrite the current goal using H7 (from right to left).
An exact proof term for the current goal is Lbeta .
∎
Proof: Let alpha and x be given.
Assume Ha Hx .
Apply Hx to the current goal.
We will
prove x ⊆ PSNo alpha (λbeta ⇒ beta ∈ x ) .
Let u be given.
Assume Hu : u ∈ x .
Apply binunionE alpha {beta ' |beta ∈ alpha } u (Hx1 u Hu ) to the current goal.
Assume H1 : u ∈ alpha .
We will
prove u ∈ {beta ∈ alpha |beta ∈ x } ∪ {beta ' |beta ∈ alpha , beta ∉ x } .
Apply SepI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hu .
Let beta be given.
We will
prove u ∈ {beta ∈ alpha |beta ∈ x } ∪ {beta ' |beta ∈ alpha , beta ∉ x } .
We will
prove u ∈ {beta ' |beta ∈ alpha , beta ∉ x } .
rewrite the current goal using H3 (from left to right).
We prove the intermediate
claim L2 :
beta ∉ x .
An exact proof term for the current goal is H6 H4 .
Apply H4 to the current goal.
We will
prove (beta ' ) ∈ x .
rewrite the current goal using H3 (from right to left).
We will prove u ∈ x .
An exact proof term for the current goal is Hu .
An
exact proof term for the current goal is
ReplSepI alpha (λbeta ⇒ beta ∉ x ) (λbeta ⇒ beta ' ) beta H2 L2 .
We will
prove PSNo alpha (λbeta ⇒ beta ∈ x ) ⊆ x .
Let u be given.
We will prove u ∈ x .
Apply SepE alpha (λbeta ⇒ beta ∈ x ) u H1 to the current goal.
Assume H2 : u ∈ alpha .
Assume H3 : u ∈ x .
An exact proof term for the current goal is H3 .
Let beta be given.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H3 H5 .
∎
Definition. We define
SNo to be
λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type
set → prop .
Theorem. (
SNo_SNo ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let z be given.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hz .
∎
Proof: Let x, alpha and beta be given.
Assume Ha Hb Hax Hbx .
Let gamma be given.
Assume Hc : gamma ∈ alpha .
We will
prove gamma ∈ beta .
Apply Hax to the current goal.
Assume Hax1 Hax2 .
Apply Hbx to the current goal.
Assume Hbx1 Hbx2 .
We prove the intermediate
claim Lc :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
Apply exactly1of2_or (gamma ' ∈ x ) (gamma ∈ x ) (Hax2 gamma Hc ) to the current goal.
Assume H1 : gamma ' ∈ x .
We prove the intermediate
claim L1 :
gamma ' ∈ beta ∪ {delta ' |delta ∈ beta } .
An exact proof term for the current goal is Hbx1 (gamma ' ) H1 .
We prove the intermediate
claim L2 :
gamma ' ∈ beta ∨ gamma ' ∈ {delta ' |delta ∈ beta } .
An
exact proof term for the current goal is
binunionE beta {delta ' |delta ∈ beta } (gamma ' ) L1 .
Apply L2 to the current goal.
Assume H1 : gamma ∈ x .
We prove the intermediate
claim L1 :
gamma ∈ beta ∪ {delta ' |delta ∈ beta } .
An exact proof term for the current goal is Hbx1 gamma H1 .
We prove the intermediate
claim L2 :
gamma ∈ beta ∨ gamma ∈ {delta ' |delta ∈ beta } .
An
exact proof term for the current goal is
binunionE beta {delta ' |delta ∈ beta } gamma L1 .
Apply L2 to the current goal.
An exact proof term for the current goal is H2 .
∎
Proof: Let x, alpha and beta be given.
Assume Ha Hb Hax Hbx .
∎
Proof: Let x be given.
An
exact proof term for the current goal is
Eps_i_ex (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x ) Hx .
∎
Proof: Let x be given.
Assume Hx .
Assume H1 _ .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoLev_ ) The following is provable:
Proof: Let x be given.
Assume Hx .
Assume _ H1 .
An exact proof term for the current goal is H1 .
∎
Proof: Let x be given.
Assume Hx .
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Hx2 .
∎
Proof: Let alpha be given.
Let p be given.
We prove the intermediate
claim L1 :
SNo_ alpha (PSNo alpha p ) .
An
exact proof term for the current goal is
SNo_PSNo alpha Ha p .
We prove the intermediate
claim L2 :
SNo (PSNo alpha p ) .
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is L1 .
∎
Theorem. (
SNo_Subq ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy H1 H2 .
Apply SNoLev_ x Hx to the current goal.
Apply SNoLev_ y Hy to the current goal.
Let u be given.
Assume Hu : u ∈ x .
An exact proof term for the current goal is Hx2a u Hu .
Apply H2 u H3 to the current goal.
Assume H4 _ .
An exact proof term for the current goal is H4 Hu .
Let beta be given.
We prove the intermediate
claim L3 :
beta ∈ SNoLev y .
An
exact proof term for the current goal is
H1 beta H4 .
We will prove u ∈ y .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H6 .
Apply H9 to the current goal.
Apply H2 beta H4 to the current goal.
Assume _ H10 .
An exact proof term for the current goal is H10 H7 .
Apply H8 to the current goal.
We will
prove beta ' ∈ x .
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is Hu .
∎
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Theorem. (
SNoEq_I ) The following is provable:
Proof: Let alpha, x and y be given.
Assume Hxy .
An exact proof term for the current goal is Hxy .
∎
Theorem. (
SNo_eq ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy H1 H2 .
We will prove x ⊆ y .
Apply SNo_Subq x y Hx Hy to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is H2 .
We will prove y ⊆ x .
Apply SNo_Subq y x Hy Hx to the current goal.
rewrite the current goal using H1 (from left to right).
Let alpha be given.
We will prove alpha ∈ y ↔ alpha ∈ x .
We will prove alpha ∈ x ↔ alpha ∈ y .
Apply H2 alpha to the current goal.
We will
prove alpha ∈ SNoLev x .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is H3 .
∎
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 .
Theorem. (
SNoLtLe ) The following is provable:
∀x y, x < y → x ≤ y
Proof: Let x and y be given.
Assume H1 .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoLeE ) The following is provable:
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
Proof: Let x and y be given.
Assume Hx Hy .
Apply H1 to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
Assume H2 .
Apply H2 to the current goal.
Apply orIR to the current goal.
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H2 H3 .
∎
Proof: Let alpha, x and y be given.
An
exact proof term for the current goal is
PNoEq_sym_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) .
∎
Proof: Let alpha, x, y and z be given.
An
exact proof term for the current goal is
PNoEq_tra_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) (λbeta ⇒ beta ∈ z ) .
∎
Theorem. (
SNoLtE ) The following is provable:
Proof: Let x and y be given.
Let p be given.
Assume Hp1 Hp2 Hp3 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
Let alpha be given.
Assume H3 : alpha ∉ x .
Assume H4 : alpha ∈ y .
We prove the intermediate
claim La :
ordinal alpha .
Set z to be the term
PSNo alpha (λbeta ⇒ beta ∈ x ) .
We prove the intermediate
claim L1 :
SNo_ alpha z .
An exact proof term for the current goal is La .
We prove the intermediate
claim L2 :
SNo z .
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is La .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
SNoLev z = alpha .
An
exact proof term for the current goal is
SNoLev_uniq z (SNoLev z ) alpha Hz1 La Hz2 L1 .
We prove the intermediate
claim L4 :
SNoEq_ alpha z x .
An exact proof term for the current goal is La .
We prove the intermediate
claim L5 :
SNoEq_ alpha z y .
Apply SNoEq_tra_ alpha z x y L4 to the current goal.
We will
prove SNoEq_ alpha x y .
An exact proof term for the current goal is H2 .
Apply Hp1 z L2 to the current goal.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is Ha .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L4 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L5 .
We will prove x < z .
rewrite the current goal using L3 (from left to right).
We will
prove alpha ∈ SNoLev x .
An exact proof term for the current goal is Ha1 .
An exact proof term for the current goal is L4 .
We will prove alpha ∉ x .
An exact proof term for the current goal is H3 .
We will prove z < y .
rewrite the current goal using L3 (from left to right).
We will
prove alpha ∈ SNoLev y .
An exact proof term for the current goal is Ha2 .
An exact proof term for the current goal is L5 .
We will prove alpha ∈ y .
An exact proof term for the current goal is H4 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H3 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H4 .
Apply Hp2 to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
Apply Hp3 to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Theorem. (
SNoLtI2 ) The following is provable:
Proof: Let x and y be given.
Assume H1 H2 H3 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Theorem. (
SNoLtI3 ) The following is provable:
Proof: Let x and y be given.
Assume H1 H2 H3 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1 .
Assume H1 .
Apply H1 to the current goal.
Apply or3I2 to the current goal.
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H2 H3 .
Assume H1 .
Apply or3I3 to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let p be given.
Assume Hp1 Hp2 Hp3 .
Assume H .
Apply H to the current goal.
An exact proof term for the current goal is Hp1 .
An exact proof term for the current goal is Hp2 .
An exact proof term for the current goal is Hp3 .
∎
Theorem. (
SNoLt_tra ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLe_ref ) The following is provable:
Theorem. (
SNoLe_antisym ) The following is provable:
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
Proof: Let x and y be given.
Assume Hx Hy Hxy Hyx .
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H1 H2 .
∎
Theorem. (
SNoLtLe_tra ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLeLt_tra ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLe_tra ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLtLe_or ) The following is provable:
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
Proof: Let x and y be given.
Assume Hx Hy .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : x < y .
Apply orIL to the current goal.
An exact proof term for the current goal is H1 .
Assume H1 : x = y .
Apply orIR to the current goal.
We will prove y ≤ x .
rewrite the current goal using H1 (from left to right).
We will prove y ≤ y .
Assume H1 : y < x .
Apply orIR to the current goal.
We will prove y ≤ x .
An exact proof term for the current goal is H1 .
∎
Proof: Let alpha, beta, p and q be given.
Assume Ha Hb .
rewrite the current goal using
SNoLev_PSNo alpha Ha p (from left to right).
We will
prove PNoEq_ alpha p (λgamma ⇒ gamma ∈ PSNo alpha p ) .
An exact proof term for the current goal is Ha .
We will
prove PNoLt alpha (λgamma ⇒ gamma ∈ PSNo alpha p ) beta q .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha, beta, p and q be given.
Assume Ha Hb .
rewrite the current goal using
SNoLev_PSNo alpha Ha p (from left to right).
We will
prove PNoEq_ alpha (λgamma ⇒ gamma ∈ PSNo alpha p ) p .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Definition. 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 .
Proof: Let L and R be given.
Apply HC to the current goal.
Assume HC .
Apply HC to the current goal.
Assume HLR : ∀x ∈ L , ∀y ∈ R , x < y .
Set L' to be the term
λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L of type
set → (set → prop ) → prop .
Set R' to be the term
λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R of type
set → (set → prop ) → prop .
Set tau to be the term
PNo_bd L' R' .
We prove the intermediate
claim LLR :
PNoLt_pwise L' R' .
Let gamma be given.
Let p be given.
Assume H1 : L' gamma p .
Apply H1 to the current goal.
Assume _ H1 .
Let delta be given.
Let q be given.
Assume H2 : R' delta q .
Apply H2 to the current goal.
Assume _ H2 .
We will
prove PNoLt gamma p delta q .
We will
prove PSNo gamma p < PSNo delta q .
An
exact proof term for the current goal is
HLR (PSNo gamma p ) H1 (PSNo delta q ) H2 .
We prove the intermediate
claim La :
ordinal alpha .
Let x be given.
Assume Hx : x ∈ L .
An exact proof term for the current goal is HL x Hx .
Let y be given.
Assume Hy : y ∈ R .
An exact proof term for the current goal is HR y Hy .
We prove the intermediate
claim Lab :
ordinal (alpha ∪ beta ) .
Assume H1 .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Lb .
Assume H1 .
rewrite the current goal using
binunion_com (from left to right).
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is La .
Let gamma be given.
Let p be given.
Assume H1 .
Apply H1 to the current goal.
We will
prove gamma ∈ alpha ∪ beta .
We will
prove PSNo gamma p ∈ L .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_PSNo gamma H1 p (from left to right).
We will
prove gamma ∈ ordsucc gamma .
Let gamma be given.
Let p be given.
Assume H1 .
Apply H1 to the current goal.
We will
prove gamma ∈ alpha ∪ beta .
We will
prove PSNo gamma p ∈ R .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_PSNo gamma H1 p (from left to right).
We will
prove gamma ∈ ordsucc gamma .
Apply PNo_bd_pred L' R' LLR (alpha ∪ beta ) Lab LLab LRab to the current goal.
Assume H1 .
Apply H1 to the current goal.
Apply H2 to the current goal.
We prove the intermediate
claim LNoC :
SNo (SNoCut L R ) .
We use tau to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim LLleveqtau :
SNoLev (SNoCut L R ) = tau .
We prove the intermediate
claim LLbdtau :
tau ∈ ordsucc (alpha ∪ beta ) .
An
exact proof term for the current goal is
PNo_bd_In L' R' LLR (alpha ∪ beta ) Lab LLab LRab .
rewrite the current goal using LLleveqtau (from left to right).
An exact proof term for the current goal is LLbdtau .
We prove the intermediate
claim LLecw :
PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) w .
We will
prove PNoEq_ tau (λgamma ⇒ gamma ∈ PSNo tau w ) w .
An
exact proof term for the current goal is
PNoEq_PSNo tau H1 w .
An exact proof term for the current goal is LNoC .
We prove the intermediate
claim LL :
∀x ∈ L , x < SNoCut L R .
Let x be given.
Assume Hx : x ∈ L .
We will
prove x < PSNo tau w .
We prove the intermediate
claim L1 :
SNo x .
An exact proof term for the current goal is HL x Hx .
We prove the intermediate
claim L2 :
x = PSNo (SNoLev x ) (λgamma ⇒ gamma ∈ x ) .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
L' (SNoLev x ) (λgamma ⇒ gamma ∈ x ) .
Apply andI to the current goal.
An exact proof term for the current goal is LLx .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hx .
We will
prove x < PSNo tau w .
rewrite the current goal using L2 (from left to right).
We will
prove PNoLt (SNoLev x ) (λgamma ⇒ gamma ∈ x ) tau w .
An
exact proof term for the current goal is
H4 (SNoLev x ) LLx (λgamma ⇒ gamma ∈ x ) L3 .
We prove the intermediate
claim LR :
∀y ∈ R , SNoCut L R < y .
Let y be given.
Assume Hy : y ∈ R .
We will
prove PSNo tau w < y .
We prove the intermediate
claim L1 :
SNo y .
An exact proof term for the current goal is HR y Hy .
We prove the intermediate
claim L2 :
y = PSNo (SNoLev y ) (λgamma ⇒ gamma ∈ y ) .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
R' (SNoLev y ) (λgamma ⇒ gamma ∈ y ) .
Apply andI to the current goal.
An exact proof term for the current goal is LLy .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hy .
We will
prove PSNo tau w < y .
rewrite the current goal using L2 (from left to right).
We will
prove PNoLt tau w (SNoLev y ) (λgamma ⇒ gamma ∈ y ) .
An
exact proof term for the current goal is
H5 (SNoLev y ) LLy (λgamma ⇒ gamma ∈ y ) L3 .
Apply and5I to the current goal.
An exact proof term for the current goal is LNoC .
An exact proof term for the current goal is LLbd .
An exact proof term for the current goal is LL .
An exact proof term for the current goal is LR .
Let z be given.
Assume H10 : ∀x ∈ L , x < z .
Assume H11 : ∀y ∈ R , z < y .
An exact proof term for the current goal is Hz .
Apply andI to the current goal.
Let gamma be given.
Let q be given.
Assume Hq : L' gamma q .
We will
prove PNoLt gamma q (SNoLev z ) (λgamma ⇒ gamma ∈ z ) .
Apply Hq to the current goal.
rewrite the current goal using
SNo_PSNo_eta z Hz (from right to left).
We will
prove PSNo gamma q < z .
An
exact proof term for the current goal is
H10 (PSNo gamma q ) Hq2 .
Let gamma be given.
Let q be given.
Assume Hq : R' gamma q .
We will
prove PNoLt (SNoLev z ) (λgamma ⇒ gamma ∈ z ) gamma q .
Apply Hq to the current goal.
rewrite the current goal using
SNo_PSNo_eta z Hz (from right to left).
We will
prove z < PSNo gamma q .
An
exact proof term for the current goal is
H11 (PSNo gamma q ) Hq2 .
We prove the intermediate
claim LLznt :
SNoLev z ∉ tau .
An
exact proof term for the current goal is
H3 (SNoLev z ) H12 (λgamma ⇒ gamma ∈ z ) Lzimv .
We prove the intermediate
claim LLzlet :
tau ⊆ SNoLev z .
An exact proof term for the current goal is LLznt H12 .
Assume H12 .
An exact proof term for the current goal is H12 .
rewrite the current goal using LLleveqtau (from left to right).
We will
prove tau ⊆ SNoLev z ∧ PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) (λgamma ⇒ gamma ∈ z ) .
Apply andI to the current goal.
An exact proof term for the current goal is LLzlet .
We will
prove PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) (λgamma ⇒ gamma ∈ z ) .
Assume H12 .
Apply H12 to the current goal.
Apply H12 to the current goal.
Let delta be given.
Assume H13 .
Apply H13 to the current goal.
Assume Hd : delta ∈ tau .
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
Assume H14 : ¬ w delta .
Assume H15 : delta ∈ z .
We prove the intermediate
claim Ld :
ordinal delta .
An
exact proof term for the current goal is
ordinal_Hered tau H1 delta Hd .
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop .
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop .
We prove the intermediate claim Lnz0d : ¬ z0 delta .
Assume H10 .
Apply H10 to the current goal.
Assume H11 : delta ∈ z .
Assume H12 : delta ≠ delta .
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d : z1 delta .
We will prove delta ∈ z ∨ delta = delta .
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z ) to the current goal.
Apply andI to the current goal.
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Assume He1 : eps ∈ delta .
Apply iff_trans (w eps ) (eps ∈ z ) (z0 eps ) to the current goal.
An exact proof term for the current goal is H13 eps He1 .
An
exact proof term for the current goal is
PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
Assume He1 : eps = delta .
We will prove w eps ↔ z0 eps .
rewrite the current goal using He1 (from left to right).
We will prove w delta ↔ z0 delta .
Apply iffI to the current goal.
Assume H16 : w delta .
An exact proof term for the current goal is H14 H16 .
Assume H16 : z0 delta .
An exact proof term for the current goal is Lnz0d H16 .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is H2 .
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Assume He1 : eps ∈ delta .
An
exact proof term for the current goal is
PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
Assume He1 : eps = delta .
We will prove eps ∈ z ↔ z1 eps .
rewrite the current goal using He1 (from left to right).
We will prove delta ∈ z ↔ z1 delta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Lz1d .
Assume _ .
An exact proof term for the current goal is H15 .
We will
prove delta ∈ SNoLev z .
Apply LLzlet to the current goal.
We will prove delta ∈ tau .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is Lzimv .
Apply PNoEq_tra_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) w (λgamma ⇒ gamma ∈ z ) to the current goal.
An exact proof term for the current goal is LLecw .
We will
prove PNoEq_ tau w (λgamma ⇒ gamma ∈ z ) .
An exact proof term for the current goal is H12 .
Apply H12 to the current goal.
Let delta be given.
Assume H13 .
Apply H13 to the current goal.
Assume Hd : delta ∈ tau .
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
Assume H14 : delta ∉ z .
Assume H15 : w delta .
We prove the intermediate
claim Ld :
ordinal delta .
An
exact proof term for the current goal is
ordinal_Hered tau H1 delta Hd .
Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop .
Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop .
We prove the intermediate claim Lnz0d : ¬ z0 delta .
Assume H10 .
Apply H10 to the current goal.
Assume H11 : delta ∈ z .
Assume H12 : delta ≠ delta .
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d : z1 delta .
We will prove delta ∈ z ∨ delta = delta .
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z ) to the current goal.
Apply andI to the current goal.
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Assume He1 : eps ∈ delta .
An
exact proof term for the current goal is
PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
Assume He1 : eps = delta .
We will prove eps ∈ z ↔ z0 eps .
rewrite the current goal using He1 (from left to right).
We will prove delta ∈ z ↔ z0 delta .
Apply iffI to the current goal.
Assume H16 : delta ∈ z .
An exact proof term for the current goal is H14 H16 .
Assume H16 : z0 delta .
An exact proof term for the current goal is Lnz0d H16 .
We will
prove delta ∈ SNoLev z .
Apply LLzlet to the current goal.
We will prove delta ∈ tau .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is Lzimv .
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Assume He1 : eps ∈ delta .
Apply iff_trans (w eps ) (eps ∈ z ) (z1 eps ) to the current goal.
An exact proof term for the current goal is H13 eps He1 .
An
exact proof term for the current goal is
PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
Assume He1 : eps = delta .
We will prove w eps ↔ z1 eps .
rewrite the current goal using He1 (from left to right).
We will prove w delta ↔ z1 delta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Lz1d .
Assume _ .
An exact proof term for the current goal is H15 .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume HLR .
Let p be given.
Assume Hp .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
An exact proof term for the current goal is Hp .
∎
Proof: Let L be given.
Assume H1 .
We will
prove (∀x ∈ L , SNo x ) ∧ (∀y ∈ 0 , SNo y ) ∧ (∀x ∈ L , ∀y ∈ 0 , x < y ) .
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
EmptyE y Hy .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
EmptyE y Hy .
∎
Proof: Let R be given.
Assume H1 .
We will
prove (∀x ∈ 0 , SNo x ) ∧ (∀y ∈ R , SNo y ) ∧ (∀x ∈ 0 , ∀y ∈ R , x < y ) .
Apply and3I to the current goal.
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
An exact proof term for the current goal is H1 .
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
∎
Proof:
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
∎
Definition. We define
SNoS_ to be
λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha ) |∃beta ∈ alpha , SNo_ beta x } of type
set → set .
Theorem. (
SNoS_E ) The following is provable:
Proof: Let alpha be given.
Let x be given.
We will
prove ∃beta ∈ alpha , SNo_ beta x .
An
exact proof term for the current goal is
SepE2 (𝒫 (SNoElts_ alpha ) ) (λx ⇒ ∃beta ∈ alpha , SNo_ beta x ) x H1 .
∎
Beginning of Section TaggedSets2
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1 }
Notation . We use ' as a postfix operator with priority 100 corresponding to applying term tag .
Theorem. (
SNoS_I ) The following is provable:
Proof: Let alpha be given.
Let x be given.
Let beta be given.
Apply H1 to the current goal.
We will
prove x ∈ SNoS_ alpha .
We will
prove x ∈ {x ∈ 𝒫 (SNoElts_ alpha ) |∃gamma ∈ alpha , SNo_ gamma x } .
Apply SepI to the current goal.
Apply PowerI to the current goal.
Apply Ha to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 beta Hb .
We will
prove ∃gamma ∈ alpha , SNo_ gamma x .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoS_I2 ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy Hxy .
∎
Theorem. (
SNoS_Subq ) The following is provable:
Proof: Let alpha and beta be given.
Assume Ha Hb Hab .
Let x be given.
Apply SNoS_E alpha Ha x Hx to the current goal.
Let gamma be given.
Assume Hc .
Apply Hc to the current goal.
Assume Hc1 : gamma ∈ alpha .
An
exact proof term for the current goal is
SNoS_I beta Hb x gamma (Hab gamma Hc1 ) Hc2 .
∎
Proof: Let alpha be given.
Assume Ha .
Let x be given.
Assume Hx .
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hx2 .
An exact proof term for the current goal is Hx .
∎
Theorem. (
SNoS_E2 ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Apply SNoS_E alpha Ha x Hx to the current goal.
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
SNo_SNo beta Lb x H1 .
We prove the intermediate
claim Lxb :
SNoLev x = beta .
We prove the intermediate
claim Lxa :
SNoLev x ∈ alpha .
rewrite the current goal using Lxb (from left to right).
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is Hp Lxa Hx1 Lx Hx2 .
∎
Proof: Let w be given.
Let x be given.
Assume Hxw : x = w .
rewrite the current goal using Hxw (from left to right) at position 2.
An exact proof term for the current goal is Hx1 .
∎
Definition. We define
SNoL to be
λz ⇒ {x ∈ SNoS_ (SNoLev z ) |x < z } of type
set → set .
Definition. We define
SNoR to be
λz ⇒ {y ∈ SNoS_ (SNoLev z ) |z < y } of type
set → set .
Proof: Let z be given.
Set L to be the term
SNoL z .
Set R to be the term
SNoR z .
We prove the intermediate
claim L1 :
∀x ∈ L , SNo x .
Let x be given.
Assume Hx : x ∈ L .
We prove the intermediate
claim L1a :
x ∈ SNoS_ (SNoLev z ) .
An
exact proof term for the current goal is
SepE1 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L2 :
∀y ∈ R , SNo y .
Let y be given.
Assume Hy : y ∈ R .
We prove the intermediate
claim L2a :
y ∈ SNoS_ (SNoLev z ) .
An
exact proof term for the current goal is
SepE1 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
We prove the intermediate claim L3 : ∀x ∈ L , ∀y ∈ R , x < y .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Apply SNoLt_tra x z y (L1 x Hx ) Hz (L2 y Hy ) to the current goal.
We will prove x < z .
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
We will prove z < y .
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
We will
prove (∀x ∈ L , SNo x ) ∧ (∀y ∈ R , SNo y ) ∧ (∀x ∈ L , ∀y ∈ R , x < y ) .
Apply and3I to the current goal.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is L3 .
∎
Theorem. (
SNoL_E ) The following is provable:
Proof: Let x be given.
Let w be given.
Let p be given.
Assume Hp .
Assume Hw2 : w < x .
An exact proof term for the current goal is Hp Hw5 Hw3 Hw2 .
∎
Theorem. (
SNoR_E ) The following is provable:
Proof: Let x be given.
Let z be given.
Let p be given.
Assume Hp .
Assume Hz2 : x < z .
An exact proof term for the current goal is Hp Hz5 Hz3 Hz2 .
∎
Theorem. (
SNoL_SNoS ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let w be given.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw3 : w < x .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
∎
Theorem. (
SNoR_SNoS ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let z be given.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz3 : x < z .
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
∎
Theorem. (
SNoL_I ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx Hxz1 Hxz2 .
We will
prove x ∈ SNoL z .
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 x z Hx Hz Hxz1 .
We will prove x < z .
An exact proof term for the current goal is Hxz2 .
∎
Theorem. (
SNoR_I ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let y be given.
Assume Hy Hyz Hzy .
We will
prove y ∈ SNoR z .
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 y z Hy Hz Hyz .
We will prove z < y .
An exact proof term for the current goal is Hzy .
∎
Theorem. (
SNo_eta ) The following is provable:
Proof: Let z be given.
Set L to be the term
SNoL z .
Set R to be the term
SNoR z .
We prove the intermediate
claim LC :
SNoCutP L R .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is H1 .
We prove the intermediate claim L5 : ∀x ∈ L , x < z .
Let x be given.
Assume Hx : x ∈ L .
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
We prove the intermediate claim L6 : ∀y ∈ R , z < y .
Let y be given.
Assume Hy : y ∈ R .
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
Apply H5 z Hz L5 L6 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Apply H4 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
An exact proof term for the current goal is H9 .
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is H8 .
Apply H3 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
An exact proof term for the current goal is H9 .
An exact proof term for the current goal is H8 .
Apply H6 to the current goal.
An exact proof term for the current goal is H8 .
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hz .
An exact proof term for the current goal is L7 .
An exact proof term for the current goal is H7 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Theorem. (
SNoCut_Le ) The following is provable:
Proof: Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2 .
Apply HLR1 to the current goal.
Assume HLR1a .
Apply HLR1a to the current goal.
Assume HLR1c : ∀x ∈ L1 , ∀y ∈ R1 , x < y .
Apply HLR2 to the current goal.
Assume HLR2a .
Apply HLR2a to the current goal.
Assume HLR2c : ∀x ∈ L2 , ∀y ∈ R2 , x < y .
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Let z be given.
We prove the intermediate claim LzL1 : ∀x ∈ L1 , x < z .
Let x be given.
Assume Hx : x ∈ L1 .
Apply SNoLt_tra x (SNoCut L2 R2 ) z (HLR1a x Hx ) H8 Hz1 to the current goal.
We will
prove x < SNoCut L2 R2 .
An exact proof term for the current goal is H1 x Hx .
We will
prove SNoCut L2 R2 < z .
An exact proof term for the current goal is Hz5 .
We prove the intermediate claim LzR1 : ∀y ∈ R1 , z < y .
Let y be given.
Assume Hy : y ∈ R1 .
Apply SNoLt_tra z (SNoCut L1 R1 ) y Hz1 H3 (HLR1b y Hy ) to the current goal.
We will
prove z < SNoCut L1 R1 .
An exact proof term for the current goal is Hz6 .
We will
prove SNoCut L1 R1 < y .
An exact proof term for the current goal is H6 y Hy .
Apply H7 z Hz1 LzL1 LzR1 to the current goal.
Assume _ .
Apply H14 to the current goal.
Set z to be the term
SNoCut L2 R2 .
We prove the intermediate claim LzR1 : ∀y ∈ R1 , z < y .
Let y be given.
Assume Hy : y ∈ R1 .
We will
prove z < SNoCut L1 R1 .
An exact proof term for the current goal is H13 .
We will
prove SNoCut L1 R1 < y .
An exact proof term for the current goal is H6 y Hy .
Apply H7 z H8 H1 LzR1 to the current goal.
Assume _ .
Apply H17 to the current goal.
An exact proof term for the current goal is H14 .
Set z to be the term
SNoCut L1 R1 .
We prove the intermediate claim LzL2 : ∀x ∈ L2 , x < z .
Let x be given.
Assume Hx : x ∈ L2 .
We will
prove x < SNoCut L2 R2 .
An exact proof term for the current goal is H10 x Hx .
We will
prove SNoCut L2 R2 < z .
An exact proof term for the current goal is H13 .
Apply H12 z H3 LzL2 H2 to the current goal.
Assume _ .
Apply H17 to the current goal.
An exact proof term for the current goal is H14 .
An exact proof term for the current goal is H13 .
∎
Proof: Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2 .
We prove the intermediate
claim LNLR1 :
SNo (SNoCut L1 R1 ) .
We prove the intermediate
claim LNLR2 :
SNo (SNoCut L2 R2 ) .
An
exact proof term for the current goal is
SNoCut_Le L1 R1 L2 R2 HLR1 HLR2 H1 H4 .
An
exact proof term for the current goal is
SNoCut_Le L2 R2 L1 R1 HLR2 HLR1 H3 H2 .
∎
Proof: Let x and y be given.
Assume Hx Hy Hxy .
Let p be given.
Assume Hp1 Hp2 Hp3 .
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz1 Hz2 _ _ Hz3 Hz4 _ _ .
Assume Hz2a Hz2b .
Apply Hp1 z to the current goal.
We will
prove z ∈ SNoL y .
An
exact proof term for the current goal is
SNoL_I y Hy z Hz1 Hz2b Hz4 .
We will
prove z ∈ SNoR x .
An
exact proof term for the current goal is
SNoR_I x Hx z Hz1 Hz2a Hz3 .
Assume H1 _ _ .
Apply Hp2 to the current goal.
An
exact proof term for the current goal is
SNoL_I y Hy x Hx H1 Hxy .
Assume H1 _ _ .
Apply Hp3 to the current goal.
An
exact proof term for the current goal is
SNoR_I x Hx y Hy H1 Hxy .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let p be given.
Assume Hp1 Hp2 Hp3 Hp4 Hp5 Hp6 Hp7 .
Assume H1 : x < y .
An exact proof term for the current goal is Hp2 .
An exact proof term for the current goal is Hp3 .
An exact proof term for the current goal is Hp4 .
Assume H1 : x = y .
An exact proof term for the current goal is Hp1 H1 .
Assume H1 : y < x .
Let z be given.
Assume H2 H3 .
An exact proof term for the current goal is Hp5 z H3 H2 .
An exact proof term for the current goal is Hp7 .
An exact proof term for the current goal is Hp6 .
∎
Proof: Let alpha be given.
Apply andI to the current goal.
Let beta be given.
We will
prove beta ∈ alpha ∪ {beta ' |beta ∈ alpha } .
An exact proof term for the current goal is Hb .
Let beta be given.
We will
prove beta ' ∉ alpha .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha be given.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An
exact proof term for the current goal is
ordinal_SNo_ alpha Ha .
∎
Proof: Let alpha be given.
∎
Proof: Let alpha be given.
Let z be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
We will prove z < alpha .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : z < alpha .
An exact proof term for the current goal is H1 .
Assume H1 : z = alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using La2 (from right to left) at position 1.
We will
prove SNoLev alpha ∈ alpha .
rewrite the current goal using H1 (from right to left) at position 1.
We will
prove SNoLev z ∈ alpha .
An exact proof term for the current goal is Hz2 .
Assume H1 : alpha < z .
Apply SNoLtE alpha z La1 Hz H1 to the current goal.
Let w be given.
rewrite the current goal using La2 (from left to right).
Assume H5 : alpha < w .
Assume H6 : w < z .
Apply H7 to the current goal.
rewrite the current goal using La2 (from left to right).
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is H4 H2 .
∎
Proof: Let alpha be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Let x be given.
Apply SNoL_E alpha La1 x Hx to the current goal.
Assume Hx3 : x < alpha .
We will
prove x ∈ SNoS_ alpha .
rewrite the current goal using La2 (from right to left).
Apply SNoS_I2 x alpha Hx1 La1 to the current goal.
An exact proof term for the current goal is Hx2 .
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
We will
prove x ∈ SNoL alpha .
Apply SNoL_I alpha La1 x Hx3 to the current goal.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hx1 .
∎
Proof: Let alpha be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Let x be given.
Apply SNoR_E alpha La1 x Hx to the current goal.
rewrite the current goal using La2 (from left to right).
Assume Hx3 : alpha < x .
Apply SNoLt_tra x alpha x Hx1 La1 Hx1 to the current goal.
We will prove alpha < x .
An exact proof term for the current goal is Hx3 .
∎
Theorem. (
nat_p_SNo ) The following is provable:
Proof: Let n be given.
Assume Hn .
An exact proof term for the current goal is Hn .
∎
Theorem. (
omega_SNo ) The following is provable:
Proof: Let n be given.
Assume Hn .
An exact proof term for the current goal is Hn .
∎
Proof: Let n be given.
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hn .
∎
Proof: Let alpha be given.
Let beta be given.
We prove the intermediate
claim Lb1 :
SNo beta .
rewrite the current goal using Lb2 (from left to right).
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha be given.
Apply Ha to the current goal.
Assume Ha1 _ .
Let z be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
We will prove z ≤ alpha .
We will prove z < alpha .
Apply dneg to the current goal.
Assume H1 : ¬ (z ≤ alpha ) .
Let beta be given.
Apply dneg to the current goal.
Apply H1 to the current goal.
We will prove z < alpha .
We prove the intermediate
claim Lb1 :
SNo beta .
rewrite the current goal using Lb2 (from left to right).
rewrite the current goal using Hz3 (from left to right).
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
rewrite the current goal using Lb2 (from left to right).
Let gamma be given.
We will
prove gamma ∈ z ↔ gamma ∈ beta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Hc .
Assume _ .
We will prove gamma ∈ z .
Apply IH gamma Hc to the current goal.
We will prove gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb2 gamma Hc .
rewrite the current goal using Lb2 (from left to right).
An exact proof term for the current goal is H2 .
We will
prove beta < alpha .
We prove the intermediate claim L2 : alpha ⊆ z .
We prove the intermediate claim L3 : z = alpha .
Apply SNo_eq z alpha Hz La1 to the current goal.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hz3 .
rewrite the current goal using Hz3 (from left to right).
Let beta be given.
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Hb .
Assume _ .
An
exact proof term for the current goal is
L2 beta Hb .
Apply H1 to the current goal.
We will prove z ≤ alpha .
rewrite the current goal using L3 (from left to right).
We will prove alpha ≤ alpha .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb Hab .
We prove the intermediate
claim L1 :
alpha ∈ ordsucc beta .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L1a :
alpha = beta .
An exact proof term for the current goal is Hab .
An exact proof term for the current goal is H1 .
rewrite the current goal using L1a (from left to right).
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is L1 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Assume H1 .
Assume H2 .
An exact proof term for the current goal is H2 .
We will prove alpha < alpha .
We will
prove beta ≤ alpha .
∎
Proof: Let m be given.
Assume Hm .
We will prove 0 ⊆ m .
∎
Theorem. (
SNo_0 ) The following is provable:
Theorem. (
SNo_1 ) The following is provable:
Proof:
An
exact proof term for the current goal is
nat_1 .
∎
Theorem. (
SNo_2 ) The following is provable:
Proof:
An
exact proof term for the current goal is
nat_2 .
∎
Theorem. (
SNoLev_0 ) The following is provable:
Proof:
rewrite the current goal using
binunion_idl 0 (from left to right).
Assume _ _ _ .
We prove the intermediate
claim L1 :
SNoLev (SNoCut 0 0 ) = 0 .
We will prove 0 = 0 .
Use reflexivity.
Use transitivity with and 0 .
An exact proof term for the current goal is L1 .
Use symmetry.
An
exact proof term for the current goal is
SNoLev_0 .
rewrite the current goal using L1 (from left to right).
Let beta be given.
An
exact proof term for the current goal is
EmptyE beta Hb .
∎
Theorem. (
SNoL_0 ) The following is provable:
Proof:
Let z be given.
We prove the intermediate
claim Lz :
z ∈ SNoS_ 0 .
rewrite the current goal using
SNoLev_0 (from right to left).
An
exact proof term for the current goal is
SNoL_SNoS_ 0 z Hz .
An
exact proof term for the current goal is
EmptyE (SNoLev z ) Hz1 .
∎
Theorem. (
SNoR_0 ) The following is provable:
Proof:
Let z be given.
We prove the intermediate
claim Lz :
z ∈ SNoS_ 0 .
rewrite the current goal using
SNoLev_0 (from right to left).
An
exact proof term for the current goal is
SNoR_SNoS_ 0 z Hz .
An
exact proof term for the current goal is
EmptyE (SNoLev z ) Hz1 .
∎
Theorem. (
SNoL_1 ) The following is provable:
Proof:
Let x be given.
We will prove x ∈ 1 .
Assume _ .
We prove the intermediate claim L1 : 0 = x .
rewrite the current goal using
SNoLev_0 (from left to right).
We will prove 0 = 0 .
Use reflexivity.
rewrite the current goal using
SNoLev_0 (from left to right).
Let beta be given.
An
exact proof term for the current goal is
EmptyE beta Hb .
rewrite the current goal using L1 (from right to left).
An
exact proof term for the current goal is
In_0_1 .
Let x be given.
Assume Hx : x ∈ 1 .
We will
prove x ∈ SNoL 1 .
Apply cases_1 x Hx (λx ⇒ x ∈ SNoL 1 ) to the current goal.
We will
prove 0 ∈ SNoL 1 .
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
In_0_1 .
∎
Theorem. (
SNoR_1 ) The following is provable:
Proof: Let x be given.
We prove the intermediate
claim LLx2 :
SNo (SNoLev x ) .
We prove the intermediate
claim L3 :
x ≤ SNoLev x .
Let z be given.
Assume Hz4 : x < z .
Apply SNoLt_tra z x z Hz Hx Hz to the current goal.
We will prove z < x .
Apply H2 to the current goal.
An exact proof term for the current goal is Hz7 .
An exact proof term for the current goal is Hz .
We will prove x < z .
An exact proof term for the current goal is Hz4 .
An exact proof term for the current goal is H4 .
An exact proof term for the current goal is H4 .
Use symmetry.
An exact proof term for the current goal is H3 .
∎
Proof: Let x be given.
rewrite the current goal using
SNo_max_SNoLev x Hx H2 (from right to left).
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
Set p to be the term λdelta ⇒ delta ∈ x ∧ delta ≠ alpha of type set → prop .
Assume _ .
Assume H4 : alpha ≠ alpha .
Apply H4 to the current goal.
Use reflexivity.
Let beta be given.
rewrite the current goal using H5 (from right to left).
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
Set p to be the term λdelta ⇒ delta ∈ x ∨ delta = alpha of type set → prop .
Apply SepI to the current goal.
We will
prove alpha ∈ ordsucc alpha .
We will prove alpha ∈ x ∨ alpha = alpha .
Apply orIR to the current goal.
Use reflexivity.
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
Set p to be the term
λbeta ⇒ beta ∈ x of type
set → prop .
Set q to be the term
λbeta ⇒ beta ∈ x ∧ beta ≠ alpha of type
set → prop .
We will
prove PNoEq_ alpha q p .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
Set p to be the term
λbeta ⇒ beta ∈ x of type
set → prop .
Set q to be the term
λbeta ⇒ beta ∈ x ∨ beta = alpha of type
set → prop .
We will
prove PNoEq_ alpha q p .
∎
Proof: Let x be given.
Assume Hx Hx0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is Hx0 .
rewrite the current goal using Hx0 (from left to right).
Let alpha be given.
Assume Ha : alpha ∈ 0 .
An
exact proof term for the current goal is
EmptyE alpha Ha .
∎
Definition. We define
eps_ to be
λn ⇒ {0 } ∪ {(ordsucc m ) ' |m ∈ n } of type
set → set .
Proof: Let n and alpha be given.
Assume Ha .
Assume H2 : alpha ∈ {0 } .
An
exact proof term for the current goal is
SingE 0 alpha H2 .
Let m be given.
Assume Hm : m ∈ n .
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is Ha .
∎
Theorem. (
eps_0_1 ) The following is provable:
Proof:
Let x be given.
Assume Hx : x ∈ {0 } .
rewrite the current goal using
SingE 0 x Hx (from left to right).
We will prove 0 ∈ 1 .
An
exact proof term for the current goal is
In_0_1 .
Let m be given.
Assume Hm : m ∈ 0 .
An
exact proof term for the current goal is
EmptyE m Hm .
Let x be given.
Assume Hx : x ∈ 1 .
Apply cases_1 x Hx (λx ⇒ x ∈ eps_ 0 ) to the current goal.
We will
prove 0 ∈ {0 } ∪ {(ordsucc m ) ' |m ∈ 0 } .
Apply SingI to the current goal.
∎
Theorem. (
SNo__eps_ ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
Apply andI to the current goal.
Let x be given.
Assume Hx : x ∈ {0 } .
rewrite the current goal using
SingE 0 x Hx (from left to right).
Let m be given.
Assume Hm : m ∈ n .
rewrite the current goal using Hxm (from left to right).
Let m be given.
We prove the intermediate
claim Lm :
nat_p m .
Apply nat_inv m Lm to the current goal.
Assume Hm : m = 0 .
rewrite the current goal using Hm (from left to right).
We will
prove 0 ' ∉ eps_ n .
Assume H2 : 0 ' ∈ {0 } .
Apply EmptyE {1 } to the current goal.
We will prove {1 } ∈ 0 .
rewrite the current goal using
SingE 0 (0 ' ) H2 (from right to left) at position 2.
We will prove {1 } ∈ 0 ' .
We will prove {1 } ∈ 0 ∪ {{1 } } .
We will prove {1 } ∈ {{1 } } .
Apply SingI to the current goal.
Let m be given.
Assume Hm : m ∈ n .
An exact proof term for the current goal is H3 .
We will
prove 0 ∈ eps_ n .
We will
prove 0 ∈ {0 } ∪ {(ordsucc m ) ' |m ∈ n } .
An
exact proof term for the current goal is
SingI 0 .
Assume H1 .
Apply H1 to the current goal.
Let k be given.
Assume H1 .
Apply H1 to the current goal.
We prove the intermediate
claim Lm :
nat_p m .
rewrite the current goal using Hmk (from left to right).
An
exact proof term for the current goal is
nat_ordsucc k Hk .
rewrite the current goal using Hmk (from right to left).
An exact proof term for the current goal is Hm .
We prove the intermediate claim Lk : k ∈ n .
rewrite the current goal using H2 (from right to left).
We will
prove m ' ∈ eps_ n .
We will
prove m ' ∈ {0 } ∪ {(ordsucc m ) ' |m ∈ n } .
rewrite the current goal using Hmk (from left to right).
An
exact proof term for the current goal is
ReplI n (λk ⇒ (ordsucc k ) ' ) k Lk .
We will
prove m ∉ eps_ n .
Assume H2 : m ∈ {0 } .
Apply EmptyE 0 to the current goal.
We will prove 0 ∈ 0 .
rewrite the current goal using
SingE 0 m H2 (from right to left) at position 2.
We will prove 0 ∈ m .
rewrite the current goal using Hmk (from left to right).
Let j be given.
Assume Hj : j ∈ n .
rewrite the current goal using Hmj (from right to left).
∎
Theorem. (
SNo_eps_ ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
∎
Theorem. (
SNo_eps_1 ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
∎
Proof: Let n be given.
Assume Hn .
An
exact proof term for the current goal is
SNo__eps_ n Hn .
∎
Proof: Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
We prove the intermediate
claim Lnn :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim Lmn :
nat_p m .
An
exact proof term for the current goal is
nat_p_trans n Lnn m Hm .
We prove the intermediate
claim Lm :
m ∈ ω .
An
exact proof term for the current goal is
nat_p_omega m Lmn .
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
Let k be given.
We prove the intermediate
claim Lk :
ordinal k .
Apply iffI to the current goal.
We will
prove 0 ∈ eps_ m .
We will
prove 0 ∈ {0 } ∪ {(ordsucc j ) ' |j ∈ m } .
Apply SingI to the current goal.
We will
prove 0 ∈ eps_ n .
We will
prove 0 ∈ {0 } ∪ {(ordsucc j ) ' |j ∈ n } .
Apply SingI to the current goal.
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
∎
Proof: Let n be given.
Assume Hn .
rewrite the current goal using
SNoLev_0 (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_0 (from left to right).
Let alpha be given.
Assume Ha : alpha ∈ 0 .
An
exact proof term for the current goal is
EmptyE alpha Ha .
rewrite the current goal using
SNoLev_0 (from left to right).
We will
prove 0 ∈ eps_ n .
We will
prove 0 ∈ {0 } ∪ {(ordsucc m ) ' |m ∈ n } .
Apply SingI to the current goal.
∎
Proof: Let n be given.
Let x be given.
Assume Hxpos : 0 < x .
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We will
prove eps_ n < x .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_eps_ n Ln (from right to left) at position 1.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Hx1 .
Let z be given.
Assume Hz5 : x < z .
We prove the intermediate claim Lz0 : z = 0 .
We will prove x < x .
Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.
We will prove z < x .
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos .
We prove the intermediate claim Lx0 : x = 0 .
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos .
rewrite the current goal using
SNoLev_eps_ n Ln (from left to right).
∎
Proof: Let n be given.
Assume Hn .
Let x be given.
Assume Hxpos : 0 < x .
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We will
prove eps_ n ≤ x .
Let z be given.
Assume Hz5 : x < z .
We prove the intermediate claim Lz0 : z = 0 .
We will prove x < x .
Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.
We will prove z < x .
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos .
We prove the intermediate claim Lx0 : x = 0 .
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos .
rewrite the current goal using
SNoLev_eps_ n Ln (from left to right).
rewrite the current goal using H4 (from left to right) at position 1.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H2 .
∎
Proof: Let n be given.
Assume Hn .
Let x be given.
Assume Hx2 : 0 < x .
An exact proof term for the current goal is Hx1a .
We prove the intermediate claim L2 : x = 0 .
An
exact proof term for the current goal is
SNoLev_0_eq_0 x Hx1c H1 .
rewrite the current goal using L2 (from left to right) at position 1.
An exact proof term for the current goal is Hx2 .
Assume H1 .
Apply H1 to the current goal.
Let m be given.
Assume H1 .
Apply H1 to the current goal.
We use m to witness the existential quantifier.
Apply andI to the current goal.
We will prove m ∈ n .
rewrite the current goal using Hm2 (from left to right).
We will
prove x = eps_ m .
An exact proof term for the current goal is Hm2 .
An exact proof term for the current goal is Hx3 .
rewrite the current goal using Hm2 (from left to right).
Let k be given.
We prove the intermediate
claim L3 :
ordinal k .
Apply iffI to the current goal.
We will
prove 0 ∈ eps_ m .
Apply SingI to the current goal.
We will
prove 0 ∈ eps_ n .
Apply SingI to the current goal.
∎
Proof: Let n be given.
Assume Hn .
Set L to be the term {0 } .
Set R to be the term
{eps_ m |m ∈ n } .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀z ∈ R , SNo z ) ∧ (∀w ∈ L , ∀z ∈ R , w < z ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_0 .
Let z be given.
Assume Hz .
Let m be given.
Assume Hm1 : m ∈ n .
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
nat_p_trans n Ln m Hm1 .
Let w be given.
Assume Hw .
Let z be given.
Assume Hz .
Let m be given.
Assume Hm1 : m ∈ n .
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using Hm2 (from left to right).
We will
prove 0 < eps_ m .
An
exact proof term for the current goal is
nat_p_trans n Ln m Hm1 .
∎
Proof: Let n be given.
Assume Hn .
Set L to be the term {0 } .
Set R to be the term
{eps_ m |m ∈ n } .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim L1 :
SNoCutP L R .
An
exact proof term for the current goal is
eps_SNoCutP n Hn .
We prove the intermediate
claim LRS :
∀z ∈ R , SNo z .
Apply L1 to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim L2 :
(⋃x ∈ L ordsucc (SNoLev x ) ) = 1 .
Let k be given.
Assume Hk .
Let w be given.
Assume Hw : w ∈ L .
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using
SNoLev_0 (from left to right).
Assume H2 : k ∈ 1 .
We will prove k ∈ 1 .
An exact proof term for the current goal is H2 .
Let i be given.
Assume Hi .
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
In_0_1 .
Assume Hn0 : n ≠ 0 .
Let k be given.
Assume Hk .
Let z be given.
Assume Hz : z ∈ R .
Let m be given.
Assume Hm1 : m ∈ n .
rewrite the current goal using Hm2 (from left to right).
An exact proof term for the current goal is Ln .
An exact proof term for the current goal is Hm1 .
Apply L3b to the current goal.
An exact proof term for the current goal is H3 .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is L3a .
Let i be given.
Apply nat_inv n Ln to the current goal.
Assume H2 : n = 0 .
An exact proof term for the current goal is Hn0 H2 .
Assume H2 .
Apply H2 to the current goal.
Let n' be given.
Assume H2 .
Apply H2 to the current goal.
We will
prove eps_ n' ∈ R .
Apply ReplI to the current goal.
We will prove n' ∈ n .
rewrite the current goal using Hn'2 (from left to right).
rewrite the current goal using Hn'2 (from right to left).
An exact proof term for the current goal is Hi .
Apply xm (n = 0 ) to the current goal.
Assume H2 : n = 0 .
We prove the intermediate claim L4a : R = 0 .
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using H2 (from left to right).
Assume Hm1 : m ∈ 0 .
An
exact proof term for the current goal is
EmptyE m Hm1 .
rewrite the current goal using L4a (from left to right).
rewrite the current goal using
binunion_idr (from left to right).
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is L2 .
Assume H2 : n ≠ 0 .
rewrite the current goal using L3 H2 (from right to left).
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 H2 (from left to right).
Let i be given.
Assume Hi .
An exact proof term for the current goal is Ln .
rewrite the current goal using L4 (from left to right).
We prove the intermediate
claim L5 :
SNo (eps_ n ) .
An
exact proof term for the current goal is
SNo_eps_ n Hn .
We prove the intermediate
claim L6 :
∀w ∈ L , w < eps_ n .
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
We will
prove 0 < eps_ n .
An
exact proof term for the current goal is
SNo_eps_pos n Hn .
We prove the intermediate
claim L7 :
∀z ∈ R , eps_ n < z .
Let z be given.
Assume Hz .
Let m be given.
Assume Hm1 : m ∈ n .
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
SNo_eps_decr n Hn m Hm1 .
Apply H5 (eps_ n ) L5 L6 L7 to the current goal.
Use symmetry.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
We prove the intermediate
claim L8 :
eps_ n < SNoCut L R .
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
Apply H3 to the current goal.
Apply SingI to the current goal.
Let z be given.
We prove the intermediate claim L9 : ∀w ∈ L , w < z .
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
We will prove 0 < z .
An
exact proof term for the current goal is
SNo_eps_pos n Hn .
An exact proof term for the current goal is Hz5 .
We prove the intermediate claim L10 : ∀v ∈ R , z < v .
Let v be given.
Assume Hv .
Apply SNoLt_tra z (SNoCut L R ) v Hz1 H1 (LRS v Hv ) Hz6 to the current goal.
Apply H4 to the current goal.
An exact proof term for the current goal is Hv .
Apply H5 z Hz1 L9 L10 to the current goal.
Apply H9 to the current goal.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
We prove the intermediate
claim L11 :
∃m ∈ n , SNoCut L R = eps_ m .
An exact proof term for the current goal is H9 .
An exact proof term for the current goal is H1 .
Apply H3 to the current goal.
Apply SingI to the current goal.
An exact proof term for the current goal is H10 .
Apply L11 to the current goal.
Let m be given.
Assume H12 .
Apply H12 to the current goal.
Assume Hm1 : m ∈ n .
rewrite the current goal using Hm2 (from right to left) at position 1.
Apply H4 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hm1 .
An exact proof term for the current goal is H8 .
An exact proof term for the current goal is H7 .
∎
End of Section TaggedSets2
Theorem. (
SNo_etaE ) The following is provable:
Proof: Let z be given.
Let p be given.
Assume H1 .
We prove the intermediate
claim L1 :
z = SNoCut L R .
An
exact proof term for the current goal is
SNo_eta z Hz .
We prove the intermediate
claim LL :
∀x, x ∈ L → SNo x ∧ SNoLev x ∈ SNoLev z ∧ x < z .
Let x be given.
Assume Hx : x ∈ L .
Assume Hx2 : x < z .
Let beta be given.
Assume Hx3 .
Apply Hx3 to the current goal.
We prove the intermediate
claim Lx1 :
SNo x .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb .
An exact proof term for the current goal is Hx3 .
We prove the intermediate
claim Lx2 :
SNoLev x = beta .
An exact proof term for the current goal is Hx4 .
An exact proof term for the current goal is Lb .
Apply Hx5 to the current goal.
An exact proof term for the current goal is Hx3 .
rewrite the current goal using Lx2 (from left to right).
An exact proof term for the current goal is Hb .
Apply and3I to the current goal.
An exact proof term for the current goal is Lx1 .
An exact proof term for the current goal is Lx3 .
We will prove x < z .
An exact proof term for the current goal is Hx2 .
We prove the intermediate
claim LR :
∀y, y ∈ R → SNo y ∧ SNoLev y ∈ SNoLev z ∧ z < y .
Let y be given.
Assume Hy : y ∈ R .
Assume Hy2 : z < y .
Let beta be given.
Assume Hy3 .
Apply Hy3 to the current goal.
We prove the intermediate
claim Ly1 :
SNo y .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb .
An exact proof term for the current goal is Hy3 .
We prove the intermediate
claim Ly2 :
SNoLev y = beta .
An exact proof term for the current goal is Hy4 .
An exact proof term for the current goal is Lb .
Apply Hy5 to the current goal.
An exact proof term for the current goal is Hy3 .
rewrite the current goal using Ly2 (from left to right).
An exact proof term for the current goal is Hb .
Apply and3I to the current goal.
An exact proof term for the current goal is Ly1 .
An exact proof term for the current goal is Ly3 .
We will prove z < y .
An exact proof term for the current goal is Hy2 .
Apply H1 L R to the current goal.
We will
prove (∀x ∈ L , SNo x ) ∧ (∀y ∈ R , SNo y ) ∧ (∀x ∈ L , ∀y ∈ R , x < y ) .
Apply and3I to the current goal.
Let x be given.
Assume Hx .
Apply LL x Hx to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Let y be given.
Assume Hy .
Apply LR y Hy to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Apply LL x Hx to the current goal.
Assume H2 .
Apply H2 to the current goal.
Assume H4 : x < z .
Apply LR y Hy to the current goal.
Assume H5 .
Apply H5 to the current goal.
Assume H7 : z < y .
An
exact proof term for the current goal is
SNoLt_tra x z y H2 Hz H5 H4 H7 .
Let x be given.
Assume Hx .
Apply LL x Hx to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
Let y be given.
Assume Hy .
Apply LR y Hy to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
An exact proof term for the current goal is L1 .
∎
Theorem. (
SNo_ind ) The following is provable:
∀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
Proof: Let P be given.
Assume H1 .
We prove the intermediate
claim L1 :
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → P z .
Let alpha be given.
Let z be given.
We will prove P z .
Apply SNo_etaE z Hz to the current goal.
Let L and R be given.
Apply H2 to the current goal.
Assume H6 .
Apply H6 to the current goal.
Assume H8 : ∀x ∈ L , ∀y ∈ R , x < y .
rewrite the current goal using H5 (from left to right).
Apply H1 to the current goal.
An exact proof term for the current goal is H2 .
We will prove ∀x, x ∈ L → P x .
Let x be given.
Assume Hx : x ∈ L .
Apply IH (SNoLev z ) Hz2 x to the current goal.
An exact proof term for the current goal is H6 x Hx .
An exact proof term for the current goal is H3 x Hx .
We will prove ∀y, y ∈ R → P y .
Let y be given.
Assume Hy : y ∈ R .
Apply IH (SNoLev z ) Hz2 y to the current goal.
An exact proof term for the current goal is H7 y Hy .
An exact proof term for the current goal is H4 y Hy .
Let z be given.
An exact proof term for the current goal is Hz .
∎
Beginning of Section SurrealRecI
Variable F : set → (set → set ) → set
Let G : set → (set → set → set ) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha ) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) (λz : set ⇒ default )
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
Proof: Let z be given.
We prove the intermediate claim L1 : ∀alpha, ∀g h : set → set → set , (∀x ∈ alpha , g x = h x ) → G alpha g = G alpha h .
Let alpha, g and h be given.
Assume Hgh : ∀x ∈ alpha , g x = h x .
We will prove G alpha g = G alpha h .
Apply xm (ordinal alpha ) to the current goal.
rewrite the current goal using
If_ii_1 (ordinal alpha ) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ h (SNoLev w ) w ) else default ) (λz : set ⇒ default ) H1 (from left to right).
rewrite the current goal using
If_ii_1 (ordinal alpha ) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) (λz : set ⇒ default ) H1 (from left to right).
We will
prove (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) = (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ h (SNoLev w ) w ) else default ) .
Apply func_ext set set to the current goal.
Let z be given.
rewrite the current goal using
If_i_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
If_i_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
Apply Fr to the current goal.
An exact proof term for the current goal is Hz3 .
Let w be given.
We prove the intermediate
claim LLw :
SNoLev w ∈ alpha .
Apply H1 to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev z ) H2 (SNoLev w ) Hw1 .
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hw1 .
rewrite the current goal using
Hgh (SNoLev w ) LLw (from left to right).
Use reflexivity.
rewrite the current goal using
If_i_0 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
If_ii_0 (ordinal alpha ) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ h (SNoLev w ) w ) else default ) (λz : set ⇒ default ) H1 (from left to right).
An
exact proof term for the current goal is
If_ii_0 (ordinal alpha ) (λz ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) (λz : set ⇒ default ) H1 .
rewrite the current goal using
In_rec_ii_eq G L1 (from left to right).
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set ) ) → (set → set )
Let G : set → (set → set → (set → set ) ) → set → (set → set ) ≝ λalpha g ⇒ If_iii (ordinal alpha ) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default ) (λz : set ⇒ default )
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set ) , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
Proof: Let z be given.
We prove the intermediate claim L1 : ∀alpha, ∀g h : set → set → (set → set ) , (∀x ∈ alpha , g x = h x ) → G alpha g = G alpha h .
Let alpha, g and h be given.
Assume Hgh : ∀x ∈ alpha , g x = h x .
We will prove G alpha g = G alpha h .
Apply xm (ordinal alpha ) to the current goal.
Apply func_ext set (set → set ) to the current goal.
Let z be given.
rewrite the current goal using
If_ii_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
If_ii_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
Apply Fr to the current goal.
An exact proof term for the current goal is Hz3 .
Let w be given.
We prove the intermediate
claim LLw :
SNoLev w ∈ alpha .
Apply H1 to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev z ) H2 (SNoLev w ) Hw1 .
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hw1 .
rewrite the current goal using
Hgh (SNoLev w ) LLw (from left to right).
Use reflexivity.
rewrite the current goal using
If_ii_0 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
In_rec_iii_eq G L1 (from left to right).
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set ) → set
Let G : set → (set → set → set ) → set → (set → set ) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y )
Let H : set → (set → set → set ) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f ) z else Empty
Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , ∀y, SNo y → g x y = h x y ) → (∀y ∈ SNoS_ (SNoLev z ) , g w y = h w y ) → F w z g = F w z h
Theorem. (
SNo_rec2_G_prop ) The following is provable:
∀w, SNo w → ∀f k : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , f x = k x ) → ∀z, SNo z → ∀g h : set → set , (∀u ∈ SNoS_ (SNoLev z ) , g u = h u ) → G w f z g = G w k z h
Proof: Let w be given.
Let f and k be given.
Let z be given.
Let g and h be given.
We will prove G w f z g = G w k z h .
We will prove F w z (λx y ⇒ if x = w then g y else f x y ) = F w z (λx y ⇒ if x = w then h y else k x y ) .
Apply Fr to the current goal.
An exact proof term for the current goal is Hw .
An exact proof term for the current goal is Hz .
Let x be given.
Let y be given.
We will prove (if x = w then g y else f x y ) = (if x = w then h y else k x y ) .
We prove the intermediate claim Lxw : x ≠ w .
An
exact proof term for the current goal is
SNoS_In_neq w Hw x Hx .
rewrite the current goal using
If_i_0 (x = w ) (g y ) (f x y ) Lxw (from left to right).
rewrite the current goal using
If_i_0 (x = w ) (h y ) (k x y ) Lxw (from left to right).
We will prove f x y = k x y .
rewrite the current goal using Hfk x Hx (from left to right).
Use reflexivity.
Let y be given.
We will prove (if w = w then g y else f w y ) = (if w = w then h y else k w y ) .
rewrite the current goal using
If_i_1 (w = w ) (g y ) (f w y ) (λq H ⇒ H ) (from left to right).
rewrite the current goal using
If_i_1 (w = w ) (h y ) (k w y ) (λq H ⇒ H ) (from left to right).
We will prove g y = h y .
An exact proof term for the current goal is Hgh y Hy .
∎
Proof: Let w be given.
Let f be given.
We prove the intermediate
claim L1 :
∀z, SNo z → ∀g h : set → set , (∀u ∈ SNoS_ (SNoLev z ) , g u = h u ) → G w f z g = G w f z h .
Let z be given.
Assume Hz .
Let g and h be given.
Assume Hgh .
We prove the intermediate
claim L1a :
∀x ∈ SNoS_ (SNoLev w ) , f x = f x .
Let x be given.
Assume Hx .
Use reflexivity.
An
exact proof term for the current goal is
SNo_rec2_G_prop w Hw f f L1a z Hz g h Hgh .
An
exact proof term for the current goal is
SNo_rec_i_eq (G w f ) L1 .
∎
Proof: Let w be given.
Let z be given.
We prove the intermediate
claim L1 :
∀w, SNo w → ∀g h : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , g x = h x ) → H w g = H w h .
Let w be given.
Let g and h be given.
We will prove H w g = H w h .
Apply func_ext set set to the current goal.
Let z be given.
Apply xm (SNo z ) to the current goal.
Let alpha be given.
Let z be given.
Apply SNoS_E2 alpha Ha z Hz to the current goal.
rewrite the current goal using
SNo_rec2_eq_1 w Hw g z Hz3 (from left to right).
rewrite the current goal using
SNo_rec2_eq_1 w Hw h z Hz3 (from left to right).
Let y be given.
An
exact proof term for the current goal is
IH (SNoLev z ) Hz1 y Hy .
Let x be given.
Let y be given.
We prove the intermediate claim Lxw : x ≠ w .
An
exact proof term for the current goal is
SNoS_In_neq w Hw x Hx .
Let y be given.
We prove the intermediate
claim Ly :
SNo y .
An exact proof term for the current goal is Hy3 .
rewrite the current goal using
SNo_rec_ii_eq H L1 w Hw (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
rewrite the current goal using
SNo_rec_ii_eq H L1 w Hw (from left to right).
An exact proof term for the current goal is L2 .
∎
End of Section SurrealRec2
Proof: Let P be given.
Assume H1 .
Let x be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
H1 (ordsucc (SNoLev x ) ) LsLx x LxsLx .
∎
Proof: Let P be given.
Assume H1 .
Let x and y be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
SNoS_SNoLev y Hy .
∎
Proof: Let P be given.
Assume H1 .
Let x, y and z be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
SNoS_SNoLev y Hy .
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
Proof: Let P be given.
We prove the intermediate
claim L1 :
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha , P x .
Let alpha be given.
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply H1 x Hx3 to the current goal.
An
exact proof term for the current goal is
IH (SNoLev x ) Hx1 .
∎
Proof: Let P be given.
Let alpha be given.
Let beta be given.
Let x be given.
Let y be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply H1 x y Hx3 Hy3 to the current goal.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb w Hw y Hy .
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 x Hx .
Let w be given.
Let z be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 w Hw z Hz .
∎
Theorem. (
SNoLev_ind3 ) The following is provable:
∀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
Proof: Let P be given.
Let alpha be given.
Let beta be given.
Let gamma be given.
Let x be given.
Let y be given.
Let z be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply SNoS_E2 gamma Hc z Hz to the current goal.
Apply H1 x y z Hx3 Hy3 Hz3 to the current goal.
Let u be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb gamma Hc u Hu y Hy z Hz .
Let v be given.
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 gamma Hc x Hx v Hv z Hz .
An
exact proof term for the current goal is
IHc (SNoLev z ) Hz1 x Hx y Hy .
Let u be given.
Let v be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 gamma Hc u Hu v Hv z Hz .
Let u be given.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb (SNoLev z ) Hz2 u Hu y Hy w Hw .
Let v be given.
Let w be given.
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 (SNoLev z ) Hz2 x Hx v Hv w Hw .
Let u be given.
Let v be given.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 (SNoLev z ) Hz2 u Hu v Hv w Hw .
∎
Theorem. (
SNo_omega ) The following is provable:
Theorem. (
SNoLt_0_1 ) The following is provable:
0 < 1
Proof:
We will prove 0 ∈ 1 .
An
exact proof term for the current goal is
In_0_1 .
∎
Theorem. (
SNoLt_0_2 ) The following is provable:
0 < 2
Proof:
We will prove 0 ∈ 2 .
An
exact proof term for the current goal is
In_0_2 .
∎
Theorem. (
SNoLt_1_2 ) The following is provable:
1 < 2
Proof:
We will prove 1 ∈ 2 .
An
exact proof term for the current goal is
In_1_2 .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim Lx1 :
SNo_ (SNoLev x ) x .
An
exact proof term for the current goal is
SNoLev_ x Hx .
Apply Lx1 to the current goal.
Apply andI to the current goal.
Let beta be given.
We prove the intermediate
claim Lb :
beta ∈ SNoLev x .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is Hb .
∎
Theorem. (
restr_SNo ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim La :
ordinal alpha .
We prove the intermediate
claim L1 :
SNo_ alpha (x ∩ SNoElts_ alpha ) .
An
exact proof term for the current goal is
restr_SNo_ x Hx alpha Ha .
An
exact proof term for the current goal is
SNo_SNo alpha La (x ∩ SNoElts_ alpha ) L1 .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim La :
ordinal alpha .
We prove the intermediate
claim L1 :
SNo_ alpha (x ∩ SNoElts_ alpha ) .
An
exact proof term for the current goal is
restr_SNo_ x Hx alpha Ha .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
Let beta be given.
Apply iffI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Proof: Let x be given.
Assume Hx .
Apply SNo_eq to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
Use symmetry.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
∎
Proof: Let x be given.
Assume Hx .
Apply SNo_eq to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
Use symmetry.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
∎