Primitive . 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
Primitive . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
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 .
Primitive . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . 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
Primitive . 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
Primitive . 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 .
Primitive . 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:
Proof: An exact proof term for the current goal is (λH ⇒ H ) .
∎
Proof: An exact proof term for the current goal is (λp H ⇒ H ) .
∎
Theorem. (
andI )
∀A B : prop , A → B → A ∧ B
Proof: An exact proof term for the current goal is (λA B a b P H ⇒ H a b ) .
∎
Proof: An exact proof term for the current goal is (λA B H ⇒ H A (λa b ⇒ a ) ) .
∎
Proof: An exact proof term for the current goal is (λA B H ⇒ H B (λa b ⇒ b ) ) .
∎
Proof: An exact proof term for the current goal is (λA B a P H1 H2 ⇒ H1 a ) .
∎
Proof: An exact proof term for the current goal is (λA B b P H1 H2 ⇒ H2 b ) .
∎
Beginning of Section PropN
Variable P1 P2 P3 : prop
Theorem. (
and3I )
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Proof: An
exact proof term for the current goal is
(λH1 H2 H3 ⇒ andI (P1 ∧ P2 ) P3 (andI P1 P2 H1 H2 ) H3 ) .
∎
Theorem. (
and3E )
P1 ∧ P2 ∧ P3 → (∀p : prop , (P1 → P2 → P3 → p ) → p )
Proof: An exact proof term for the current goal is (λu p H ⇒ u p (λu u3 ⇒ u p (λu1 u2 ⇒ H u1 u2 u3 ) ) ) .
∎
Proof: An
exact proof term for the current goal is
(λu ⇒ orIL (P1 ∨ P2 ) P3 (orIL P1 P2 u ) ) .
∎
Proof: An
exact proof term for the current goal is
(λu ⇒ orIL (P1 ∨ P2 ) P3 (orIR P1 P2 u ) ) .
∎
Proof: An
exact proof term for the current goal is
(orIR (P1 ∨ P2 ) P3 ) .
∎
Theorem. (
or3E )
P1 ∨ P2 ∨ P3 → (∀p : prop , (P1 → p ) → (P2 → p ) → (P3 → p ) → p )
Proof: An exact proof term for the current goal is (λu p H1 H2 H3 ⇒ u p (λu ⇒ u p H1 H2 ) H3 ) .
∎
Variable P4 : prop
Theorem. (
and4I )
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Proof: An
exact proof term for the current goal is
(λH1 H2 H3 H4 ⇒ andI (P1 ∧ P2 ∧ P3 ) P4 (and3I H1 H2 H3 ) H4 ) .
∎
Variable P5 : prop
Theorem. (
and5I )
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
Proof: An
exact proof term for the current goal is
(λH1 H2 H3 H4 H5 ⇒ andI (P1 ∧ P2 ∧ P3 ∧ P4 ) P5 (and4I H1 H2 H3 H4 ) H5 ) .
∎
End of Section PropN
Proof: Let A and B be given.
Apply andI to the current goal.
Assume a : A .
An
exact proof term for the current goal is
(u (orIL A B a ) ) .
Assume b : B .
An
exact proof term for the current goal is
(u (orIR A B b ) ) .
∎
Proof: Let P be given.
Assume H1 .
Let x be given.
Assume H2 .
Apply H1 to the current goal.
We use x to witness the existential quantifier.
An exact proof term for the current goal is H2 .
∎
Theorem. (
iffI )
∀A B : prop , (A → B ) → (B → A ) → (A ↔ B )
Proof: An
exact proof term for the current goal is
(λA B ⇒ andI (A → B ) (B → A ) ) .
∎
Theorem. (
iffEL )
∀A B : prop , (A ↔ B ) → A → B
Proof: An
exact proof term for the current goal is
(λA B ⇒ andEL (A → B ) (B → A ) ) .
∎
Theorem. (
iffER )
∀A B : prop , (A ↔ B ) → B → A
Proof: An
exact proof term for the current goal is
(λA B ⇒ andER (A → B ) (B → A ) ) .
∎
Proof: An
exact proof term for the current goal is
(λA : prop ⇒ andI (A → A ) (A → A ) (λH : A ⇒ H ) (λH : A ⇒ H ) ) .
∎
Theorem. (
iff_sym )
∀A B : prop , (A ↔ B ) → (B ↔ A )
Proof: Let A and B be given.
Apply H1 to the current goal.
Assume H2 : A → B .
Assume H3 : B → A .
An
exact proof term for the current goal is
iffI B A H3 H2 .
∎
Theorem. (
iff_trans )
∀A B C : prop , (A ↔ B ) → (B ↔ C ) → (A ↔ C )
Proof: Let A, B and C be given.
Apply H1 to the current goal.
Assume H3 : A → B .
Assume H4 : B → A .
Apply H2 to the current goal.
Assume H5 : B → C .
Assume H6 : C → B .
An
exact proof term for the current goal is
(iffI A C (λH ⇒ H5 (H3 H ) ) (λH ⇒ H4 (H6 H ) ) ) .
∎
Proof: Let x, y and z be given.
Assume H1 H2 .
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is H1 .
∎
Theorem. (
f_eq_i )
∀f : set → set , ∀x y, x = y → f x = f y
Proof: Let f, x and y be given.
Assume H1 .
rewrite the current goal using H1 (from left to right).
Use reflexivity.
∎
Proof: Let x and y be given.
Assume H1 H2 .
Apply H1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2 .
∎
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 .
Proof: Let P be given.
Assume H1 .
Apply H1 to the current goal.
Let x be given.
Assume H2 .
An
exact proof term for the current goal is
Eps_i_ax P x H2 .
∎
Theorem. (
pred_ext )
∀P Q : set → prop , (∀x, P x ↔ Q x ) → P = Q
Proof: Let P and Q be given.
Assume H1 .
Apply func_ext set prop to the current goal.
Let x be given.
An exact proof term for the current goal is H1 x .
∎
Theorem. (
prop_ext_2 )
∀p q : prop , (p → q ) → (q → p ) → p = q
Proof: Let p and q be given.
Assume H1 H2 .
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 H2 .
∎
Proof: An
exact proof term for the current goal is
(λ(X x : set )(H : x ∈ X ) ⇒ H ) .
∎
Theorem. (
Subq_tra )
∀X Y Z : set , X ⊆ Y → Y ⊆ Z → X ⊆ Z
Proof: An
exact proof term for the current goal is
(λ(X Y Z : set )(H1 : X ⊆ Y )(H2 : Y ⊆ Z )(x : set )(H : x ∈ X ) ⇒ (H2 x (H1 x H ) ) ) .
∎
Proof: An exact proof term for the current goal is (λX Y z H1 H2 H3 ⇒ H2 (H1 z H3 ) ) .
∎
Proof: Let x be given.
Assume H .
We use x to witness the existential quantifier.
An exact proof term for the current goal is H .
∎
Proof: An
exact proof term for the current goal is
(λ(X x : set )(H : x ∈ Empty ) ⇒ EmptyE x H (x ∈ X ) ) .
∎
Proof: Let X be given.
An exact proof term for the current goal is H1 .
An
exact proof term for the current goal is
(Subq_Empty X ) .
∎
Proof: Let X be given.
Let x be given.
An exact proof term for the current goal is (H1 x H2 ) .
∎
Theorem. (
UnionI )
∀X x Y : set , x ∈ Y → Y ∈ X → x ∈ ⋃ X
Proof: Let X, x and Y be given.
Apply UnionEq X x to the current goal.
Assume _ H3 .
Apply H3 to the current goal.
We will
prove ∃Y : set , x ∈ Y ∧ Y ∈ X .
We use Y 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 H2 .
∎
Theorem. (
UnionE )
∀X x : set , x ∈ ⋃ X → ∃Y : set , x ∈ Y ∧ Y ∈ X
Proof: An
exact proof term for the current goal is
(λX x : set ⇒ iffEL (x ∈ ⋃ X ) (∃Y : set , x ∈ Y ∧ Y ∈ X ) (UnionEq X x ) ) .
∎
Theorem. (
UnionE_impred )
∀X x : set , x ∈ ⋃ X → ∀p : prop , (∀Y : set , x ∈ Y → Y ∈ X → p ) → p
Proof: Let X and x be given.
Assume H1 .
Let p be given.
Assume Hp .
Apply UnionE X x H1 to the current goal.
Let x be given.
Assume H2 .
Apply H2 to the current goal.
An exact proof term for the current goal is Hp x .
∎
Theorem. (
PowerI )
∀X Y : set , Y ⊆ X → Y ∈ 𝒫 X
Proof: Let X and Y be given.
Apply PowerEq X Y to the current goal.
An exact proof term for the current goal is (λ_ H ⇒ H ) .
∎
Theorem. (
PowerE )
∀X Y : set , Y ∈ 𝒫 X → Y ⊆ X
Proof: Let X and Y be given.
Apply PowerEq X Y to the current goal.
An exact proof term for the current goal is (λH _ ⇒ H ) .
∎
Proof: An
exact proof term for the current goal is
(λX : set ⇒ PowerI X X (Subq_ref X ) ) .
∎
Proof: Let P of type prop be given.
Set p1 to be the term
λx : set ⇒ x = Empty ∨ P .
Set p2 to be the term
λx : set ⇒ x ≠ Empty ∨ P .
We prove the intermediate
claim L1 :
p1 Empty .
Apply orIL to the current goal.
An exact proof term for the current goal is (λq H ⇒ H ) .
An
exact proof term for the current goal is
(Eps_i_ax p1 Empty L1 ) .
We prove the intermediate
claim L3 :
p2 (𝒫 Empty ) .
Apply orIL to the current goal.
rewrite the current goal using H1 (from right to left) at position 2.
An
exact proof term for the current goal is
(Eps_i_ax p2 (𝒫 Empty ) L3 ) .
Apply L2 to the current goal.
Apply L4 to the current goal.
Apply orIR to the current goal.
Assume H3 : P .
We prove the intermediate
claim L5 :
p1 = p2 .
Let x be given.
Apply iffI to the current goal.
Assume H4 .
Apply orIR to the current goal.
We will prove P .
An exact proof term for the current goal is H3 .
Assume H4 .
Apply orIR to the current goal.
We will prove P .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
rewrite the current goal using L5 (from right to left).
An exact proof term for the current goal is H1 .
Assume H2 : P .
Apply orIL to the current goal.
We will prove P .
An exact proof term for the current goal is H2 .
Assume H1 : P .
Apply orIL to the current goal.
We will prove P .
An exact proof term for the current goal is H1 .
∎
Proof: Let P be given.
Assume H1 .
Apply xm P to the current goal.
An exact proof term for the current goal is (λH ⇒ H ) .
An exact proof term for the current goal is H1 H2 .
∎
Proof: Let P be given.
Apply dneg to the current goal.
Apply u to the current goal.
Let x be given.
Apply dneg to the current goal.
∎
Proof: Apply func_ext prop (prop → prop ) to the current goal.
Let x be given.
Apply func_ext prop prop to the current goal.
Let y be given.
Apply H2 to the current goal.
Assume H3 H4 .
An
exact proof term for the current goal is
(H1 False H3 H4 ) .
Apply (xm x ) to the current goal.
Assume H2 : x .
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
Apply (xm y ) to the current goal.
Assume H3 : y .
Apply orIR to the current goal.
An exact proof term for the current goal is H3 .
Apply H1 to the current goal.
An
exact proof term for the current goal is
(andI (¬ x ) (¬ y ) H2 H3 ) .
∎
Definition. We define
exactly1of2 to be
λA B : prop ⇒ A ∧ ¬ B ∨ ¬ A ∧ B of type
prop → prop → prop .
Proof: Let A and B be given.
Assume HA : A .
We will
prove A ∧ ¬ B ∨ ¬ A ∧ B .
Apply orIL to the current goal.
An
exact proof term for the current goal is
(andI A (¬ B ) HA HB ) .
∎
Proof: Let A and B be given.
Assume HB : B .
We will
prove A ∧ ¬ B ∨ ¬ A ∧ B .
Apply orIR to the current goal.
An
exact proof term for the current goal is
(andI (¬ A ) B HA HB ) .
∎
Proof: Let A and B be given.
Let p be given.
Apply (H1 p ) to the current goal.
An
exact proof term for the current goal is
(λH4 : A ∧ ¬ B ⇒ H4 p H2 ) .
An
exact proof term for the current goal is
(λH4 : ¬ A ∧ B ⇒ H4 p H3 ) .
∎
Proof: Let A and B be given.
An
exact proof term for the current goal is
(λ(HA : A )(_ : ¬ B ) ⇒ orIL A B HA ) .
An
exact proof term for the current goal is
(λ(_ : ¬ A )(HB : B ) ⇒ orIR A B HB ) .
∎
Theorem. (
ReplI )
∀A : set , ∀F : set → set , ∀x : set , x ∈ A → F x ∈ { F x | x ∈ A }
Proof: Let A, F and x be given.
Assume H1 .
Apply ReplEq A F (F x ) to the current goal.
Assume _ H2 .
Apply H2 to the current goal.
We will
prove ∃x' ∈ A , F x = F x' .
We use x 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 (λq H ⇒ H ) .
∎
Theorem. (
ReplE )
∀A : set , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ A } → ∃x ∈ A , y = F x
Proof: Let A, F and y be given.
Apply ReplEq A F y to the current goal.
An exact proof term for the current goal is (λH _ ⇒ H ) .
∎
Theorem. (
ReplE_impred )
∀A : set , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ A } → ∀p : prop , (∀x : set , x ∈ A → y = F x → p ) → p
Proof: Let A, F and y be given.
Assume H1 .
Apply ReplE A F y H1 to the current goal.
Let x be given.
Assume H2 .
Apply H2 to the current goal.
Assume H3 H4 .
Let p be given.
Assume Hp .
An exact proof term for the current goal is Hp x H3 H4 .
∎
Theorem. (
ReplE' )
∀X, ∀f : set → set , ∀p : set → prop , (∀x ∈ X , p (f x ) ) → ∀y ∈ { f x | x ∈ X } , p y
Proof: Let X, f and p be given.
Assume H1 .
Let y be given.
Assume Hy .
Let x be given.
We will prove p y .
rewrite the current goal using Hx2 (from left to right).
An exact proof term for the current goal is H1 x Hx .
∎
Proof: Let F be given.
Let y be given.
Let x be given.
Assume _ .
An
exact proof term for the current goal is
(EmptyE x H2 ) .
∎
Proof: Let X, F and G be given.
Let y be given.
Let x be given.
We will
prove y ∈ { G x | x ∈ X } .
rewrite the current goal using H2 (from left to right).
We will
prove F x ∈ { G x | x ∈ X } .
rewrite the current goal using H1 x Hx (from left to right).
We will
prove G x ∈ { G x | x ∈ X } .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx .
∎
Proof: Let X, F and G be given.
Let x be given.
Assume Hx .
Use symmetry.
An exact proof term for the current goal is H1 x Hx .
∎
Theorem. (
Repl_inv_eq )
∀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
Proof: Let P, f and g be given.
Assume H1 .
Let X be given.
Assume HX .
Let w be given.
Let y be given.
Let x be given.
rewrite the current goal using Hwy (from left to right).
rewrite the current goal using Hyx (from left to right).
We will
prove g (f x ) ∈ X .
rewrite the current goal using H1 x (HX x Hx ) (from left to right).
An exact proof term for the current goal is Hx .
Let x be given.
rewrite the current goal using H1 x (HX x Hx ) (from right to left).
We will
prove g (f x ) ∈ { g y | y ∈ { f x | x ∈ X } } .
Apply ReplI to the current goal.
We will
prove f x ∈ { f x | x ∈ X } .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx .
∎
Theorem. (
Repl_invol_eq )
∀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
Proof: Let P and f be given.
Assume H1 .
An
exact proof term for the current goal is
Repl_inv_eq P f f H1 .
∎
Definition. We define
If_i to be
(λp x y ⇒ Eps_i (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y ) ) 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 .
Proof: Let p, x and y be given.
Apply (xm p ) to the current goal.
Assume H1 : p .
We prove the intermediate
claim L1 :
p ∧ x = x ∨ ¬ p ∧ x = y .
Apply orIL to the current goal.
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
(Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y ) x L1 ) .
We prove the intermediate
claim L1 :
p ∧ y = x ∨ ¬ p ∧ y = y .
Apply orIR to the current goal.
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
(Eps_i_ax (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y ) y L1 ) .
∎
Proof: Let p, x and y be given.
An
exact proof term for the current goal is
(andER (¬ p ) ((if p then x else y ) = y ) H2 ) .
∎
Proof: Let p, x and y be given.
Assume H1 : p .
An
exact proof term for the current goal is
(andER p ((if p then x else y ) = x ) H2 ) .
∎
Proof: Let p, x and y be given.
Apply (xm p ) to the current goal.
Assume H1 : p .
Apply orIL to the current goal.
An
exact proof term for the current goal is
(If_i_1 p x y H1 ) .
Apply orIR to the current goal.
An
exact proof term for the current goal is
(If_i_0 p x y H1 ) .
∎
Notation .
{x ,y } is notation for
UPair x y .
Proof: Let x, y and z be given.
Let X be given.
Apply orIL to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1 .
Apply orIR to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1 .
∎
Proof: Let y and z be given.
∎
Proof: Let y and z be given.
∎
Definition. We define
Sing to be
λx ⇒ { x , x } of type
set → set .
Notation .
{x } is notation for
Sing x .
Proof: An
exact proof term for the current goal is
(λx : set ⇒ UPairI1 x x ) .
∎
Proof: An
exact proof term for the current goal is
(λx y H ⇒ UPairE y x x H (y = x ) (λH ⇒ H ) (λH ⇒ H ) ) .
∎
Proof: Let x and y be given.
Apply SingE to the current goal.
rewrite the current goal using H1 (from right to left).
Apply SingI to the current goal.
∎
Definition. We define
binunion to be
λX Y ⇒ ⋃ { X , Y } 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 .
Proof: Let X, Y and z be given.
We will
prove z ∈ ⋃ { X , Y } .
Apply (UnionI { X , Y } z X ) to the current goal.
An exact proof term for the current goal is H1 .
An
exact proof term for the current goal is
(UPairI1 X Y ) .
∎
Proof: Let X, Y and z be given.
We will
prove z ∈ ⋃ { X , Y } .
Apply (UnionI { X , Y } z Y ) to the current goal.
An exact proof term for the current goal is H1 .
An
exact proof term for the current goal is
(UPairI2 X Y ) .
∎
Proof: Let X, Y and z be given.
We will
prove z ∈ X ∨ z ∈ Y .
Let Z be given.
Apply (UPairE Z X Y H3 ) to the current goal.
Apply orIL to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H2 .
Apply orIR to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H2 .
∎
Theorem. (
binunionE' )
∀X Y z, ∀p : prop , (z ∈ X → p ) → (z ∈ Y → p ) → (z ∈ X ∪ Y → p )
Proof: Let X, Y, z and p be given.
Assume H1 H2 Hz .
Apply binunionE X Y z Hz to the current goal.
An exact proof term for the current goal is H1 H3 .
An exact proof term for the current goal is H2 H3 .
∎
Proof: Let X, Y and Z be given.
Let w be given.
We will
prove w ∈ (X ∪ Y ) ∪ Z .
Apply (binunionE X (Y ∪ Z ) w H1 ) to the current goal.
An exact proof term for the current goal is H2 .
Apply (binunionE Y Z w H2 ) to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H3 .
Let w be given.
We will
prove w ∈ X ∪ (Y ∪ Z ) .
Apply (binunionE (X ∪ Y ) Z w H1 ) to the current goal.
Apply (binunionE X Y w H2 ) to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H2 .
∎
Proof: Let X, Y and w be given.
Apply (binunionE X Y w H1 ) to the current goal.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H2 .
∎
Proof: Let X and Y be given.
∎
Proof: Let X be given.
Let x be given.
An
exact proof term for the current goal is
(EmptyE x H2 ) .
An exact proof term for the current goal is H2 .
Let x be given.
An exact proof term for the current goal is H2 .
∎
Proof: Let X be given.
An
exact proof term for the current goal is
(binunion_idl X ) .
∎
Proof: An
exact proof term for the current goal is
binunionI1 .
∎
Proof: An
exact proof term for the current goal is
binunionI2 .
∎
Proof: Let X, Y and Z be given.
Let w be given.
Apply (binunionE X Y w H3 ) to the current goal.
An exact proof term for the current goal is (H1 w H4 ) .
An exact proof term for the current goal is (H2 w H4 ) .
∎
Proof: Let X and Y be given.
An exact proof term for the current goal is H1 .
An
exact proof term for the current goal is
(Subq_ref Y ) .
rewrite the current goal using H1 (from right to left).
∎
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.
Definition. We define
famunion to be
λX F ⇒ ⋃ { F x | x ∈ X } of type
set → (set → set ) → set .
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
Theorem. (
famunionI )
∀X : set , ∀F : (set → set ) , ∀x y : set , x ∈ X → y ∈ F x → y ∈ ⋃ x ∈ X F x
Proof: An
exact proof term for the current goal is
(λX F x y H1 H2 ⇒ UnionI (Repl X F ) y (F x ) H2 (ReplI X F x H1 ) ) .
∎
Theorem. (
famunionE )
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃ x ∈ X F x ) → ∃x ∈ X , y ∈ F x
Proof: Let X, F and y be given.
We will
prove ∃x ∈ X , y ∈ F x .
Let Y be given.
Let x be given.
We use x to witness the existential quantifier.
We will
prove x ∈ X ∧ y ∈ F x .
Apply andI to the current goal.
An exact proof term for the current goal is H4 .
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is H2 .
∎
Theorem. (
famunionE_impred )
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃ x ∈ X F x ) → ∀p : prop , (∀x, x ∈ X → y ∈ F x → p ) → p
Proof: Let X, F and y be given.
Assume Hy .
Let p be given.
Assume Hp .
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is Hp x .
∎
Proof: Let F be given.
Let y be given.
Let x be given.
An
exact proof term for the current goal is
EmptyE x Hx .
∎
Proof: Let X, f and g be given.
Assume Hfg .
Let y be given.
Assume Hy .
Let x be given.
Assume Hx .
Apply famunionI X g x y Hx to the current goal.
An exact proof term for the current goal is Hfg x Hx y H1 .
∎
Proof: Let X, f and g be given.
Assume Hfg .
Let x be given.
Assume Hx .
rewrite the current goal using Hfg x Hx (from left to right).
Let x be given.
Assume Hx .
rewrite the current goal using Hfg x Hx (from left to right).
∎
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z )
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Theorem. (
SepI )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ X → P x → x ∈ { x ∈ X | P x }
Proof: Let X, P and x be given.
Set z to be the term
Eps_i (λz ⇒ z ∈ X ∧ P z ) of type
set .
Set F to be the term
λx ⇒ if P x then x else z of type
set → set .
Assume H2 : P x .
We prove the intermediate
claim L1 :
∃z ∈ X , P z .
We use x 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 H2 .
We will
prove x ∈ { x ∈ X | P x } .
An
exact proof term for the current goal is
(If_i_1 (∃z ∈ X , P z ) { F x | x ∈ X } Empty L1 ) .
rewrite the current goal using L2 (from left to right).
We will
prove x ∈ { F x | x ∈ X } .
We prove the intermediate
claim L3 :
F x = x .
An
exact proof term for the current goal is
(If_i_1 (P x ) x z H2 ) .
rewrite the current goal using L3 (from right to left).
We will
prove F x ∈ { F x | x ∈ X } .
An
exact proof term for the current goal is
(ReplI X F x H1 ) .
∎
Theorem. (
SepE )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → x ∈ X ∧ P x
Proof: Let X, P and x be given.
Set z to be the term
Eps_i (λz ⇒ z ∈ X ∧ P z ) of type
set .
Set F to be the term
λx ⇒ if P x then x else z of type
set → set .
Apply (xm (∃z ∈ X , P z ) ) to the current goal.
An
exact proof term for the current goal is
(If_i_1 (∃z ∈ X , P z ) { F x | x ∈ X } Empty H1 ) .
rewrite the current goal using L1 (from left to right).
We will
prove x ∈ { F x | x ∈ X } → x ∈ X ∧ P x .
Let y be given.
We will
prove x ∈ X ∧ P x .
Apply (xm (P y ) ) to the current goal.
Assume H5 : P y .
We prove the intermediate
claim L2 :
x = y .
rewrite the current goal using
(If_i_1 (P y ) y z H5 ) (from right to left).
An exact proof term for the current goal is H4 .
rewrite the current goal using L2 (from left to right).
We will
prove y ∈ X ∧ P y .
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H5 .
We prove the intermediate
claim L2 :
x = z .
rewrite the current goal using
(If_i_0 (P y ) y z H5 ) (from right to left).
An exact proof term for the current goal is H4 .
rewrite the current goal using L2 (from left to right).
We will
prove z ∈ X ∧ P z .
An
exact proof term for the current goal is
(Eps_i_ex (λz ⇒ z ∈ X ∧ P z ) H1 ) .
An
exact proof term for the current goal is
(If_i_0 (∃z ∈ X , P z ) { F x | x ∈ X } Empty H1 ) .
rewrite the current goal using L1 (from left to right).
An
exact proof term for the current goal is
(EmptyE x H2 ) .
∎
Theorem. (
SepE1 )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → x ∈ X
Proof: An
exact proof term for the current goal is
(λX P x H ⇒ SepE X P x H (x ∈ X ) (λH _ ⇒ H ) ) .
∎
Theorem. (
SepE2 )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → P x
Proof: An
exact proof term for the current goal is
(λX P x H ⇒ SepE X P x H (P x ) (λ_ H ⇒ H ) ) .
∎
Proof: Let P be given.
Let x be given.
Assume Hx .
∎
Proof: An
exact proof term for the current goal is
SepE1 .
∎
Proof: An
exact proof term for the current goal is
(λX P ⇒ PowerI X (Sep X P ) (Sep_Subq X P ) ) .
∎
Definition. We define
ReplSep to be
λX P F ⇒ { F x | x ∈ { z ∈ X | P z } } of type
set → (set → prop ) → (set → set ) → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Theorem. (
ReplSepI )
∀X : set , ∀P : set → prop , ∀F : set → set , ∀x : set , x ∈ X → P x → F x ∈ { F x | x ∈ X , P x }
Proof: An
exact proof term for the current goal is
(λX P F x u v ⇒ ReplI (Sep X P ) F x (SepI X P x u v ) ) .
∎
Theorem. (
ReplSepE )
∀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
Proof: Let X, P, F and y be given.
Apply (ReplE { z ∈ X | P z } F y H1 ) to the current goal.
Let x be given.
Apply H2 to the current goal.
Apply (SepE X P x H3 ) to the current goal.
Assume H6 : P x .
We use x to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H6 .
An exact proof term for the current goal is H4 .
∎
Theorem. (
ReplSepE_impred )
∀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
Proof: Let X, P, F and y be given.
Let p be given.
We will prove p .
Apply ReplSepE X P F y H1 to the current goal.
Let x be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
An exact proof term for the current goal is H2 x .
∎
Definition. We define
binintersect to be
λX Y ⇒ { x ∈ X | x ∈ Y } 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 .
Proof: An
exact proof term for the current goal is
(λX Y z H1 H2 ⇒ SepI X (λx : set ⇒ x ∈ Y ) z H1 H2 ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H1 ⇒ SepE X (λx : set ⇒ x ∈ Y ) z H1 ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H1 ⇒ SepE1 X (λx : set ⇒ x ∈ Y ) z H1 ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H1 ⇒ SepE2 X (λx : set ⇒ x ∈ Y ) z H1 ) .
∎
Proof: Let X and Y be given.
Let x be given.
An exact proof term for the current goal is H2 .
Apply H1 to the current goal.
An exact proof term for the current goal is H2 .
∎
Proof: Let X, Y and Z be given.
Let w be given.
An exact proof term for the current goal is (H1 w H3 ) .
An exact proof term for the current goal is (H2 w H3 ) .
∎
Proof: Let X and Y be given.
∎
Proof: Let X and Y be given.
∎
Definition. We define
setminus to be
λX Y ⇒ Sep X (λx ⇒ x ∉ Y ) of type
set → set → set .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
Proof: An
exact proof term for the current goal is
(λX Y z H1 H2 ⇒ SepI X (λx : set ⇒ x ∉ Y ) z H1 H2 ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H ⇒ SepE X (λx : set ⇒ x ∉ Y ) z H ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H ⇒ SepE1 X (λx : set ⇒ x ∉ Y ) z H ) .
∎
Proof: An
exact proof term for the current goal is
(λX Y z H ⇒ SepE2 X (λx : set ⇒ x ∉ Y ) z H ) .
∎
Proof: An
exact proof term for the current goal is
setminusE1 .
∎
Proof: Let X, Y and Z be given.
Let x be given.
Apply (setminusE X Y x H2 ) to the current goal.
An exact proof term for the current goal is H3 .
An
exact proof term for the current goal is
(Subq_contra Z Y x H1 H4 ) .
∎
Proof: Let A and U be given.
Apply PowerI to the current goal.
∎
Proof: Let X be given.
Let u be given.
An exact proof term for the current goal is Hu .
An
exact proof term for the current goal is
EmptyE u .
∎
Proof: Apply In_ind to the current goal.
We will
prove (∀X : set , (∀x : set , x ∈ X → x ∉ x ) → X ∉ X ) .
Let X be given.
An exact proof term for the current goal is IH X H H .
∎
Proof: Apply In_ind to the current goal.
Let x be given.
Let y be given.
An exact proof term for the current goal is IH y H2 x H2 H1 .
∎
Definition. We define
ordsucc to be
λx : set ⇒ x ∪ { x } of type
set → set .
Proof: Let x be given.
An
exact proof term for the current goal is
(λ(y : set )(H1 : y ∈ x ) ⇒ binunionI1 x { x } y H1 ) .
∎
Proof: An
exact proof term for the current goal is
(λx : set ⇒ binunionI2 x { x } x (SingI x ) ) .
∎
Proof: Let x and y be given.
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
Apply orIR to the current goal.
An
exact proof term for the current goal is
(SingE x y H2 ) .
∎
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Proof: Let a be given.
rewrite the current goal using H1 (from right to left).
An
exact proof term for the current goal is
(EmptyE a ) .
An
exact proof term for the current goal is
(L1 (ordsuccI2 a ) ) .
∎
Proof: Let a and b be given.
We prove the intermediate
claim L1 :
a ∈ ordsucc b .
rewrite the current goal using H1 (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 a ) .
Apply (ordsuccE b a L1 ) to the current goal.
We prove the intermediate
claim L2 :
b ∈ ordsucc a .
rewrite the current goal using H1 (from left to right).
An
exact proof term for the current goal is
(ordsuccI2 b ) .
Apply (ordsuccE a b L2 ) to the current goal.
An
exact proof term for the current goal is
(In_no2cycle a b H2 H3 ) .
Use symmetry.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H2 .
∎
Proof: Let a and b be given.
Assume H1 .
An
exact proof term for the current goal is
H1 (ordsucc_inj a b H2 ) .
∎
Proof: An
exact proof term for the current goal is
(ordsuccI2 0 ) .
∎
Proof: An
exact proof term for the current goal is
(ordsuccI2 1 ) .
∎
Proof:
An
exact proof term for the current goal is
In_1_2 .
∎
Proof:
An
exact proof term for the current goal is
In_1_3 .
∎
Proof:
An
exact proof term for the current goal is
In_2_3 .
∎
Proof:
An
exact proof term for the current goal is
In_1_4 .
∎
Proof:
An
exact proof term for the current goal is
In_2_4 .
∎
Proof:
An
exact proof term for the current goal is
In_3_4 .
∎
Proof:
An
exact proof term for the current goal is
In_1_5 .
∎
Proof:
An
exact proof term for the current goal is
In_1_6 .
∎
Proof:
An
exact proof term for the current goal is
In_1_7 .
∎
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 .
Proof: An exact proof term for the current goal is (λp H _ ⇒ H ) .
∎
Proof: An exact proof term for the current goal is (λn H1 p H2 H3 ⇒ H3 n (H1 p H2 H3 ) ) .
∎
Proof: Let n be given.
Assume H1 .
Apply H1 (λn ⇒ 0 ∈ ordsucc n ) to the current goal.
An
exact proof term for the current goal is
In_0_1 .
∎
Proof: Let n be given.
Assume H1 .
Let m be given.
An
exact proof term for the current goal is
(EmptyE m Hm ) .
Let n be given.
Let m be given.
Apply (ordsuccE n m H2 ) to the current goal.
An exact proof term for the current goal is (IH m H3 ) .
rewrite the current goal using H3 (from left to right).
∎
Proof: Let p be given.
We prove the intermediate
claim L1 :
nat_p 0 ∧ p 0 .
Let n be given.
Apply H3 to the current goal.
Assume H5 : p n .
Apply andI to the current goal.
An
exact proof term for the current goal is
(nat_ordsucc n H4 ) .
An exact proof term for the current goal is (H2 n H4 H5 ) .
Let n be given.
Assume H3 .
We prove the intermediate
claim L3 :
nat_p n ∧ p n .
An
exact proof term for the current goal is
(H3 (λn ⇒ nat_p n ∧ p n ) L1 L2 ) .
An
exact proof term for the current goal is
(andER (nat_p n ) (p n ) L3 ) .
∎
Proof: Let p be given.
Assume H1 H2 .
An
exact proof term for the current goal is
nat_ind p H1 (λn H _ ⇒ H2 n H ) .
∎
Proof:
Apply orIL to the current goal.
Use reflexivity.
Let n be given.
Assume Hn .
Apply orIR to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
∎
Proof: Let p be given.
We prove the intermediate
claim L1 :
∀n : set , nat_p n → ∀m ∈ n , p m .
We will
prove ∀m ∈ 0 , p m .
Let m be given.
An
exact proof term for the current goal is
(EmptyE m Hm ) .
Let n be given.
Let m be given.
We will prove p m .
Apply (ordsuccE n m Hm ) to the current goal.
An exact proof term for the current goal is (IHn m H2 ) .
We will prove p m .
rewrite the current goal using H2 (from left to right).
We will prove p n .
An exact proof term for the current goal is (H1 n Hn IHn ) .
We will
prove ∀n, nat_p n → p n .
An exact proof term for the current goal is (λn Hn ⇒ H1 n Hn (L1 n Hn ) ) .
∎
Proof:
Let m be given.
An
exact proof term for the current goal is
(EmptyE m Hm ) .
Let n be given.
Let m be given.
Apply (ordsuccE n m Hm ) to the current goal.
An exact proof term for the current goal is (IHn m H1 ) .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hn .
∎
Proof:
We will
prove ∀m ∈ 0 , m ⊆ 0 .
Let m be given.
An
exact proof term for the current goal is
(EmptyE m Hm ) .
Let n be given.
Let m be given.
Apply (ordsuccE n m Hm ) to the current goal.
An exact proof term for the current goal is (IHn m H1 ) .
An
exact proof term for the current goal is
(ordsuccI1 n ) .
rewrite the current goal using H1 (from left to right).
An
exact proof term for the current goal is
(ordsuccI1 n ) .
∎
Proof: Let n be given.
Let m be given.
Let k be given.
Apply (ordsuccE n m Hm ) to the current goal.
An
exact proof term for the current goal is
nat_trans n Hn m H1 k Hk .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hk .
∎
Proof:
Let n be given.
Let m be given.
Let k be given.
Let m be given.
An exact proof term for the current goal is Hm .
An
exact proof term for the current goal is
(ordsuccI2 n ) .
∎
Theorem. (
cases_1 )
∀i ∈ 1 , ∀p : set → prop , p 0 → p i
Proof: Let i be given.
Assume Hi .
Let p be given.
Assume Hp0 .
Apply EmptyE i Hil to the current goal.
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp0 .
∎
Theorem. (
cases_2 )
∀i ∈ 2 , ∀p : set → prop , p 0 → p 1 → p i
Proof: Let i be given.
Assume Hi .
Let p be given.
Assume Hp0 Hp1 .
An
exact proof term for the current goal is
cases_1 i Hil p Hp0 .
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp1 .
∎
Theorem. (
cases_3 )
∀i ∈ 3 , ∀p : set → prop , p 0 → p 1 → p 2 → p i
Proof: Let i be given.
Assume Hi .
Let p be given.
Assume Hp0 Hp1 Hp2 .
An
exact proof term for the current goal is
cases_2 i Hil p Hp0 Hp1 .
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp2 .
∎
Proof:
An
exact proof term for the current goal is
neq_0_2 .
∎
Proof:
An
exact proof term for the current goal is
neq_1_2 .
∎
Proof:
An
exact proof term for the current goal is
neq_1_3 .
∎
Proof:
An
exact proof term for the current goal is
neq_2_3 .
∎
Proof: An exact proof term for the current goal is (λU C p v ⇒ C p (λC H3 ⇒ C p (λH1 H2 ⇒ v H1 H2 H3 ) ) ) .
∎
Proof: An
exact proof term for the current goal is
(λU C ⇒ ZF_closed_E U C (∀X ∈ U , ⋃ X ∈ U ) (λH _ _ ⇒ H ) ) .
∎
Proof: An
exact proof term for the current goal is
(λU C ⇒ ZF_closed_E U C (∀X ∈ U , 𝒫 X ∈ U ) (λ_ H _ ⇒ H ) ) .
∎
Proof: An
exact proof term for the current goal is
(λU C ⇒ ZF_closed_E U C (∀X ∈ U , ∀F : set → set , (∀x ∈ X , F x ∈ U ) → { F x | x ∈ X } ∈ U ) (λ_ _ H ⇒ H ) ) .
∎
Proof: Let U be given.
Let x be given.
Let y be given.
Let z be given.
Let X be given.
Assume _ .
Apply (xm (x ∈ X ) ) to the current goal.
rewrite the current goal using
(If_i_1 (x ∈ X ) x y H2 ) (from left to right).
We will
prove (z = x → z ∈ { x , y } ) .
rewrite the current goal using H3 (from left to right).
An
exact proof term for the current goal is
(UPairI1 x y ) .
rewrite the current goal using
(If_i_0 (x ∈ X ) x y H2 ) (from left to right).
We will
prove (z = y → z ∈ { x , y } ) .
rewrite the current goal using H3 (from left to right).
An
exact proof term for the current goal is
(UPairI2 x y ) .
Let z be given.
We will
prove 𝒫 x ∈ 𝒫 (𝒫 x ) .
Apply (UPairE z x y Hz ) to the current goal.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
(If_i_1 (x ∈ (𝒫 x ) ) x y (Self_In_Power x ) ) (from right to left) at position 1.
An exact proof term for the current goal is L1a .
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
(If_i_0 (x ∈ Empty ) x y (EmptyE x ) ) (from right to left) at position 1.
An exact proof term for the current goal is L1b .
rewrite the current goal using L1 (from right to left).
We prove the intermediate
claim L2 :
𝒫 (𝒫 x ) ∈ U .
We prove the intermediate
claim L3 :
∀X ∈ 𝒫 (𝒫 x ) , (if x ∈ X then x else y ) ∈ U .
Let X be given.
Assume _ .
Apply (xm (x ∈ X ) ) to the current goal.
rewrite the current goal using
(If_i_1 (x ∈ X ) x y H1 ) (from left to right).
An exact proof term for the current goal is Hx .
rewrite the current goal using
(If_i_0 (x ∈ X ) x y H1 ) (from left to right).
An exact proof term for the current goal is Hy .
∎
Proof: An
exact proof term for the current goal is
(λU C x H ⇒ ZF_UPair_closed U C x H x H ) .
∎
Proof: Let n be given.
Apply SepI to the current goal.
An exact proof term for the current goal is H .
∎
Proof: Let n be given.
Assume Hn .
An exact proof term for the current goal is Hn .
∎
Proof: An
exact proof term for the current goal is
(λalpha H ⇒ andEL (TransSet alpha ) (∀beta ∈ alpha , TransSet beta ) H ) .
∎
Proof:
Apply andI to the current goal.
Let x be given.
An
exact proof term for the current goal is
(EmptyE x Hx ) .
Let x be given.
An
exact proof term for the current goal is
(EmptyE x Hx ) .
∎
Proof: Let alpha be given.
Let beta be given.
Apply H1 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (H4 beta H2 ) .
Let x be given.
We prove the intermediate
claim L1 :
x ∈ alpha .
An exact proof term for the current goal is (H3 beta H2 x Hx ) .
An exact proof term for the current goal is (H4 x L1 ) .
∎
Proof: Let X be given.
Let x be given.
Let y be given.
Apply (ordsuccE X x H2 ) to the current goal.
An exact proof term for the current goal is (H1 x H4 y H3 ) .
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3 .
∎
Proof: Let alpha be given.
Apply H1 to the current goal.
Apply andI to the current goal.
Let beta be given.
Apply (ordsuccE alpha beta H4 ) to the current goal.
An exact proof term for the current goal is (H3 beta H5 ) .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let n be given.
Let m be given.
An
exact proof term for the current goal is
(omega_nat_p n Hn ) .
An exact proof term for the current goal is Hm .
∎
Proof:
Apply andI to the current goal.
Let n be given.
An
exact proof term for the current goal is
(omega_nat_p n Hn ) .
∎
Proof: Let X be given.
Let x be given.
Let y be given.
Apply (ordsuccE x y H3 ) to the current goal.
An exact proof term for the current goal is (H1 x H2 y H4 ) .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let alpha be given.
∎
Proof: Apply In_ind to the current goal.
Let alpha be given.
We will
prove ∀beta : set , ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha .
Apply In_ind to the current goal.
Let beta be given.
We will
prove alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha .
Apply (xm (alpha ∈ beta ) ) to the current goal.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1 .
Apply (xm (beta ∈ alpha ) ) to the current goal.
Apply or3I3 to the current goal.
An exact proof term for the current goal is H2 .
Apply or3I2 to the current goal.
We will
prove alpha = beta .
We will
prove alpha ⊆ beta .
Let gamma be given.
We will
prove gamma ∈ beta .
We prove the intermediate
claim Lgamma :
ordinal gamma .
An
exact proof term for the current goal is
(ordinal_Hered alpha Halpha gamma H3 ) .
Apply (or3E (gamma ∈ beta ) (gamma = beta ) (beta ∈ gamma ) (IHalpha gamma H3 beta Lgamma Hbeta ) ) to the current goal.
An exact proof term for the current goal is H4 .
Apply H2 to the current goal.
We will
prove beta ∈ alpha .
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
We will
prove beta ∈ alpha .
An
exact proof term for the current goal is
(ordinal_TransSet alpha Halpha gamma H3 beta H4 ) .
We will
prove beta ⊆ alpha .
Let delta be given.
We will
prove delta ∈ alpha .
We prove the intermediate
claim Ldelta :
ordinal delta .
An
exact proof term for the current goal is
(ordinal_Hered beta Hbeta delta H3 ) .
Apply (or3E (alpha ∈ delta ) (alpha = delta ) (delta ∈ alpha ) (IHbeta delta H3 Halpha Ldelta ) ) to the current goal.
Apply H1 to the current goal.
We will
prove alpha ∈ beta .
An
exact proof term for the current goal is
(ordinal_TransSet beta Hbeta delta H3 alpha H4 ) .
Apply H1 to the current goal.
We will
prove alpha ∈ beta .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H4 .
∎
Proof: Let alpha and beta be given.
Assume H1 H2 .
∎
Proof: Let alpha and beta be given.
Apply orIL to the current goal.
An exact proof term for the current goal is H3 .
Apply orIR to the current goal.
rewrite the current goal using H3 (from left to right).
Apply orIR to the current goal.
An
exact proof term for the current goal is
(ordinal_TransSet alpha H1 beta H3 ) .
∎
Proof: Let alpha and beta be given.
Apply orIL to the current goal.
An
exact proof term for the current goal is
(ordinal_TransSet beta H2 alpha H3 ) .
Apply orIR to the current goal.
An exact proof term for the current goal is H3 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Assume H1 .
Apply H1 to the current goal.
Apply ordsuccE beta alpha H2 to the current goal.
An
exact proof term for the current goal is
In_no2cycle alpha beta H3 Hb .
Apply In_irref alpha to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is Hb .
Apply orIR to the current goal.
An exact proof term for the current goal is H2 .
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
∎
Proof: Let alpha be given.
Assume Ha .
Apply xm (∃beta ∈ alpha , alpha = ordsucc beta ) to the current goal.
Assume H1 .
Apply orIR to the current goal.
An exact proof term for the current goal is H1 .
Apply orIL to the current goal.
Let beta be given.
An exact proof term for the current goal is H3 .
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 H2 .
An exact proof term for the current goal is H3 .
∎
Proof: Let alpha be given.
Assume Ha .
Let beta be given.
Assume Hb .
We prove the intermediate
claim L1 :
ordsucc beta ⊆ alpha .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L2 :
ordsucc beta = alpha .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is H1 .
rewrite the current goal using L2 (from left to right).
∎
Proof: Let X and F be given.
Assume HXF .
Apply andI to the current goal.
Let y be given.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1 .
Apply H1 to the current goal.
We will
prove y ⊆ ⋃ x ∈ X F x .
We prove the intermediate
claim LFx :
ordinal (F x ) .
An exact proof term for the current goal is HXF x Hx .
Apply LFx to the current goal.
Assume HFx1 _ .
Let z be given.
We will
prove z ∈ ⋃ x ∈ X F x .
We prove the intermediate
claim LzFx :
z ∈ F x .
An exact proof term for the current goal is HFx1 y Hy z Hz .
An
exact proof term for the current goal is
famunionI X F x z Hx LzFx .
Let y be given.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1 .
Apply H1 to the current goal.
We prove the intermediate
claim LFx :
ordinal (F x ) .
An exact proof term for the current goal is HXF x Hx .
We prove the intermediate
claim Ly :
ordinal y .
An
exact proof term for the current goal is
ordinal_Hered (F x ) LFx y Hy .
Apply Ly to the current goal.
Assume Hy1 _ .
An exact proof term for the current goal is Hy1 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Hb to the current goal.
Assume Hb1 _ .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Hb to the current goal.
Assume Hb1 _ .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hb .
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 Ha .
∎
Theorem. (
ordinal_ind )
∀p : set → prop , (∀alpha, ordinal alpha → (∀beta ∈ alpha , p beta ) → p alpha ) → ∀alpha, ordinal alpha → p alpha
Proof: Let p be given.
Apply In_ind to the current goal.
Let alpha be given.
We will prove p alpha .
Apply (H1 alpha H2 ) to the current goal.
Let beta be given.
We will prove p beta .
Apply (IH beta H3 ) to the current goal.
An
exact proof term for the current goal is
(ordinal_Hered alpha H2 beta H3 ) .
∎
Proof: Let p be given.
Assume H1 .
Apply dneg to the current goal.
We prove the intermediate
claim L1 :
∀alpha, ordinal alpha → ¬ p alpha .
Let alpha be given.
Assume Ha .
Assume H3 : p alpha .
Apply H2 to the current goal.
We use alpha to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is IH .
Apply H1 to the current goal.
Let alpha be given.
Assume H1a .
Apply H1a to the current goal.
Assume Hp : p alpha .
An exact proof term for the current goal is L1 alpha Ha Hp .
∎
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 .
Theorem. (
bijI )
∀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
Proof: Let X, Y and f be given.
Assume Hf1 Hf2 Hf3 .
We will
prove (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) ∧ (∀w ∈ Y , ∃u ∈ X , f u = w ) .
Apply and3I to the current goal.
An exact proof term for the current goal is Hf1 .
An exact proof term for the current goal is Hf2 .
An exact proof term for the current goal is Hf3 .
∎
Theorem. (
bijE )
∀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
Proof: Let X, Y and f be given.
Assume Hf .
Let p be given.
Assume Hp .
Apply Hf to the current goal.
Assume Hf .
Apply Hf to the current goal.
Assume Hf1 Hf2 Hf3 .
An exact proof term for the current goal is Hp Hf1 Hf2 Hf3 .
∎
Definition. We define
inv to be
λX f ⇒ λy : set ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y ) of type
set → (set → set ) → set → set .
Theorem. (
surj_rinv )
∀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
Proof: Let X, Y and f be given.
Assume H1 .
Let y be given.
Apply H1 y Hy to the current goal.
Let x be given.
Assume H2 .
An
exact proof term for the current goal is
Eps_i_ax (λx ⇒ x ∈ X ∧ f x = y ) x H2 .
∎
Theorem. (
inj_linv )
∀X, ∀f : set → set , (∀u v ∈ X , f u = f v → u = v ) → ∀x ∈ X , inv X f (f x ) = x
Proof: Let X and f be given.
Assume H1 .
Let x be given.
Assume Hx .
We prove the intermediate
claim L1 :
inv X f (f x ) ∈ X ∧ f (inv X f (f x ) ) = f x .
Apply Eps_i_ax (λx' ⇒ x' ∈ X ∧ f x' = f x ) x to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx .
Apply L1 to the current goal.
Assume H2 H3 .
An
exact proof term for the current goal is
H1 (inv X f (f x ) ) H2 x Hx H3 .
∎
Proof: Let X, Y and f be given.
Assume H1 .
Apply H1 to the current goal.
Assume H2 .
Apply H2 to the current goal.
Set g to be the term
λy ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y ) of type
set → set .
We prove the intermediate
claim L1 :
∀y ∈ Y , g y ∈ X ∧ f (g y ) = y .
An
exact proof term for the current goal is
surj_rinv X Y f H5 .
We will
prove (∀u ∈ Y , g u ∈ X ) ∧ (∀u v ∈ Y , g u = g v → u = v ) ∧ (∀w ∈ X , ∃u ∈ Y , g u = w ) .
Apply and3I to the current goal.
We will
prove ∀u ∈ Y , g u ∈ X .
Let u be given.
Assume Hu .
Apply L1 u Hu to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We will
prove ∀u v ∈ Y , g u = g v → u = v .
Let u be given.
Assume Hu .
Let v be given.
Assume Hv H6 .
Apply L1 u Hu to the current goal.
Apply L1 v Hv to the current goal.
rewrite the current goal using H8 (from right to left).
rewrite the current goal using H10 (from right to left).
rewrite the current goal using H6 (from right to left).
Use reflexivity.
We will
prove ∀w ∈ X , ∃u ∈ Y , g u = w .
Let w be given.
Assume Hw .
We prove the intermediate
claim Lfw :
f w ∈ Y .
An exact proof term for the current goal is H3 w Hw .
We use f w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lfw .
An
exact proof term for the current goal is
inj_linv X f H4 w Hw .
∎
Proof: Let X be given.
We will
prove (∀u ∈ X , u ∈ X ) ∧ (∀u v ∈ X , u = v → u = v ) ∧ (∀w ∈ X , ∃u ∈ X , u = w ) .
Apply and3I to the current goal.
An exact proof term for the current goal is (λu Hu ⇒ Hu ) .
An exact proof term for the current goal is (λu Hu v Hv H1 ⇒ H1 ) .
Let w be given.
Assume Hw .
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw .
∎
Theorem. (
bij_comp )
∀X Y Z : set , ∀f g : set → set , bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x ) )
Proof: Let X, Y, Z, f and g be given.
Assume Hf .
Apply Hf to the current goal.
Assume Hf12 Hf3 .
Apply Hf12 to the current goal.
Assume Hf1 Hf2 .
Assume Hg .
Apply Hg to the current goal.
Assume Hg12 Hg3 .
Apply Hg12 to the current goal.
Assume Hg1 Hg2 .
We will
prove (∀u ∈ X , g (f u ) ∈ Z ) ∧ (∀u v ∈ X , g (f u ) = g (f v ) → u = v ) ∧ (∀w ∈ Z , ∃u ∈ X , g (f u ) = w ) .
Apply and3I to the current goal.
Let u be given.
An exact proof term for the current goal is (Hg1 (f u ) (Hf1 u Hu ) ) .
Let u be given.
Let v be given.
Apply Hf2 u Hu v Hv to the current goal.
Apply Hg2 (f u ) (Hf1 u Hu ) (f v ) (Hf1 v Hv ) to the current goal.
We will
prove g (f u ) = g (f v ) .
An exact proof term for the current goal is H1 .
Let w be given.
Apply Hg3 w Hw to the current goal.
Let y be given.
Assume Hy12 .
Apply Hy12 to the current goal.
Apply Hf3 y Hy1 to the current goal.
Let u be given.
Assume Hu12 .
Apply Hu12 to the current goal.
We will
prove ∃u ∈ X , g (f u ) = w .
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu1 .
rewrite the current goal using Hu2 (from left to right).
An exact proof term for the current goal is Hy2 .
∎
Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set , bij X Y f of type
set → set → prop .
Proof: Let X be given.
We will
prove ∃f : set → set , bij X X f .
We use (λx : set ⇒ x ) to witness the existential quantifier.
An
exact proof term for the current goal is
bij_id X .
∎
Proof: Let X and Y be given.
Assume H1 .
Apply H1 to the current goal.
Let f be given.
We will
prove ∃g : set → set , bij Y X g .
We use
(inv X f ) to
witness the existential quantifier.
We will
prove bij Y X (inv X f ) .
An
exact proof term for the current goal is
bij_inv X Y f H2 .
∎
Proof: Let X, Y and Z be given.
Assume H1 H2 .
Apply H1 to the current goal.
Let f be given.
Apply H2 to the current goal.
Let g be given.
We will
prove ∃h : set → set , bij X Z h .
We use (λx : set ⇒ g (f x ) ) to witness the existential quantifier.
An
exact proof term for the current goal is
bij_comp X Y Z f g H3 H4 .
∎
Proof: Let X be given.
Assume H1 .
Let x be given.
Assume Hx .
Apply H1 to the current goal.
Let f be given.
Apply bijE X 0 f Hf to the current goal.
An
exact proof term for the current goal is
EmptyE (f x ) (Hf1 x Hx ) .
∎
Beginning of Section SchroederBernstein
Proof: Let A and F be given.
Assume H1 H2 .
Set Y to be the term
{ u ∈ A | ∀X ∈ 𝒫 A , F X ⊆ X → u ∈ X } of type
set .
We prove the intermediate
claim L1 :
Y ∈ 𝒫 A .
We prove the intermediate
claim L2 :
F Y ∈ 𝒫 A .
An exact proof term for the current goal is H1 Y L1 .
We prove the intermediate
claim L3 :
∀X ∈ 𝒫 A , F X ⊆ X → Y ⊆ X .
Let X be given.
Let y be given.
An
exact proof term for the current goal is
SepE2 A (λu ⇒ ∀X ∈ 𝒫 A , F X ⊆ X → u ∈ X ) y Hy X HX H3 .
We prove the intermediate
claim L4 :
F Y ⊆ Y .
Let u be given.
Apply SepI to the current goal.
An
exact proof term for the current goal is
PowerE A (F Y ) L2 u H3 .
Let X be given.
We prove the intermediate
claim L4a :
Y ⊆ X .
An exact proof term for the current goal is L3 X HX H4 .
We prove the intermediate
claim L4b :
F Y ⊆ F X .
An exact proof term for the current goal is H2 Y L1 X HX L4a .
Apply H4 to the current goal.
Apply L4b to the current goal.
An exact proof term for the current goal is H3 .
We prove the intermediate
claim L5 :
F (F Y ) ⊆ F Y .
An exact proof term for the current goal is H2 (F Y ) L2 Y L1 L4 .
We use Y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L4 .
Apply L3 to the current goal.
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is L5 .
∎
Proof: Let A, B and f be given.
Assume Hf .
Let U be given.
Assume HU .
Apply PowerI to the current goal.
Let y be given.
Let x be given.
rewrite the current goal using H1 (from left to right).
Apply Hf to the current goal.
Apply PowerE A U HU to the current goal.
An exact proof term for the current goal is Hx .
∎
Proof: Let f, U and V be given.
Assume HUV .
Let y be given.
Let x be given.
rewrite the current goal using H1 (from left to right).
We will
prove f x ∈ { f x | x ∈ V } .
Apply ReplI to the current goal.
Apply HUV to the current goal.
An exact proof term for the current goal is Hx .
∎
Proof: Let A, U and V be given.
Assume HUV .
Let x be given.
Assume Hx .
Apply setminusE A V x Hx to the current goal.
Assume H1 H2 .
An exact proof term for the current goal is H1 .
Apply H2 to the current goal.
An exact proof term for the current goal is HUV x H3 .
∎
Proof: Let A, B, f and g be given.
Assume Hf Hg .
Apply Hf to the current goal.
Assume Hf1 Hf2 .
Apply Hg to the current goal.
Assume Hg1 Hg2 .
Set F to be the term
λX ⇒ { g y | y ∈ B ∖ { f x | x ∈ A ∖ X } } of type
set → set .
We prove the intermediate
claim L1 :
∀U ∈ 𝒫 A , F U ∈ 𝒫 A .
Let U be given.
Assume HU .
We will
prove B ∖ { f x | x ∈ A ∖ U } ∈ 𝒫 B .
We prove the intermediate
claim L2 :
∀U V ∈ 𝒫 A , U ⊆ V → F U ⊆ F V .
Let U be given.
Assume HU .
Let V be given.
Assume HV HUV .
We will
prove A ∖ V ⊆ A ∖ U .
An exact proof term for the current goal is HUV .
Let Y be given.
Assume H1 .
Apply H1 to the current goal.
Set h to be the term
λx ⇒ if x ∈ Y then inv B g x else f x of type
set → set .
We will
prove ∃f : set → set , bij A B f .
We use h to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx .
Apply xm (x ∈ Y ) to the current goal.
rewrite the current goal using
If_i_1 (x ∈ Y ) (inv B g x ) (f x ) H3 (from left to right).
We will
prove inv B g x ∈ B .
We prove the intermediate
claim L1 :
x ∈ F Y .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H3 .
Let y be given.
We prove the intermediate
claim L2 :
y ∈ B .
An
exact proof term for the current goal is
setminusE1 B { f x | x ∈ A ∖ Y } y H4 .
rewrite the current goal using H5 (from left to right).
We will
prove inv B g (g y ) ∈ B .
rewrite the current goal using
inj_linv B g Hg2 y L2 (from left to right).
An exact proof term for the current goal is L2 .
rewrite the current goal using
If_i_0 (x ∈ Y ) (inv B g x ) (f x ) H3 (from left to right).
Apply Hf1 to the current goal.
An exact proof term for the current goal is Hx .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Apply xm (x ∈ Y ) to the current goal.
rewrite the current goal using
If_i_1 (x ∈ Y ) (inv B g x ) (f x ) H3 (from left to right).
We prove the intermediate
claim Lx :
x ∈ F Y .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H3 .
Let z be given.
Assume Hz1a Hz1b .
Apply xm (y ∈ Y ) to the current goal.
rewrite the current goal using
If_i_1 (y ∈ Y ) (inv B g y ) (f y ) H4 (from left to right).
We will
prove inv B g x = inv B g y → x = y .
We prove the intermediate
claim Ly :
y ∈ F Y .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4 .
Let w be given.
rewrite the current goal using Hz2 (from left to right).
rewrite the current goal using Hw2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 z Hz1a (from left to right).
Use f_equal.
An exact proof term for the current goal is H5 .
rewrite the current goal using
If_i_0 (y ∈ Y ) (inv B g y ) (f y ) H4 (from left to right).
We will
prove inv B g x = f y → x = y .
rewrite the current goal using Hz2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 z Hz1a (from left to right).
We will
prove z = f y → g z = y .
Apply Hz1b to the current goal.
We will
prove z ∈ { f x | x ∈ A ∖ Y } .
rewrite the current goal using H5 (from left to right).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is H4 .
rewrite the current goal using
If_i_0 (x ∈ Y ) (inv B g x ) (f x ) H3 (from left to right).
Apply xm (y ∈ Y ) to the current goal.
rewrite the current goal using
If_i_1 (y ∈ Y ) (inv B g y ) (f y ) H4 (from left to right).
We will
prove f x = inv B g y → x = y .
We prove the intermediate
claim Ly :
y ∈ F Y .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4 .
Let w be given.
Assume Hw1a Hw1b .
rewrite the current goal using Hw2 (from left to right).
rewrite the current goal using
inj_linv B g Hg2 w Hw1a (from left to right).
Apply Hw1b to the current goal.
We will
prove w ∈ { f x | x ∈ A ∖ Y } .
rewrite the current goal using H5 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is H3 .
rewrite the current goal using
If_i_0 (y ∈ Y ) (inv B g y ) (f y ) H4 (from left to right).
We will
prove f x = f y → x = y .
An exact proof term for the current goal is Hf2 x Hx y Hy .
Let w be given.
Apply xm (w ∈ { f x | x ∈ A ∖ Y } ) to the current goal.
Let x be given.
Apply setminusE A Y x H4 to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6 .
rewrite the current goal using
If_i_0 (x ∈ Y ) (inv B g x ) (f x ) H7 (from left to right).
Use symmetry.
An exact proof term for the current goal is H5 .
We prove the intermediate
claim Lgw :
g w ∈ Y .
rewrite the current goal using H2 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hw .
We will
prove w ∉ { f x | x ∈ A ∖ Y } .
An exact proof term for the current goal is H3 .
We use (g w ) to witness the existential quantifier.
Apply andI to the current goal.
Apply Hg1 to the current goal.
An exact proof term for the current goal is Hw .
rewrite the current goal using
If_i_1 (g w ∈ Y ) (inv B g (g w ) ) (f (g w ) ) Lgw (from left to right).
An
exact proof term for the current goal is
inj_linv B g Hg2 w Hw .
∎
End of Section SchroederBernstein
Beginning of Section PigeonHole
Proof:
We will
prove ∀f : set → set , (∀i ∈ 1 , f i ∈ 0 ) → ¬ (∀i j ∈ 1 , f i = f j → i = j ) .
Let f be given.
Assume H1 .
Let n be given.
Let f be given.
Assume H3 .
Apply H3 to the current goal.
Let k be given.
Assume Hk .
Apply Hk to the current goal.
Apply IH f' to the current goal.
Let i be given.
Apply xm (k ⊆ i ) to the current goal.
rewrite the current goal using
If_i_1 (k ⊆ i ) (f (ordsucc i ) ) (f i ) H4 (from left to right).
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is H5 .
We prove the intermediate
claim L2 :
k = ordsucc i .
Apply H2 to the current goal.
An exact proof term for the current goal is Hk1 .
An exact proof term for the current goal is L1 .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is Hk2 .
We prove the intermediate
claim L3 :
i ∈ k .
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is H4 i L3 .
rewrite the current goal using
If_i_0 (k ⊆ i ) (f (ordsucc i ) ) (f i ) H4 (from left to right).
An exact proof term for the current goal is H5 .
Apply H4 to the current goal.
We prove the intermediate
claim L2 :
k = i .
Apply H2 to the current goal.
An exact proof term for the current goal is Hk1 .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is Hk2 .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is (λx Hx ⇒ Hx ) .
We will
prove ∀i j ∈ ordsucc n , f' i = f' j → i = j .
Let i be given.
Assume Hi .
Let j be given.
Assume Hj .
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is Hj .
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hj .
Apply xm (k ⊆ i ) to the current goal.
rewrite the current goal using
If_i_1 (k ⊆ i ) (f (ordsucc i ) ) (f i ) H4 (from left to right).
Apply xm (k ⊆ j ) to the current goal.
rewrite the current goal using
If_i_1 (k ⊆ j ) (f (ordsucc j ) ) (f j ) H5 (from left to right).
Assume H6 .
An
exact proof term for the current goal is
H2 (ordsucc i ) Li2 (ordsucc j ) Lj2 H6 .
rewrite the current goal using
If_i_0 (k ⊆ j ) (f (ordsucc j ) ) (f j ) H5 (from left to right).
Assume H6 .
We prove the intermediate
claim L3 :
ordsucc i = j .
Apply H2 to the current goal.
An exact proof term for the current goal is Li2 .
An exact proof term for the current goal is Lj1 .
An exact proof term for the current goal is H6 .
Apply H5 to the current goal.
rewrite the current goal using L3 (from right to left).
Let x be given.
Apply H4 to the current goal.
An exact proof term for the current goal is Hx .
rewrite the current goal using
If_i_0 (k ⊆ i ) (f (ordsucc i ) ) (f i ) H4 (from left to right).
Apply xm (k ⊆ j ) to the current goal.
rewrite the current goal using
If_i_1 (k ⊆ j ) (f (ordsucc j ) ) (f j ) H5 (from left to right).
Assume H6 .
We prove the intermediate
claim L3 :
i = ordsucc j .
Apply H2 to the current goal.
An exact proof term for the current goal is Li1 .
An exact proof term for the current goal is Lj2 .
An exact proof term for the current goal is H6 .
Apply H4 to the current goal.
rewrite the current goal using L3 (from left to right).
Let x be given.
Apply H5 to the current goal.
An exact proof term for the current goal is Hx .
rewrite the current goal using
If_i_0 (k ⊆ j ) (f (ordsucc j ) ) (f j ) H5 (from left to right).
We will
prove f i = f j → i = j .
Apply H2 to the current goal.
An exact proof term for the current goal is Li1 .
An exact proof term for the current goal is Lj1 .
Apply IH f to the current goal.
Let i be given.
An exact proof term for the current goal is Hfi .
Apply H3 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is Hfi .
We will
prove ∀i j ∈ ordsucc n , f i = f j → i = j .
Let i be given.
Assume Hi .
Let j be given.
Assume Hj .
Apply H2 to the current goal.
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is Hj .
∎
Proof: Let n be given.
Assume Hn .
Let f be given.
Assume Hf1 Hf2 .
We will
prove (∀i ∈ n , f i ∈ n ) ∧ (∀i j ∈ n , f i = f j → i = j ) ∧ (∀j ∈ n , ∃i ∈ n , f i = j ) .
Apply and3I to the current goal.
An exact proof term for the current goal is Hf1 .
An exact proof term for the current goal is Hf2 .
Let j be given.
Apply dneg to the current goal.
Set f' to be the term
λi : set ⇒ if i = n then j else f i .
Let i be given.
Assume Hi .
Apply xm (i = n ) to the current goal.
rewrite the current goal using
If_i_1 (i = n ) j (f i ) H1 (from left to right).
An exact proof term for the current goal is Hj .
rewrite the current goal using
If_i_0 (i = n ) j (f i ) H1 (from left to right).
Apply Hf1 to the current goal.
Apply ordsuccE n i Hi to the current goal.
An exact proof term for the current goal is H2 .
Apply H1 H2 to the current goal.
We will
prove ∀i k ∈ ordsucc n , f' i = f' k → i = k .
Let i be given.
Assume Hi .
Let k be given.
Assume Hk .
We prove the intermediate
claim Li :
i ≠ n → i ∈ n .
Apply ordsuccE n i Hi to the current goal.
Assume H2 .
An exact proof term for the current goal is H2 .
Assume H2 .
Apply Hin H2 to the current goal.
We prove the intermediate
claim Lk :
k ≠ n → k ∈ n .
Apply ordsuccE n k Hk to the current goal.
Assume H2 .
An exact proof term for the current goal is H2 .
Assume H2 .
Apply Hkn H2 to the current goal.
Apply xm (i = n ) to the current goal.
Apply xm (k = n ) to the current goal.
Assume _ .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is H2 .
rewrite the current goal using
If_i_1 (i = n ) j (f i ) H2 (from left to right).
rewrite the current goal using
If_i_0 (k = n ) j (f k ) H3 (from left to right).
Apply H1 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lk H3 .
Use symmetry.
An exact proof term for the current goal is H4 .
Apply xm (k = n ) to the current goal.
rewrite the current goal using
If_i_0 (i = n ) j (f i ) H2 (from left to right).
rewrite the current goal using
If_i_1 (k = n ) j (f k ) H3 (from left to right).
Apply H1 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Li H2 .
An exact proof term for the current goal is H4 .
rewrite the current goal using
If_i_0 (i = n ) j (f i ) H2 (from left to right).
rewrite the current goal using
If_i_0 (k = n ) j (f k ) H3 (from left to right).
We will
prove f i = f k → i = k .
Apply Hf2 to the current goal.
An exact proof term for the current goal is Li H2 .
An exact proof term for the current goal is Lk H3 .
∎
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃n ∈ ω , equip X n of type
set → prop .
Proof: Let p be given.
Assume H1 H2 .
We prove the intermediate
claim L1 :
∀n, nat_p n → ∀X, equip X n → p X .
Let X be given.
rewrite the current goal using
equip_0_Empty X H3 (from left to right).
An exact proof term for the current goal is H1 .
Let n be given.
Assume Hn .
Let X be given.
Let f be given.
Set Z to be the term
{ f i | i ∈ n } .
Set y to be the term f n .
We prove the intermediate
claim L1a :
X = Z ∪ { y } .
Let x be given.
Apply Hf3 x Hx to the current goal.
Let i be given.
Assume H .
Apply H to the current goal.
Apply ordsuccE n i Hi to the current goal.
rewrite the current goal using H4 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is H5 .
rewrite the current goal using H4 (from right to left).
rewrite the current goal using H5 (from left to right).
An
exact proof term for the current goal is
SingI (f n ) .
Let x be given.
Let i be given.
rewrite the current goal using H5 (from left to right).
An
exact proof term for the current goal is
Hf1 i (ordsuccI1 n i Hi ) .
rewrite the current goal using
SingE y x H4 (from left to right).
An
exact proof term for the current goal is
Hf1 n (ordsuccI2 n ) .
We prove the intermediate
claim L1b :
equip Z n .
We will
prove ∃f : set → set , bij n Z f .
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi .
We will
prove f i ∈ { f i | i ∈ n } .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hi .
Let i be given.
Assume Hi .
Let j be given.
Assume Hj .
Apply Hf2 to the current goal.
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is Hj .
Apply ReplE' to the current goal.
Let i be given.
We will
prove ∃i' ∈ n , f i' = f i .
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi .
rewrite the current goal using L1a (from left to right).
We will
prove p (Z ∪ { y } ) .
Apply H2 Z y to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_p_omega n Hn .
An exact proof term for the current goal is L1b .
Let i be given.
rewrite the current goal using
Hf2 n (ordsuccI2 n ) i (ordsuccI1 n i Hi ) H5 (from left to right) at position 1.
An exact proof term for the current goal is Hi .
We will prove p Z .
An exact proof term for the current goal is IHn Z L1b .
Let X be given.
Assume H3 .
Apply H3 to the current goal.
Let n be given.
Assume H .
Apply H to the current goal.
An
exact proof term for the current goal is
L1 n (omega_nat_p n Hn ) X H4 .
∎
Proof:
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
∎
Proof: Let X and y be given.
Assume H1 .
Apply H1 to the current goal.
Let n be given.
Assume H .
Apply H to the current goal.
Let f be given.
Apply bijE n X f Hf to the current goal.
Apply xm (y ∈ X ) to the current goal.
We prove the intermediate
claim L1 :
X ∪ { y } = X .
Let x be given.
Assume Hx .
Assume H4 .
An exact proof term for the current goal is H4 .
rewrite the current goal using
SingE y x H4 (from left to right).
An exact proof term for the current goal is H3 .
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H1 .
We use
ordsucc n to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
We prove the intermediate
claim Lg :
∃g : set → set , (∀i ∈ n , g i = f i ) ∧ g n = y .
We use
(λi : set ⇒ if i ∈ n then f i else y ) to
witness the existential quantifier.
Apply andI to the current goal.
Let i be given.
Assume Hi .
An
exact proof term for the current goal is
If_i_1 (i ∈ n ) (f i ) y Hi .
An
exact proof term for the current goal is
If_i_0 (n ∈ n ) (f n ) y (In_irref n ) .
Apply Lg to the current goal.
Let g be given.
Assume H .
Apply H to the current goal.
Assume Hg1 Hg2 .
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi .
Apply ordsuccE n i Hi to the current goal.
rewrite the current goal using Hg1 i H4 (from left to right).
An exact proof term for the current goal is Hf1 i H4 .
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Apply SingI to the current goal.
We will
prove ∀i j ∈ ordsucc n , g i = g j → i = j .
Let i be given.
Assume Hi .
Let j be given.
Assume Hj .
Apply ordsuccE n i Hi to the current goal.
rewrite the current goal using Hg1 i H4 (from left to right).
Apply ordsuccE n j Hj to the current goal.
rewrite the current goal using Hg1 j H5 (from left to right).
An exact proof term for the current goal is Hf2 i H4 j H5 .
rewrite the current goal using H5 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Apply H3 to the current goal.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hf1 i H4 .
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Apply ordsuccE n j Hj to the current goal.
rewrite the current goal using Hg1 j H5 (from left to right).
Apply H3 to the current goal.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hf1 j H5 .
rewrite the current goal using H5 (from left to right).
Assume _ .
Use reflexivity.
Let x be given.
Assume Hx .
Apply Hf3 x H4 to the current goal.
Let i be given.
Assume H .
Apply H to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi .
rewrite the current goal using Hg1 i Hi (from left to right).
An exact proof term for the current goal is H5 .
We use n to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using
SingE y x H4 (from left to right).
An exact proof term for the current goal is Hg2 .
∎
Proof: Let X be given.
Assume HX .
rewrite the current goal using
binunion_idr X (from left to right).
An exact proof term for the current goal is HX .
Let Y and z be given.
rewrite the current goal using
binunion_asso (from left to right).
An exact proof term for the current goal is IH .
∎
Proof: Let X be given.
Let n be given.
Assume Hn .
We prove the intermediate
claim L1 :
(⋃ i ∈ ordsucc n X i ) = (⋃ i ∈ n X i ) ∪ X n .
Let z be given.
Let i be given.
Apply ordsuccE n i Hi to the current goal.
An
exact proof term for the current goal is
famunionI n X i z H3 H2 .
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H2 .
Let z be given.
Assume Hz .
Let i be given.
An exact proof term for the current goal is Hi .
An exact proof term for the current goal is H2 .
Assume Hz .
An exact proof term for the current goal is Hz .
rewrite the current goal using L1 (from left to right).
Apply IHn to the current goal.
Let i be given.
Apply H1 to the current goal.
An exact proof term for the current goal is Hi .
Apply H1 n to the current goal.
∎
Proof:
Let Y be given.
rewrite the current goal using
Empty_Subq_eq Y H1 (from left to right).
Let X and z be given.
Let Y be given.
Apply xm (z ∈ Y ) to the current goal.
We prove the intermediate
claim L1 :
Y = (Y ∖ { z } ) ∪ { z } .
Let w be given.
Apply xm (w ∈ { z } ) to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Hw .
An exact proof term for the current goal is H3 .
Let w be given.
An
exact proof term for the current goal is
setminusE1 Y { z } w H3 .
rewrite the current goal using
SingE z w H3 (from left to right).
An exact proof term for the current goal is H2 .
rewrite the current goal using L1 (from left to right).
Apply IH to the current goal.
Let y be given.
Apply binunionE X { z } y (H1 y Hy1 ) to the current goal.
An exact proof term for the current goal is H3 .
Apply Hy2 to the current goal.
An exact proof term for the current goal is H3 .
Apply IH to the current goal.
Let y be given.
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
rewrite the current goal using
SingE z y H3 (from right to left).
An exact proof term for the current goal is Hy .
∎
Proof: Let x and y be given.
Assume H1 H2 .
Apply ordsuccE y x H2 to the current goal.
An exact proof term for the current goal is H1 x H3 .
rewrite the current goal using H3 (from left to right).
∎
Theorem. (
exandE_i )
∀P Q : set → prop , (∃x, P x ∧ Q x ) → ∀r : prop , (∀x, P x → Q x → r ) → r
Proof: Let P and Q be given.
Assume H1 .
Let r be given.
Assume Hr .
Apply H1 to the current goal.
Let x be given.
Assume H2 .
Apply H2 to the current goal.
An exact proof term for the current goal is Hr x .
∎
Theorem. (
exandE_ii )
∀P Q : (set → set ) → prop , (∃x : set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set , P x → Q x → p ) → p
Proof: Let P and Q be given.
Assume H .
Let p be given.
Assume Hp .
Apply H to the current goal.
Let x be given.
Assume H0 .
Apply H0 to the current goal.
Assume H1 H2 .
An exact proof term for the current goal is Hp x H1 H2 .
∎
Theorem. (
exandE_iii )
∀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
Proof: Let P and Q be given.
Assume H .
Let p be given.
Assume Hp .
Apply H to the current goal.
Let x be given.
Assume H0 .
Apply H0 to the current goal.
Assume H1 H2 .
An exact proof term for the current goal is Hp x H1 H2 .
∎
Theorem. (
exandE_iiii )
∀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
Proof: Let P and Q be given.
Assume H .
Let p be given.
Assume Hp .
Apply H to the current goal.
Let x be given.
Assume H0 .
Apply H0 to the current goal.
Assume H1 H2 .
An exact proof term for the current goal is Hp x H1 H2 .
∎
Beginning of Section Descr_ii
Variable P : (set → set ) → prop
Definition. We define
Descr_ii to be
λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set , P h → h x = y ) of type
set → set .
Hypothesis Pex : ∃f : set → set , P f
Hypothesis Puniq : ∀f g : set → set , P f → P g → f = g
Proof: Apply Pex to the current goal.
Let f be given.
Assume Hf : P f .
We prove the intermediate
claim L1 :
f = Descr_ii .
Apply func_ext set set to the current goal.
Let x be given.
We will
prove f x = Eps_i (λy ⇒ ∀h : set → set , P h → h x = y ) .
We prove the intermediate
claim L2 :
∀h : set → set , P h → h x = f x .
Let h be given.
Assume Hh .
rewrite the current goal using Puniq f h Hf Hh (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
We prove the intermediate
claim L3 :
∀h : set → set , P h → h x = Descr_ii x .
An
exact proof term for the current goal is
Eps_i_ax (λy ⇒ ∀h : set → set , P h → h x = y ) (f x ) L2 .
An exact proof term for the current goal is L3 f Hf .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hf .
∎
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set ) → prop
Definition. We define
Descr_iii to be
λx y : set ⇒ Eps_i (λz ⇒ ∀h : set → set → set , P h → h x y = z ) 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
Proof: Apply Pex to the current goal.
Let f be given.
Assume Hf : P f .
We prove the intermediate
claim L1 :
f = Descr_iii .
Apply func_ext set (set → set ) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
We will
prove f x y = Eps_i (λz ⇒ ∀h : set → set → set , P h → h x y = z ) .
We prove the intermediate
claim L2 :
∀h : set → set → set , P h → h x y = f x y .
Let h be given.
Assume Hh .
rewrite the current goal using Puniq f h Hf Hh (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
We prove the intermediate
claim L3 :
∀h : set → set → set , P h → h x y = Descr_iii x y .
An
exact proof term for the current goal is
Eps_i_ax (λz ⇒ ∀h : set → set → set , P h → h x y = z ) (f x y ) L2 .
An exact proof term for the current goal is L3 f Hf .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hf .
∎
End of Section Descr_iii
Beginning of Section Descr_Vo1
Definition. We define
Descr_Vo1 to be
λx : set ⇒ ∀h : set → prop , P h → h x of type
Vo 1 .
Hypothesis Pex : ∃f : Vo 1 , P f
Hypothesis Puniq : ∀f g : Vo 1 , P f → P g → f = g
Proof: Apply Pex to the current goal.
Let f be given.
Assume Hf : P f .
We prove the intermediate
claim L1 :
f = Descr_Vo1 .
Apply func_ext set prop to the current goal.
Let x be given.
Assume H1 : f x .
Let h be given.
Assume Hh : P h .
We will prove h x .
rewrite the current goal using Puniq f h Hf Hh (from right to left).
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H1 f Hf .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hf .
∎
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Definition. We define
If_ii to be
λx ⇒ if p then f x else g x of type
set → set .
Proof: Assume H1 .
Apply func_ext set set to the current goal.
Let x be given.
An
exact proof term for the current goal is
If_i_1 p (f x ) (g x ) H1 .
∎
Proof: Assume H1 .
Apply func_ext set set to the current goal.
Let x be given.
An
exact proof term for the current goal is
If_i_0 p (f x ) (g x ) H1 .
∎
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Definition. We define
If_iii to be
λx y ⇒ if p then f x y else g x y of type
set → set → set .
Proof: Assume H1 .
Apply func_ext set (set → set ) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
An
exact proof term for the current goal is
If_i_1 p (f x y ) (g x y ) H1 .
∎
Proof: Assume H1 .
Apply func_ext set (set → set ) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
An
exact proof term for the current goal is
If_i_0 p (f x y ) (g x y ) H1 .
∎
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set ) → set
Definition. We define
In_rec_i_G to be
λX Y ⇒ ∀R : set → set → prop , (∀X : set , ∀f : set → set , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → set → prop .
Proof: Let X of type set be given.
Let f of type set → set be given.
Let R of type set → set → prop be given.
We will prove R X (F X f ) .
Apply (H2 X f ) to the current goal.
We will
prove ∀x ∈ X , R x (f x ) .
Let x of type set be given.
We will prove R x (f x ) .
An exact proof term for the current goal is (H1 x H3 R H2 ) .
∎
Proof: Let X and Y be given.
Set R to be the term
(λX : set ⇒ λY : set ⇒ ∃f : set → set , (∀x ∈ X , In_rec_i_G x (f x ) ) ∧ Y = F X f ) .
Apply (H1 R ) to the current goal.
We will
prove ∀Z : set , ∀g : set → set , (∀z ∈ Z , R z (g z ) ) → R Z (F Z g ) .
Let Z and g be given.
We will
prove ∃f : set → set , (∀x ∈ Z , In_rec_i_G x (f x ) ) ∧ F Z g = F Z f .
We use g to witness the existential quantifier.
Apply andI to the current goal.
Let z be given.
Let f of type set → set be given.
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
(In_rec_i_G_c z f H3 ) .
∎
Hypothesis Fr : ∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Apply In_ind to the current goal.
Let X be given.
Let Y and Z be given.
We prove the intermediate
claim L1 :
∃f : set → set , (∀x ∈ X , In_rec_i_G x (f x ) ) ∧ Y = F X f .
We prove the intermediate
claim L2 :
∃f : set → set , (∀x ∈ X , In_rec_i_G x (f x ) ) ∧ Z = F X f .
Let g be given.
Let h be given.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H6 (from left to right).
We will
prove F X g = F X h .
Apply Fr to the current goal.
We will
prove ∀x ∈ X , g x = h x .
Let x be given.
An exact proof term for the current goal is (IH x H7 (g x ) (h x ) (H3 x H7 ) (H5 x H7 ) ) .
∎
Proof: Apply In_ind to the current goal.
Let X be given.
∎
Proof: Let X and R be given.
Apply (H1 X In_rec_i ) to the current goal.
Let x be given.
Assume _ .
∎
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set ) ) → (set → set )
Definition. We define
In_rec_G_ii to be
λX Y ⇒ ∀R : set → (set → set ) → prop , (∀X : set , ∀f : set → (set → set ) , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → (set → set ) → prop .
Proof: Let X of type set be given.
Let f of type set → (set → set ) be given.
Let R of type set → (set → set ) → prop be given.
We will prove R X (F X f ) .
Apply (H2 X f ) to the current goal.
We will
prove ∀x ∈ X , R x (f x ) .
Let x of type set be given.
We will prove R x (f x ) .
An exact proof term for the current goal is (H1 x H3 R H2 ) .
∎
Proof: Let X and Y be given.
Set R to be the term
(λX : set ⇒ λY : (set → set ) ⇒ ∃f : set → (set → set ) , (∀x ∈ X , In_rec_G_ii x (f x ) ) ∧ Y = F X f ) .
Apply (H1 R ) to the current goal.
We will
prove ∀Z : set , ∀g : set → (set → set ) , (∀z ∈ Z , R z (g z ) ) → R Z (F Z g ) .
Let Z and g be given.
We will
prove ∃f : set → (set → set ) , (∀x ∈ Z , In_rec_G_ii x (f x ) ) ∧ F Z g = F Z f .
We use g to witness the existential quantifier.
Apply andI to the current goal.
Let z be given.
Let f of type set → (set → set ) be given.
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
(In_rec_G_ii_c z f H3 ) .
An exact proof term for the current goal is (λq H ⇒ H ) .
∎
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Apply In_ind to the current goal.
Let X be given.
Let Y and Z be given.
We prove the intermediate
claim L1 :
∃f : set → (set → set ) , (∀x ∈ X , In_rec_G_ii x (f x ) ) ∧ Y = F X f .
We prove the intermediate
claim L2 :
∃f : set → (set → set ) , (∀x ∈ X , In_rec_G_ii x (f x ) ) ∧ Z = F X f .
Let g be given.
Let h be given.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H6 (from left to right).
We will
prove F X g = F X h .
Apply Fr to the current goal.
We will
prove ∀x ∈ X , g x = h x .
Let x be given.
An exact proof term for the current goal is (IH x H7 (g x ) (h x ) (H3 x H7 ) (H5 x H7 ) ) .
∎
Proof: Apply In_ind to the current goal.
Let X be given.
We use
(F X In_rec_ii ) to
witness the existential quantifier.
∎
Proof: Let X and R be given.
Let x be given.
Assume _ .
∎
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set ) ) → (set → set → set )
Definition. We define
In_rec_G_iii to be
λX Y ⇒ ∀R : set → (set → set → set ) → prop , (∀X : set , ∀f : set → (set → set → set ) , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → (set → set → set ) → prop .
Proof: Let X of type set be given.
Let f of type set → (set → set → set ) be given.
Let R of type set → (set → set → set ) → prop be given.
We will prove R X (F X f ) .
Apply (H2 X f ) to the current goal.
We will
prove ∀x ∈ X , R x (f x ) .
Let x of type set be given.
We will prove R x (f x ) .
An exact proof term for the current goal is (H1 x H3 R H2 ) .
∎
Proof: Let X and Y be given.
Set R to be the term
(λX : set ⇒ λY : (set → set → set ) ⇒ ∃f : set → (set → set → set ) , (∀x ∈ X , In_rec_G_iii x (f x ) ) ∧ Y = F X f ) .
Apply (H1 R ) to the current goal.
We will
prove ∀Z : set , ∀g : set → (set → set → set ) , (∀z ∈ Z , R z (g z ) ) → R Z (F Z g ) .
Let Z and g be given.
We will
prove ∃f : set → (set → set → set ) , (∀x ∈ Z , In_rec_G_iii x (f x ) ) ∧ F Z g = F Z f .
We use g to witness the existential quantifier.
Apply andI to the current goal.
Let z be given.
Let f of type set → (set → set → set ) be given.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
∎
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Apply In_ind to the current goal.
Let X be given.
Let Y and Z be given.
We prove the intermediate
claim L1 :
∃f : set → (set → set → set ) , (∀x ∈ X , In_rec_G_iii x (f x ) ) ∧ Y = F X f .
We prove the intermediate
claim L2 :
∃f : set → (set → set → set ) , (∀x ∈ X , In_rec_G_iii x (f x ) ) ∧ Z = F X f .
Let g be given.
Let h be given.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H6 (from left to right).
We will
prove F X g = F X h .
Apply Fr to the current goal.
We will
prove ∀x ∈ X , g x = h x .
Let x be given.
An exact proof term for the current goal is (IH x H7 (g x ) (h x ) (H3 x H7 ) (H5 x H7 ) ) .
∎
Proof: Apply In_ind to the current goal.
Let X be given.
We use
(F X In_rec_iii ) to
witness the existential quantifier.
∎
Proof: Let X and R be given.
Let x be given.
Assume _ .
∎
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
Theorem. (
nat_primrec_r )
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Let X, g and h be given.
We will
prove F X g = F X h .
Apply xm (⋃ X ∈ X ) to the current goal.
rewrite the current goal using
(H1 (⋃ X ) H2 ) (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
We prove the intermediate
claim L1 :
(if ⋃ X ∈ X then f (⋃ X ) (g (⋃ X ) ) else z ) = z .
An
exact proof term for the current goal is
(If_i_0 (⋃ X ∈ X ) (f (⋃ X ) (g (⋃ X ) ) ) z H2 ) .
We prove the intermediate
claim L2 :
(if ⋃ X ∈ X then f (⋃ X ) (h (⋃ X ) ) else z ) = z .
An
exact proof term for the current goal is
(If_i_0 (⋃ X ∈ X ) (f (⋃ X ) (h (⋃ X ) ) ) z H2 ) .
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is L1 .
∎
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 .
Proof: Let n and m be given.
Assume Hm .
∎
Proof: Let n be given.
rewrite the current goal using
(add_nat_0R n ) (from left to right).
An exact proof term for the current goal is Hn .
Let m be given.
rewrite the current goal using
(add_nat_SR n m Hm ) (from left to right).
An exact proof term for the current goal is IHm .
∎
Proof: Use symmetry.
rewrite the current goal using
add_nat_0R 1 (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
∎
Proof:
Let m be given.
rewrite the current goal using
(add_nat_SR 0 m Hm ) (from left to right).
rewrite the current goal using IHm (from left to right).
Use reflexivity.
∎
Proof: Let n be given.
rewrite the current goal using
add_nat_0R (from left to right).
rewrite the current goal using
add_nat_0R (from left to right).
Use reflexivity.
Let m be given.
rewrite the current goal using
(add_nat_SR n m Hm ) (from left to right).
rewrite the current goal using IHm (from left to right).
Use reflexivity.
∎
Proof: Let n be given.
We will
prove n + 0 = 0 + n .
rewrite the current goal using
(add_nat_0L n Hn ) (from left to right).
An
exact proof term for the current goal is
(add_nat_0R n ) .
Let m be given.
rewrite the current goal using
(add_nat_SL m Hm n Hn ) (from left to right).
rewrite the current goal using IHm (from right to left).
An
exact proof term for the current goal is
(add_nat_SR n m Hm ) .
∎
Proof:
Let m be given.
Assume Hm Hnm .
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm .
Use symmetry.
An
exact proof term for the current goal is
add_nat_0R m .
Let n be given.
Assume Hn .
Apply EmptyE n to the current goal.
Apply Hnm to the current goal.
Let m be given.
We prove the intermediate
claim Lnm :
n ⊆ m .
Apply Hnm to the current goal.
An exact proof term for the current goal is H1 .
Apply IH m Hm Lnm to the current goal.
Let k be given.
Assume H .
Apply H to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
rewrite the current goal using
add_nat_SR k n Hn (from left to right).
Use f_equal.
An exact proof term for the current goal is H1 .
∎
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 .
Proof: Let n be given.
An
exact proof term for the current goal is
(nat_primrec_0 0 (λ_ r ⇒ n + r ) ) .
∎
Proof: Let n and m be given.
Assume Hm .
An
exact proof term for the current goal is
(nat_primrec_S 0 (λ_ r ⇒ n + r ) m Hm ) .
∎
Proof: Let n be given.
rewrite the current goal using
(mul_nat_0R n ) (from left to right).
An
exact proof term for the current goal is
nat_0 .
Let m be given.
rewrite the current goal using
(mul_nat_SR n m Hm ) (from left to right).
An
exact proof term for the current goal is
(add_nat_p n Hn (n * m ) IHm ) .
∎
End of Section NatArith
Proof: We prove the intermediate
claim L1 :
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → { 0 } ∪ { g x | x ∈ X } = { 0 } ∪ { h x | x ∈ X } .
Let X, g and h be given.
We prove the intermediate
claim L1a :
{ g x | x ∈ X } = { h x | x ∈ X } .
An
exact proof term for the current goal is
(ReplEq_ext X g h H ) .
rewrite the current goal using L1a (from left to right).
Use reflexivity.
∎
Proof: Let X be given.
rewrite the current goal using
(Inj1_eq X ) (from left to right).
Apply SingI to the current goal.
∎
Proof: Let X and x be given.
rewrite the current goal using
(Inj1_eq X ) (from left to right).
An
exact proof term for the current goal is
(ReplI X Inj1 x H ) .
∎
Proof: Let X and y be given.
rewrite the current goal using
(Inj1_eq X ) (from left to right).
Apply orIL to the current goal.
An
exact proof term for the current goal is
(SingE 0 y H2 ) .
Apply orIR to the current goal.
We will
prove ∃x ∈ X , y = Inj1 x .
An
exact proof term for the current goal is
(ReplE X Inj1 y H2 ) .
∎
Proof: Let x be given.
Apply (EmptyE 0 ) to the current goal.
rewrite the current goal using H1 (from right to left) at position 2.
An
exact proof term for the current goal is
(Inj1I1 x ) .
∎
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Proof: An
exact proof term for the current goal is
(λX x H ⇒ ReplI X Inj1 x H ) .
∎
Proof: An
exact proof term for the current goal is
(λX y H ⇒ ReplE X Inj1 y H ) .
∎
Proof: We prove the intermediate
claim L1 :
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → { g x | x ∈ X ∖ { 0 } } = { h x | x ∈ X ∖ { 0 } } .
Let X, g and h be given.
Let x be given.
Apply H1 to the current goal.
An
exact proof term for the current goal is
(setminusE1 X { 0 } x H2 ) .
∎
Proof: Apply In_ind to the current goal.
Let X be given.
rewrite the current goal using
Unj_eq (from left to right).
Let x be given.
Let y be given.
rewrite the current goal using H3 (from left to right).
Apply (Inj1E X y H4 ) to the current goal.
Apply H5 to the current goal.
rewrite the current goal using H6 (from left to right).
Apply SingI to the current goal.
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ y = Inj1 x ) H6 ) to the current goal.
Let z be given.
rewrite the current goal using H8 (from left to right).
rewrite the current goal using (IH z H7 ) (from left to right).
An exact proof term for the current goal is H7 .
Let x be given.
rewrite the current goal using (IH x H1 ) (from right to left).
An
exact proof term for the current goal is
(Inj1I2 X x H1 ) .
An
exact proof term for the current goal is
(Inj1NE2 x ) .
∎
Proof: Let X and Y be given.
rewrite the current goal using
(Unj_Inj1_eq X ) (from right to left).
rewrite the current goal using
(Unj_Inj1_eq Y ) (from right to left).
rewrite the current goal using H1 (from left to right).
Use reflexivity.
∎
Proof: Let X be given.
rewrite the current goal using
(Unj_eq (Inj0 X ) ) (from left to right).
Let x be given.
Let y be given.
Let z be given.
We prove the intermediate
claim L1 :
x = z .
rewrite the current goal using H3 (from left to right).
rewrite the current goal using H7 (from left to right).
An
exact proof term for the current goal is
(Unj_Inj1_eq z ) .
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H6 .
Let x be given.
rewrite the current goal using
(Unj_Inj1_eq x ) (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is H1 .
An
exact proof term for the current goal is
(Inj1NE2 x ) .
∎
Proof: Let X and Y be given.
rewrite the current goal using
(Unj_Inj0_eq X ) (from right to left).
rewrite the current goal using
(Unj_Inj0_eq Y ) (from right to left).
rewrite the current goal using H1 (from left to right).
Use reflexivity.
∎
Proof: Let X and Y be given.
We prove the intermediate
claim L1 :
0 ∈ Inj1 Y .
An
exact proof term for the current goal is
(Inj1I1 Y ) .
We prove the intermediate
claim L2 :
0 ∈ Inj0 X .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is L1 .
Apply (Inj0E X 0 L2 ) to the current goal.
Let x be given.
Apply Inj1NE1 x to the current goal.
Use symmetry.
An
exact proof term for the current goal is
andER (x ∈ X ) (0 = Inj1 x ) H2 .
∎
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Proof: Let X, Y and x be given.
Apply ReplI to the current goal.
An exact proof term for the current goal is H .
∎
Proof: Let X, Y and y be given.
Apply ReplI to the current goal.
An exact proof term for the current goal is H .
∎
Proof: Let X, Y and z be given.
Apply orIL to the current goal.
An
exact proof term for the current goal is
(ReplE X Inj0 z H2 ) .
Apply orIR to the current goal.
An
exact proof term for the current goal is
(ReplE Y Inj1 z H2 ) .
∎
Proof: Let X be given.
Let z be given.
We will
prove z ∈ Inj0 X .
Let x be given.
An
exact proof term for the current goal is
(EmptyE x H3 ) .
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ z = Inj1 x ) H2 ) to the current goal.
Let x be given.
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
(Inj0I X x H3 ) .
Let z be given.
Let x be given.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let x be given.
An
exact proof term for the current goal is
(EmptyE x H2 ) .
rewrite the current goal using H2 (from left to right).
An
exact proof term for the current goal is
(SingI 0 ) .
∎
Proof: Let X be given.
Let z be given.
We will
prove z ∈ Inj1 X .
Let x be given.
rewrite the current goal using H4 (from left to right).
We prove the intermediate
claim L1 :
x = 0 .
rewrite the current goal using L1 (from left to right).
rewrite the current goal using
Inj0_0 (from left to right).
An
exact proof term for the current goal is
(Inj1I1 X ) .
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ z = Inj1 x ) H2 ) to the current goal.
Let x be given.
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
(Inj1I2 X x H3 ) .
Let z be given.
Apply (Inj1E X z H1 ) to the current goal.
rewrite the current goal using H2 (from left to right).
rewrite the current goal using
Inj0_0 (from right to left) at position 1.
An
exact proof term for the current goal is
In_0_1 .
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ z = Inj1 x ) H2 ) to the current goal.
Let x be given.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof:
Let n be given.
Let z be given.
Apply (Inj1E n z H1 ) to the current goal.
rewrite the current goal using H2 (from left to right).
Apply (exandE_i (λm ⇒ m ∈ n ) (λm ⇒ z = Inj1 m ) H2 ) to the current goal.
Let m be given.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using (IHn m H3 ) (from left to right).
Let m be given.
We will
prove m ∈ Inj1 n .
Apply (ordsuccE n m H1 ) to the current goal.
rewrite the current goal using H3 (from left to right).
An
exact proof term for the current goal is
(Inj1I1 n ) .
Let k be given.
rewrite the current goal using H5 (from left to right).
We prove the intermediate
claim L1 :
k ∈ m .
rewrite the current goal using H5 (from left to right).
An
exact proof term for the current goal is
(ordsuccI2 k ) .
We prove the intermediate
claim L2 :
k ∈ n .
An
exact proof term for the current goal is
(nat_trans n Hn m H2 k L1 ) .
rewrite the current goal using (IHn k L2 ) (from right to left).
An
exact proof term for the current goal is
(Inj1I2 n k L2 ) .
rewrite the current goal using H2 (from left to right).
We will
prove n ∈ Inj1 n .
Apply (nat_inv n Hn ) to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An
exact proof term for the current goal is
(Inj1I1 n ) .
Let k be given.
rewrite the current goal using H5 (from left to right) at position 1.
We prove the intermediate
claim L1 :
k ∈ n .
rewrite the current goal using H5 (from left to right).
An
exact proof term for the current goal is
(ordsuccI2 k ) .
rewrite the current goal using (IHn k L1 ) (from right to left).
An
exact proof term for the current goal is
(Inj1I2 n k L1 ) .
Let n be given.
An exact proof term for the current goal is (L n Hn ) .
∎
Proof:
An
exact proof term for the current goal is
Inj0_0 .
∎
Beginning of Section pair_setsum
Proof: Apply (func_ext set set ) to the current goal.
Let x be given.
Use symmetry.
∎
Proof: Apply (func_ext set set ) to the current goal.
Let x be given.
Use symmetry.
∎
Theorem. (
pairI0 )
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Proof:
An
exact proof term for the current goal is
Inj0_setsum .
∎
Theorem. (
pairI1 )
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Proof:
An
exact proof term for the current goal is
Inj1_setsum .
∎
Theorem. (
pairE )
∀X Y z, z ∈ pair X Y → (∃x ∈ X , z = pair 0 x ) ∨ (∃y ∈ Y , z = pair 1 y )
Theorem. (
pairE0 )
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Proof: Let X, Y and x be given.
Apply (pairE X Y (pair 0 x ) H1 ) to the current goal.
Let x' be given.
rewrite the current goal using
(Inj0_inj x x' H4 ) (from left to right).
An exact proof term for the current goal is H3 .
Let y be given.
Assume _ .
An
exact proof term for the current goal is
(Inj0_Inj1_neq x y H3 ) .
∎
Theorem. (
pairE1 )
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Proof: Let X, Y and y be given.
Apply (pairE X Y (pair 1 y ) H1 ) to the current goal.
Let x be given.
Assume _ .
Use symmetry.
An exact proof term for the current goal is H3 .
Let y' be given.
rewrite the current goal using
(Inj1_inj y y' H4 ) (from left to right).
An exact proof term for the current goal is H3 .
∎
Proof:
Let w and u be given.
rewrite the current goal using
(Unj_Inj0_eq u ) (from right to left).
We will
prove Inj0 u ∈ w .
An exact proof term for the current goal is H1 .
We use u to witness the existential quantifier.
Use reflexivity.
∎
Proof: Let w and u be given.
We will
prove Inj0 u ∈ w .
Let z be given.
Apply H3 to the current goal.
Let x be given.
We will
prove Inj0 u ∈ w .
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H5 (from right to left).
rewrite the current goal using
Unj_Inj0_eq (from left to right).
We will
prove Inj0 x ∈ w .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof:
Let w and u be given.
rewrite the current goal using
(Unj_Inj1_eq u ) (from right to left).
We will
prove Inj1 u ∈ w .
An exact proof term for the current goal is H1 .
We use u to witness the existential quantifier.
Use reflexivity.
∎
Proof: Let w and u be given.
We will
prove Inj1 u ∈ w .
Let z be given.
Apply H3 to the current goal.
Let y be given.
We will
prove Inj1 u ∈ w .
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H5 (from right to left).
rewrite the current goal using
Unj_Inj1_eq (from left to right).
We will
prove Inj1 y ∈ w .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let X and Y be given.
We will
prove proj0 (pair X Y ) ⊆ X .
Let u be given.
Apply (pairE0 X Y u ) to the current goal.
We will
prove pair 0 u ∈ pair X Y .
An
exact proof term for the current goal is
(proj0E (pair X Y ) u H1 ) .
We will
prove X ⊆ proj0 (pair X Y ) .
Let u be given.
We will
prove u ∈ proj0 (pair X Y ) .
Apply proj0I to the current goal.
We will
prove pair 0 u ∈ pair X Y .
Apply pairI0 to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let X and Y be given.
We will
prove proj1 (pair X Y ) ⊆ Y .
Let u be given.
Apply (pairE1 X Y u ) to the current goal.
We will
prove pair 1 u ∈ pair X Y .
An
exact proof term for the current goal is
(proj1E (pair X Y ) u H1 ) .
We will
prove Y ⊆ proj1 (pair X Y ) .
Let u be given.
We will
prove u ∈ proj1 (pair X Y ) .
Apply proj1I to the current goal.
We will
prove pair 1 u ∈ pair X Y .
Apply pairI1 to the current goal.
An exact proof term for the current goal is H1 .
∎
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 .
Theorem. (
pair_Sigma )
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x
Proof: Let X, Y and x be given.
Let y be given.
We will
prove pair x y ∈ ⋃ x ∈ X { pair x y | y ∈ Y x } .
Apply (famunionI X (λx ⇒ { pair x y | y ∈ Y x } ) x (pair x y ) ) to the current goal.
An exact proof term for the current goal is Hx .
We will
prove pair x y ∈ { pair x y | y ∈ Y x } .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hy .
∎
Proof: Let X, Y and z be given.
We prove the intermediate
claim L1 :
∃x ∈ X , z ∈ { pair x y | y ∈ Y x } .
An
exact proof term for the current goal is
(famunionE X (λx ⇒ { pair x y | y ∈ Y x } ) z H1 ) .
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ z ∈ { pair x y | y ∈ Y x } ) L1 ) to the current goal.
Let x be given.
Apply (ReplE_impred (Y x ) (pair x ) z H3 ) to the current goal.
Let y be given.
rewrite the current goal using H5 (from left to right).
rewrite the current goal using
proj0_pair_eq (from left to right).
We will
prove pair x (proj1 (pair x y ) ) = pair x y ∧ x ∈ X ∧ proj1 (pair x y ) ∈ Y x .
rewrite the current goal using
proj1_pair_eq (from left to right).
We will
prove pair x y = pair x y ∧ x ∈ X ∧ y ∈ Y x .
Apply and3I to the current goal.
We will
prove pair x y = pair x y .
Use reflexivity.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H4 .
∎
Proof: Let X, Y and z be given.
Assume H2 _ _ .
An exact proof term for the current goal is H2 .
∎
Proof: Let X, Y and z be given.
Assume _ H2 _ .
An exact proof term for the current goal is H2 .
∎
Proof: Let X, Y and z be given.
Assume _ _ H2 .
An exact proof term for the current goal is H2 .
∎
Theorem. (
pair_Sigma_E1 )
∀X : set , ∀Y : set → set , ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x ) → y ∈ Y x
Proof: Let X, Y, x and y be given.
rewrite the current goal using
(proj0_pair_eq x y ) (from right to left).
We will
prove y ∈ Y (proj0 (pair x y ) ) .
rewrite the current goal using
(proj1_pair_eq x y ) (from right to left) at position 1.
An
exact proof term for the current goal is
(proj1_Sigma X Y (pair x y ) H1 ) .
∎
Theorem. (
Sigma_E )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → ∃x ∈ X , ∃y ∈ Y x , z = pair x y
Proof: Let X, Y and z be given.
We use
(proj0 z ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2 .
We use
(proj1 z ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
Use symmetry.
An exact proof term for the current goal is H1 .
∎
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 ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
Theorem. (
lamI )
∀X : set , ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x
Proof: An
exact proof term for the current goal is
pair_Sigma .
∎
Theorem. (
lamE )
∀X : set , ∀F : set → set , ∀z : set , z ∈ (λ x ∈ X ⇒ F x ) → ∃x ∈ X , ∃y ∈ F x , z = pair x y
Proof: An
exact proof term for the current goal is
Sigma_E .
∎
Theorem. (
apI )
∀f x y, pair x y ∈ f → y ∈ f x
Proof: Let f, x and y be given.
rewrite the current goal using
(proj1_pair_eq x y ) (from right to left).
Apply (ReplSepI f (λz ⇒ ∃y : set , z = pair x y ) proj1 (pair x y ) H1 ) to the current goal.
We will
prove ∃y' : set , pair x y = pair x y' .
We use y to witness the existential quantifier.
Use reflexivity.
∎
Theorem. (
apE )
∀f x y, y ∈ f x → pair x y ∈ f
Proof: Let f, x and y be given.
We will
prove pair x y ∈ f .
Let z be given.
Apply H1 to the current goal.
Let v be given.
We prove the intermediate
claim L1 :
y = v .
rewrite the current goal using H2 (from left to right).
rewrite the current goal using H3 (from left to right).
We will
prove proj1 (pair x v ) = v .
We prove the intermediate
claim L2 :
z = pair x y .
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H3 .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hz .
∎
Theorem. (
beta )
∀X : set , ∀F : set → set , ∀x : set , x ∈ X → (λ x ∈ X ⇒ F x ) x = F x
Proof: Let X, F and x be given.
Let w be given.
We prove the intermediate
claim L1 :
pair x w ∈ (λ x ∈ X ⇒ F x ) .
An
exact proof term for the current goal is
(apE (λ x ∈ X ⇒ F x ) x w Hw ) .
An
exact proof term for the current goal is
(pair_Sigma_E1 X F x w L1 ) .
Let w be given.
We will
prove w ∈ (λ x ∈ X ⇒ F x ) x .
Apply apI to the current goal.
We will
prove pair x w ∈ λ x ∈ X ⇒ F x .
We will
prove pair x w ∈ ∑ x ∈ X , F x .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hw .
∎
Proof: Let u be given.
Let w be given.
Apply apI to the current goal.
We will
prove pair 0 w ∈ u .
Apply proj0E to the current goal.
An exact proof term for the current goal is H1 .
Let w be given.
Apply proj0I to the current goal.
We will
prove pair 0 w ∈ u .
Apply apE to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let u be given.
Let w be given.
Apply apI to the current goal.
We will
prove pair 1 w ∈ u .
Apply proj1E to the current goal.
An exact proof term for the current goal is H1 .
Let w be given.
Apply proj1I to the current goal.
We will
prove pair 1 w ∈ u .
Apply apE to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let x and y be given.
rewrite the current goal using
(proj0_ap_0 (pair x y ) ) (from right to left).
We will
prove proj0 (pair x y ) = x .
∎
Proof: Let x and y be given.
rewrite the current goal using
(proj1_ap_1 (pair x y ) ) (from right to left).
We will
prove proj1 (pair x y ) = y .
∎
Theorem. (
ap0_Sigma )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → (z 0 ) ∈ X
Proof: Let X, Y and z be given.
rewrite the current goal using
proj0_ap_0 (from right to left).
∎
Theorem. (
ap1_Sigma )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → (z 1 ) ∈ (Y (z 0 ) )
Proof: Let X, Y and z be given.
rewrite the current goal using
proj0_ap_0 (from right to left).
rewrite the current goal using
proj1_ap_1 (from right to left).
∎
Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 ) (u 1 ) = u of type
set → prop .
Proof: Let x and y be given.
We will
prove pair (pair x y 0 ) (pair x y 1 ) = pair x y .
rewrite the current goal using
pair_ap_0 (from left to right).
rewrite the current goal using
pair_ap_1 (from left to right).
Use reflexivity.
∎
Proof: Let x be given.
We prove the intermediate
claim L1 :
x = 0 .
rewrite the current goal using L1 (from left to right).
An
exact proof term for the current goal is
(UPairI1 0 1 ) .
rewrite the current goal using H2 (from left to right).
An
exact proof term for the current goal is
(UPairI2 0 1 ) .
∎
Proof: Let x and y be given.
Let z be given.
Apply (pairE x y z Hz ) to the current goal.
Apply (exandE_i (λu ⇒ u ∈ x ) (λu ⇒ z = pair 0 u ) H1 ) to the current goal.
Let u be given.
rewrite the current goal using H2 (from left to right).
rewrite the current goal using
(If_i_1 (0 = 0 ) x y (λq H ⇒ H ) ) (from left to right).
An exact proof term for the current goal is Hu .
Apply (exandE_i (λu ⇒ u ∈ y ) (λu ⇒ z = pair 1 u ) H1 ) to the current goal.
Let u be given.
rewrite the current goal using H2 (from left to right).
rewrite the current goal using
(If_i_0 (1 = 0 ) x y neq_1_0 ) (from left to right).
An exact proof term for the current goal is Hu .
Let z be given.
We will
prove z ∈ pair x y .
We prove the intermediate
claim L1 :
∃i ∈ 2 , ∃w ∈ (if i = 0 then x else y ) , z = pair i w .
An
exact proof term for the current goal is
(lamE 2 (λi ⇒ if i = 0 then x else y ) z Hz ) .
Let i be given.
Let w be given.
We will
prove z ∈ pair x y .
rewrite the current goal using H2 (from left to right).
We will
prove pair i w ∈ pair x y .
We prove the intermediate
claim L2 :
i ∈ { 0 , 1 } .
Apply (UPairE i 0 1 L2 ) to the current goal.
rewrite the current goal using Hi0 (from left to right).
We will
prove pair 0 w ∈ pair x y .
Apply pairI0 to the current goal.
We prove the intermediate
claim L3 :
(if i = 0 then x else y ) = x .
An
exact proof term for the current goal is
(If_i_1 (i = 0 ) x y Hi0 ) .
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw .
rewrite the current goal using Hi1 (from left to right).
We will
prove pair 1 w ∈ pair x y .
Apply pairI1 to the current goal.
We prove the intermediate
claim L3 :
(if i = 0 then x else y ) = y .
rewrite the current goal using Hi1 (from left to right).
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw .
∎
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 .
Theorem. (
PiI )
∀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
Proof: Let X, Y and f be given.
We will
prove f ∈ { f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x ) ) | ∀x ∈ X , f x ∈ Y x } .
Apply SepI to the current goal.
We will
prove f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x ) ) .
Apply PowerI to the current goal.
We will
prove f ⊆ ∑ x ∈ X , ⋃ (Y x ) .
Let z be given.
We will
prove z ∈ ∑ x ∈ X , ⋃ (Y x ) .
Apply (H1 z Hz ) to the current goal.
rewrite the current goal using H3 (from right to left).
We will
prove pair (z 0 ) (z 1 ) ∈ ∑ x ∈ X , ⋃ (Y x ) .
An exact proof term for the current goal is H4 .
We will
prove z 1 ∈ ⋃ (Y (z 0 ) ) .
Apply (UnionI (Y (z 0 ) ) (z 1 ) (f (z 0 ) ) ) to the current goal.
We will
prove z 1 ∈ f (z 0 ) .
Apply apI to the current goal.
We will
prove pair (z 0 ) (z 1 ) ∈ f .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hz .
We will
prove f (z 0 ) ∈ Y (z 0 ) .
An
exact proof term for the current goal is
(H2 (z 0 ) H4 ) .
We will
prove ∀x ∈ X , f x ∈ Y x .
An exact proof term for the current goal is H2 .
∎
Theorem. (
lam_Pi )
∀X : set , ∀Y : set → set , ∀F : set → set , (∀x ∈ X , F x ∈ Y x ) → (λ x ∈ X ⇒ F x ) ∈ (∏ x ∈ X , Y x )
Proof: Let X, Y and F be given.
We will
prove (λ x ∈ X ⇒ F x ) ∈ (∏ x ∈ X , Y x ) .
Apply PiI to the current goal.
Let u be given.
We prove the intermediate
claim L1 :
∃x ∈ X , ∃y ∈ F x , u = pair x y .
An
exact proof term for the current goal is
(lamE X F u Hu ) .
Apply (exandE_i (λx ⇒ x ∈ X ) (λx ⇒ ∃y ∈ F x , u = pair x y ) L1 ) to the current goal.
Let x be given.
Apply (exandE_i (λy ⇒ y ∈ F x ) (λy ⇒ u = pair x y ) H2 ) to the current goal.
Let y be given.
Apply andI to the current goal.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using H3 (from left to right).
We will
prove pair x y 0 ∈ X .
rewrite the current goal using
pair_ap_0 (from left to right).
An exact proof term for the current goal is Hx .
We will
prove ∀x ∈ X , (λ x ∈ X ⇒ F x ) x ∈ Y x .
Let x be given.
rewrite the current goal using
(beta X F x Hx ) (from left to right).
An exact proof term for the current goal is (H1 x Hx ) .
∎
Theorem. (
ap_Pi )
∀X : set , ∀Y : set → set , ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x ) → x ∈ X → f x ∈ Y x
Proof: Let X, Y, f and x be given.
An
exact proof term for the current goal is
(SepE2 (𝒫 (∑ x ∈ X , ⋃ (Y x ) ) ) (λf ⇒ ∀x ∈ X , f x ∈ Y x ) f Hf 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 .
Proof: Apply func_ext set (set → set ) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
We will
prove pair x y = ( x ,y ) .
∎
Theorem. (
lamI2 )
∀X, ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , ( x ,y ) ∈ λ x ∈ X ⇒ F x
Proof: We will
prove (∀X, ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , ((λx y : set ⇒ ( x ,y ) ) x y ) ∈ λ x ∈ X ⇒ F x ) .
An
exact proof term for the current goal is
lamI .
∎
Beginning of Section Tuples
Variable x0 x1 : set
Proof:
Apply If_i_1 to the current goal.
Use reflexivity.
∎
Proof:
Apply If_i_0 to the current goal.
∎
End of Section Tuples
Proof: Let X, Y, F and G be given.
Apply ReplEq_ext (X ⨯ Y ) (λw ⇒ F (w 0 ) (w 1 ) ) (λw ⇒ G (w 0 ) (w 1 ) ) to the current goal.
We will
prove ∀w ∈ X ⨯ Y , F (w 0 ) (w 1 ) = G (w 0 ) (w 1 ) .
Let w be given.
Apply H1 to the current goal.
An
exact proof term for the current goal is
ap0_Sigma X (λ_ ⇒ Y ) w Hw .
An
exact proof term for the current goal is
ap1_Sigma X (λ_ ⇒ Y ) w Hw .
∎
Proof: An
exact proof term for the current goal is
lamI2 .
∎
Proof: An
exact proof term for the current goal is
λX Y x Hx y Hy ⇒ tuple_2_Sigma X (λ_ ⇒ Y ) x Hx y Hy .
∎
End of Section pair_setsum