Primitive. The name Eps_i is a term of type (setprop)set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
Definition. We define True to be ∀p : prop, pp of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : propAFalse of type propprop.
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, (ABp)p of type proppropprop.
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, (Ap)(Bp)p of type proppropprop.
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 : propand (AB) (BA) of type proppropprop.
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 : AAprop, Q x yQ y x of type AAprop.
Definition. We define neq to be λx y : A¬ eq x y of type AAprop.
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 : AB, (∀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 : Aprop∀P : prop, (∀x : A, Q xP)P of type (Aprop)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 qp = q
Primitive. The name In is a term of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write xA, B to mean x : set, xAB.
Definition. We define Subq to be λA B ⇒ ∀xA, x B of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write xA, B to mean x : set, xAB.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (∀xX, 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:
¬ ∃x : set, x Empty
Primitive. The name is a term of type setset.
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 setset.
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(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA} ∃xA, y = F x
Definition. We define TransSet to be λU : set∀xU, x U of type setprop.
Definition. We define Union_closed to be λU : set∀X : set, X U X U of type setprop.
Definition. We define Power_closed to be λU : set∀X : set, X U𝒫 X U of type setprop.
Definition. We define Repl_closed to be λU : set∀X : set, X U∀F : setset, (∀x : set, x XF x U){F x|xX} U of type setprop.
Definition. We define ZF_closed to be λU : setUnion_closed U Power_closed U Repl_closed U of type setprop.
Primitive. The name UnivOf is a term of type setset.
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N UnivOf N
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N UTransSet UZF_closed UUnivOf N U
Theorem. (FalseE)
False∀p : prop, p
Proof:
An exact proof term for the current goal is (λH ⇒ H).
Theorem. (TrueI)
Proof:
An exact proof term for the current goal is (λp H ⇒ H).
Theorem. (andI)
∀A B : prop, ABA B
Proof:
An exact proof term for the current goal is (λA B a b P H ⇒ H a b).
Theorem. (andEL)
∀A B : prop, A BA
Proof:
An exact proof term for the current goal is (λA B H ⇒ H A (λa b ⇒ a)).
Theorem. (andER)
∀A B : prop, A BB
Proof:
An exact proof term for the current goal is (λA B H ⇒ H B (λa b ⇒ b)).
Theorem. (orIL)
∀A B : prop, AA B
Proof:
An exact proof term for the current goal is (λA B a P H1 H2 ⇒ H1 a).
Theorem. (orIR)
∀A B : prop, BA B
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)
P1P2P3P1 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, (P1P2P3p)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))).
Theorem. (or3I1)
P1P1 P2 P3
Proof:
An exact proof term for the current goal is (λu ⇒ orIL (P1 P2) P3 (orIL P1 P2 u)).
Theorem. (or3I2)
P2P1 P2 P3
Proof:
An exact proof term for the current goal is (λu ⇒ orIL (P1 P2) P3 (orIR P1 P2 u)).
Theorem. (or3I3)
P3P1 P2 P3
Proof:
An exact proof term for the current goal is (orIR (P1 P2) P3).
Theorem. (or3E)
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)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)
P1P2P3P4P1 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)
P1P2P3P4P5P1 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
Theorem. (not_or_and_demorgan)
∀A B : prop, ¬ (A B)¬ A ¬ B
Proof:
Let A and B be given.
Assume u: ¬ (A B).
Apply andI to the current goal.
We will prove ¬ A.
Assume a: A.
An exact proof term for the current goal is (u (orIL A B a)).
We will prove ¬ B.
Assume b: B.
An exact proof term for the current goal is (u (orIR A B b)).
Theorem. (not_ex_all_demorgan_i)
∀P : setprop, (¬ ∃x, P x)∀x, ¬ P x
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, (AB)(BA)(A B)
Proof:
An exact proof term for the current goal is (λA B ⇒ andI (AB) (BA)).
Theorem. (iffEL)
∀A B : prop, (A B)AB
Proof:
An exact proof term for the current goal is (λA B ⇒ andEL (AB) (BA)).
Theorem. (iffER)
∀A B : prop, (A B)BA
Proof:
An exact proof term for the current goal is (λA B ⇒ andER (AB) (BA)).
Theorem. (iff_refl)
∀A : prop, A A
Proof:
An exact proof term for the current goal is (λA : propandI (AA) (AA) (λH : AH) (λH : AH)).
Theorem. (iff_sym)
∀A B : prop, (A B)(B A)
Proof:
Let A and B be given.
Assume H1: (AB) (BA).
Apply H1 to the current goal.
Assume H2: AB.
Assume H3: BA.
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.
Assume H1: A B.
Assume H2: B C.
Apply H1 to the current goal.
Assume H3: AB.
Assume H4: BA.
Apply H2 to the current goal.
Assume H5: BC.
Assume H6: CB.
An exact proof term for the current goal is (iffI A C (λH ⇒ H5 (H3 H)) (λH ⇒ H4 (H6 H))).
Theorem. (eq_i_tra)
∀x y z, x = yy = zx = z
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 : setset, ∀x y, x = yf 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.
Theorem. (neq_i_sym)
∀x y, x yy x
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 setsetprop.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Theorem. (Eps_i_ex)
∀P : setprop, (∃x, P x)P (Eps_i P)
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 : setprop, (∀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.
Apply prop_ext to the current goal.
We will prove P x Q x.
An exact proof term for the current goal is H1 x.
Theorem. (prop_ext_2)
∀p q : prop, (pq)(qp)p = q
Proof:
Let p and q be given.
Assume H1 H2.
Apply prop_ext to the current goal.
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.
Theorem. (Subq_ref)
∀X : set, X X
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 YY ZX 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))).
Theorem. (Subq_contra)
∀X Y z : set, X Yz Yz X
Proof:
An exact proof term for the current goal is (λX Y z H1 H2 H3 ⇒ H2 (H1 z H3)).
Theorem. (EmptyE)
∀x : set, x Empty
Proof:
Let x be given.
Assume H.
Apply EmptyAx to the current goal.
We use x to witness the existential quantifier.
An exact proof term for the current goal is H.
Theorem. (Subq_Empty)
∀X : set, Empty X
Proof:
An exact proof term for the current goal is (λ(X x : set)(H : x Empty) ⇒ EmptyE x H (x X)).
Theorem. (Empty_Subq_eq)
∀X : set, X EmptyX = Empty
Proof:
Let X be given.
Assume H1: X Empty.
Apply set_ext to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is (Subq_Empty X).
Theorem. (Empty_eq)
∀X : set, (∀x, x X)X = Empty
Proof:
Let X be given.
Assume H1: ∀x, x X.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume H2: x X.
We will prove False.
An exact proof term for the current goal is (H1 x H2).
Theorem. (UnionI)
∀X x Y : set, x YY Xx X
Proof:
Let X, x and Y be given.
Assume H1: x Y.
Assume H2: Y X.
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 : setiffEL (x X) (∃Y : set, x Y Y X) (UnionEq X x)).
Theorem. (UnionE_impred)
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)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 XY 𝒫 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 𝒫 XY 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. (Empty_In_Power)
∀X : set, Empty 𝒫 X
Proof:
An exact proof term for the current goal is (λX : setPowerI X Empty (Subq_Empty X)).
Theorem. (Self_In_Power)
∀X : set, X 𝒫 X
Proof:
An exact proof term for the current goal is (λX : setPowerI X X (Subq_ref X)).
Theorem. (xm)
∀P : prop, P ¬ P
Proof:
Let P of type prop be given.
Set p1 to be the term λx : setx = Empty P.
Set p2 to be the term λx : setx Empty P.
We prove the intermediate claim L1: p1 Empty.
We will prove (Empty = Empty P).
Apply orIL to the current goal.
An exact proof term for the current goal is (λq H ⇒ H).
We prove the intermediate claim L2: (Eps_i p1) = Empty P.
An exact proof term for the current goal is (Eps_i_ax p1 Empty L1).
We prove the intermediate claim L3: p2 (𝒫 Empty).
We will prove ¬ (𝒫 Empty = Empty) P.
Apply orIL to the current goal.
Assume H1: 𝒫 Empty = Empty.
Apply EmptyE Empty to the current goal.
We will prove Empty Empty.
rewrite the current goal using H1 (from right to left) at position 2.
Apply Empty_In_Power to the current goal.
We prove the intermediate claim L4: Eps_i p2 Empty P.
An exact proof term for the current goal is (Eps_i_ax p2 (𝒫 Empty) L3).
Apply L2 to the current goal.
Assume H1: Eps_i p1 = Empty.
Apply L4 to the current goal.
Assume H2: Eps_i p2 Empty.
We will prove P ¬ P.
Apply orIR to the current goal.
We will prove ¬ P.
Assume H3: P.
We prove the intermediate claim L5: p1 = p2.
Apply pred_ext to the current goal.
Let x be given.
Apply iffI to the current goal.
Assume H4.
We will prove (¬ (x = Empty) P).
Apply orIR to the current goal.
We will prove P.
An exact proof term for the current goal is H3.
Assume H4.
We will prove (x = Empty P).
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.
We will prove P ¬ P.
Apply orIL to the current goal.
We will prove P.
An exact proof term for the current goal is H2.
Assume H1: P.
We will prove P ¬ P.
Apply orIL to the current goal.
We will prove P.
An exact proof term for the current goal is H1.
Theorem. (dneg)
∀P : prop, ¬ ¬ PP
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).
Assume H2: ¬ P.
We will prove False.
An exact proof term for the current goal is H1 H2.
Theorem. (not_all_ex_demorgan_i)
∀P : setprop, ¬ (∀x, P x)∃x, ¬ P x
Proof:
Let P be given.
Assume u: ¬ ∀x, P x.
Apply dneg to the current goal.
Assume v: ¬ ∃x, ¬ P x.
Apply u to the current goal.
Let x be given.
Apply dneg to the current goal.
Assume w: ¬ P x.
An exact proof term for the current goal is (not_ex_all_demorgan_i (λx ⇒ ¬ P x) v x w).
Theorem. (eq_or_nand)
or = (λx y : prop¬ (¬ x ¬ y))
Proof:
Apply func_ext prop (propprop) to the current goal.
Let x be given.
Apply func_ext prop prop to the current goal.
Let y be given.
Apply prop_ext_2 to the current goal.
Assume H1: x y.
Assume H2: ¬ x ¬ y.
Apply H2 to the current goal.
Assume H3 H4.
An exact proof term for the current goal is (H1 False H3 H4).
Assume H1: ¬ (¬ x ¬ y).
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.
Assume H2: ¬ x.
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.
Assume H3: ¬ y.
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 : propA ¬ B ¬ A B of type proppropprop.
Theorem. (exactly1of2_I1)
∀A B : prop, A¬ Bexactly1of2 A B
Proof:
Let A and B be given.
Assume HA: A.
Assume HB: ¬ B.
We will prove A ¬ B ¬ A B.
Apply orIL to the current goal.
We will prove A ¬ B.
An exact proof term for the current goal is (andI A (¬ B) HA HB).
Theorem. (exactly1of2_I2)
∀A B : prop, ¬ ABexactly1of2 A B
Proof:
Let A and B be given.
Assume HA: ¬ A.
Assume HB: B.
We will prove A ¬ B ¬ A B.
Apply orIR to the current goal.
We will prove ¬ A B.
An exact proof term for the current goal is (andI (¬ A) B HA HB).
Theorem. (exactly1of2_E)
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
Proof:
Let A and B be given.
Assume H1: exactly1of2 A B.
Let p be given.
Assume H2: A¬ Bp.
Assume H3: ¬ ABp.
Apply (H1 p) to the current goal.
An exact proof term for the current goal is (λH4 : A ¬ BH4 p H2).
An exact proof term for the current goal is (λH4 : ¬ A BH4 p H3).
Theorem. (exactly1of2_or)
∀A B : prop, exactly1of2 A BA B
Proof:
Let A and B be given.
Assume H1: exactly1of2 A B.
Apply (exactly1of2_E A B H1 (A B)) to the current goal.
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 : setset, ∀x : set, x AF x {F x|xA}
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 : setset, ∀y : set, y {F x|xA}∃xA, 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 : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)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 : setset, ∀p : setprop, (∀xX, p (f x))∀y{f x|xX}, p y
Proof:
Let X, f and p be given.
Assume H1.
Let y be given.
Assume Hy.
Apply ReplE_impred X f y Hy to the current goal.
Let x be given.
Assume Hx: x X.
Assume Hx2: y = f x.
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.
Theorem. (Repl_Empty)
∀F : setset, {F x|xEmpty} = Empty
Proof:
Let F be given.
Apply (Empty_eq {F x|xEmpty}) to the current goal.
Let y be given.
Assume H1: y {F x|xEmpty}.
Apply (ReplE_impred Empty F y H1) to the current goal.
Let x be given.
Assume H2: x Empty.
Assume _.
An exact proof term for the current goal is (EmptyE x H2).
Theorem. (ReplEq_ext_sub)
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} {G x|xX}
Proof:
Let X, F and G be given.
Assume H1: ∀xX, F x = G x.
Let y be given.
Assume Hy: y {F x|xX}.
Apply ReplE_impred X F y Hy to the current goal.
Let x be given.
Assume Hx: x X.
Assume H2: y = F x.
We will prove y {G x|xX}.
rewrite the current goal using H2 (from left to right).
We will prove F x {G x|xX}.
rewrite the current goal using H1 x Hx (from left to right).
We will prove G x {G x|xX}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Theorem. (ReplEq_ext)
∀X, ∀F G : setset, (∀xX, F x = G x){F x|xX} = {G x|xX}
Proof:
Let X, F and G be given.
Assume H1: ∀xX, F x = G x.
Apply set_ext to the current goal.
An exact proof term for the current goal is ReplEq_ext_sub X F G H1.
Apply ReplEq_ext_sub X G F to the current goal.
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 : setprop, ∀f g : setset, (∀x, P xg (f x) = x)∀X, (∀xX, P x){g y|y{f x|xX}} = X
Proof:
Let P, f and g be given.
Assume H1.
Let X be given.
Assume HX.
Apply set_ext to the current goal.
Let w be given.
Assume Hw: w {g y|y{f x|xX}}.
Apply ReplE_impred {f x|xX} g w Hw to the current goal.
Let y be given.
Assume Hy: y {f x|xX}.
Assume Hwy: w = g y.
Apply ReplE_impred X f y Hy to the current goal.
Let x be given.
Assume Hx: x X.
Assume Hyx: y = f x.
We will prove w X.
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.
Assume Hx: x X.
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|xX}}.
Apply ReplI to the current goal.
We will prove f x {f x|xX}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Theorem. (Repl_invol_eq)
∀P : setprop, ∀f : setset, (∀x, P xf (f x) = x)∀X, (∀xX, P x){f y|y{f x|xX}} = 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 : setp z = x ¬ p z = y)) of type propsetsetset.
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.
Theorem. (If_i_correct)
∀p : prop, ∀x y : set, p (if p then x else y) = x ¬ p (if p then x else y) = y
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.
Use reflexivity.
An exact proof term for the current goal is (Eps_i_ax (λz : setp z = x ¬ p z = y) x L1).
Assume H1: ¬ p.
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.
Use reflexivity.
An exact proof term for the current goal is (Eps_i_ax (λz : setp z = x ¬ p z = y) y L1).
Theorem. (If_i_0)
∀p : prop, ∀x y : set, ¬ p(if p then x else y) = y
Proof:
Let p, x and y be given.
Assume H1: ¬ p.
Apply (If_i_correct p x y) to the current goal.
Assume H2: p (if p then x else y) = x.
An exact proof term for the current goal is (H1 (andEL p ((if p then x else y) = x) H2) ((if p then x else y) = y)).
Assume H2: ¬ p (if p then x else y) = y.
An exact proof term for the current goal is (andER (¬ p) ((if p then x else y) = y) H2).
Theorem. (If_i_1)
∀p : prop, ∀x y : set, p(if p then x else y) = x
Proof:
Let p, x and y be given.
Assume H1: p.
Apply (If_i_correct p x y) to the current goal.
Assume H2: p (if p then x else y) = x.
An exact proof term for the current goal is (andER p ((if p then x else y) = x) H2).
Assume H2: ¬ p (if p then x else y) = y.
An exact proof term for the current goal is (andEL (¬ p) ((if p then x else y) = y) H2 H1 ((if p then x else y) = x)).
Theorem. (If_i_or)
∀p : prop, ∀x y : set, (if p then x else y) = x (if p then x else y) = y
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).
Assume H1: ¬ p.
Apply orIR to the current goal.
An exact proof term for the current goal is (If_i_0 p x y H1).
Definition. We define UPair to be λy z ⇒ {if Empty X then y else z|X𝒫 (𝒫 Empty)} of type setsetset.
Notation. {x,y} is notation for UPair x y.
Theorem. (UPairE)
∀x y z : set, x {y,z}x = y x = z
Proof:
Let x, y and z be given.
Assume H1: x {y,z}.
Apply (ReplE (𝒫 (𝒫 Empty)) (λX ⇒ if Empty X then y else z) x H1) to the current goal.
Let X be given.
Assume H2: X 𝒫 (𝒫 Empty) x = if Empty X then y else z.
We prove the intermediate claim L1: x = if Empty X then y else z.
An exact proof term for the current goal is (andER (X 𝒫 (𝒫 Empty)) (x = if Empty X then y else z) H2).
Apply (If_i_or (Empty X) y z) to the current goal.
Assume H3: (if Empty X then y else z) = y.
Apply orIL to the current goal.
We will prove x = y.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1.
Assume H3: (if Empty X then y else z) = z.
Apply orIR to the current goal.
We will prove x = z.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L1.
Theorem. (UPairI1)
∀y z : set, y {y,z}
Proof:
Let y and z be given.
We will prove y {y,z}.
rewrite the current goal using (If_i_1 (Empty 𝒫 Empty) y z (Empty_In_Power Empty)) (from right to left) at position 1.
We will prove (if Empty 𝒫 Empty then y else z) {y,z}.
Apply (ReplI (𝒫 (𝒫 Empty)) (λX : setif (Empty X) then y else z) (𝒫 Empty)) to the current goal.
We will prove 𝒫 Empty 𝒫 (𝒫 Empty).
An exact proof term for the current goal is (Self_In_Power (𝒫 Empty)).
Theorem. (UPairI2)
∀y z : set, z {y,z}
Proof:
Let y and z be given.
We will prove z {y,z}.
rewrite the current goal using (If_i_0 (Empty Empty) y z (EmptyE Empty)) (from right to left) at position 1.
We will prove (if Empty Empty then y else z) {y,z}.
Apply (ReplI (𝒫 (𝒫 Empty)) (λX : setif (Empty X) then y else z) Empty) to the current goal.
We will prove Empty 𝒫 (𝒫 Empty).
An exact proof term for the current goal is (Empty_In_Power (𝒫 Empty)).
Definition. We define Sing to be λx ⇒ {x,x} of type setset.
Notation. {x} is notation for Sing x.
Theorem. (SingI)
∀x : set, x {x}
Proof:
An exact proof term for the current goal is (λx : setUPairI1 x x).
Theorem. (SingE)
∀x y : set, y {x}y = 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)).
Theorem. (Sing_inj)
∀x y, {x} = {y}x = y
Proof:
Let x and y be given.
Assume H1: {x} = {y}.
Apply SingE to the current goal.
We will prove x {y}.
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 setsetset.
Notation. We use as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Theorem. (binunionI1)
∀X Y z : set, z Xz X Y
Proof:
Let X, Y and z be given.
Assume H1: z X.
We will prove z X Y.
We will prove z {X,Y}.
Apply (UnionI {X,Y} z X) to the current goal.
We will prove z X.
An exact proof term for the current goal is H1.
We will prove X {X,Y}.
An exact proof term for the current goal is (UPairI1 X Y).
Theorem. (binunionI2)
∀X Y z : set, z Yz X Y
Proof:
Let X, Y and z be given.
Assume H1: z Y.
We will prove z X Y.
We will prove z {X,Y}.
Apply (UnionI {X,Y} z Y) to the current goal.
We will prove z Y.
An exact proof term for the current goal is H1.
We will prove Y {X,Y}.
An exact proof term for the current goal is (UPairI2 X Y).
Theorem. (binunionE)
∀X Y z : set, z X Yz X z Y
Proof:
Let X, Y and z be given.
Assume H1: z X Y.
We will prove z X z Y.
Apply (UnionE_impred {X,Y} z H1) to the current goal.
Let Z be given.
Assume H2: z Z.
Assume H3: Z {X,Y}.
Apply (UPairE Z X Y H3) to the current goal.
Assume H4: Z = X.
Apply orIL to the current goal.
We will prove z X.
rewrite the current goal using H4 (from right to left).
We will prove z Z.
An exact proof term for the current goal is H2.
Assume H4: Z = Y.
Apply orIR to the current goal.
We will prove z Y.
rewrite the current goal using H4 (from right to left).
We will prove z Z.
An exact proof term for the current goal is H2.
Theorem. (binunionE')
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
Proof:
Let X, Y, z and p be given.
Assume H1 H2 Hz.
Apply binunionE X Y z Hz to the current goal.
Assume H3: z X.
An exact proof term for the current goal is H1 H3.
Assume H3: z Y.
An exact proof term for the current goal is H2 H3.
Theorem. (binunion_asso)
∀X Y Z : set, X (Y Z) = (X Y) Z
Proof:
Let X, Y and Z be given.
Apply set_ext to the current goal.
Let w be given.
Assume H1: w X (Y Z).
We will prove w (X Y) Z.
Apply (binunionE X (Y Z) w H1) to the current goal.
Assume H2: w X.
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: w Y Z.
Apply (binunionE Y Z w H2) to the current goal.
Assume H3: w Y.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H3.
Assume H3: w Z.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H3.
Let w be given.
Assume H1: w (X Y) Z.
We will prove w X (Y Z).
Apply (binunionE (X Y) Z w H1) to the current goal.
Assume H2: w X Y.
Apply (binunionE X Y w H2) to the current goal.
Assume H3: w X.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is H3.
Assume H3: w Y.
Apply binunionI2 to the current goal.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is H3.
Assume H2: w Z.
Apply binunionI2 to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H2.
Theorem. (binunion_com_Subq)
∀X Y : set, X Y Y X
Proof:
Let X, Y and w be given.
Assume H1: w X Y.
We will prove w Y X.
Apply (binunionE X Y w H1) to the current goal.
Assume H2: w X.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: w Y.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is H2.
Theorem. (binunion_com)
∀X Y : set, X Y = Y X
Proof:
Let X and Y be given.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binunion_com_Subq X Y).
An exact proof term for the current goal is (binunion_com_Subq Y X).
Theorem. (binunion_idl)
∀X : set, Empty X = X
Proof:
Let X be given.
Apply set_ext to the current goal.
Let x be given.
Assume H1: x Empty X.
Apply (binunionE Empty X x H1) to the current goal.
Assume H2: x Empty.
We will prove False.
An exact proof term for the current goal is (EmptyE x H2).
Assume H2: x X.
An exact proof term for the current goal is H2.
Let x be given.
Assume H2: x X.
We will prove x Empty X.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H2.
Theorem. (binunion_idr)
∀X : set, X Empty = X
Proof:
Let X be given.
rewrite the current goal using (binunion_com X Empty) (from left to right).
An exact proof term for the current goal is (binunion_idl X).
Theorem. (binunion_Subq_1)
∀X Y : set, X X Y
Proof:
An exact proof term for the current goal is binunionI1.
Theorem. (binunion_Subq_2)
∀X Y : set, Y X Y
Proof:
An exact proof term for the current goal is binunionI2.
Theorem. (binunion_Subq_min)
∀X Y Z : set, X ZY ZX Y Z
Proof:
Let X, Y and Z be given.
Assume H1: X Z.
Assume H2: Y Z.
Let w be given.
Assume H3: w X Y.
Apply (binunionE X Y w H3) to the current goal.
Assume H4: w X.
An exact proof term for the current goal is (H1 w H4).
Assume H4: w Y.
An exact proof term for the current goal is (H2 w H4).
Theorem. (Subq_binunion_eq)
∀X Y, (X Y) = (X Y = Y)
Proof:
Let X and Y be given.
Apply prop_ext_2 to the current goal.
Assume H1: X Y.
We will prove X Y = Y.
Apply set_ext to the current goal.
We will prove X Y Y.
Apply (binunion_Subq_min X Y Y) to the current goal.
We will prove X Y.
An exact proof term for the current goal is H1.
We will prove Y Y.
An exact proof term for the current goal is (Subq_ref Y).
We will prove Y X Y.
An exact proof term for the current goal is (binunion_Subq_2 X Y).
Assume H1: X Y = Y.
We will prove X Y.
rewrite the current goal using H1 (from right to left).
We will prove X X Y.
An exact proof term for the current goal is (binunion_Subq_1 X Y).
Definition. We define SetAdjoin to be λX y ⇒ X {y} of type setsetset.
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|xX} of type set(setset)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 : (setset), ∀x y : set, x Xy F xy xXF 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 : (setset), ∀y : set, y (xXF x)∃xX, y F x
Proof:
Let X, F and y be given.
Assume H1: y (xXF x).
We will prove ∃xX, y F x.
Apply (UnionE_impred {F x|xX} y H1) to the current goal.
Let Y be given.
Assume H2: y Y.
Assume H3: Y {F x|xX}.
Apply (ReplE_impred X F Y H3) to the current goal.
Let x be given.
Assume H4: x X.
Assume H5: Y = F x.
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.
We will prove y F x.
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 : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)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.
Theorem. (famunion_Empty)
∀F : setset, (xEmptyF x) = Empty
Proof:
Let F be given.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y xEmptyF x.
Apply famunionE_impred Empty F y Hy to the current goal.
Let x be given.
Assume Hx: x Empty.
We will prove False.
An exact proof term for the current goal is EmptyE x Hx.
Theorem. (famunion_Subq)
∀X, ∀f g : setset, (∀xX, f x g x)famunion X f famunion X g
Proof:
Let X, f and g be given.
Assume Hfg.
Let y be given.
Assume Hy.
Apply famunionE_impred X f y Hy to the current goal.
Let x be given.
Assume Hx.
Assume H1: y f x.
Apply famunionI X g x y Hx to the current goal.
We will prove y g x.
An exact proof term for the current goal is Hfg x Hx y H1.
Theorem. (famunion_ext)
∀X, ∀f g : setset, (∀xX, f x = g x)famunion X f = famunion X g
Proof:
Let X, f and g be given.
Assume Hfg.
Apply set_ext to the current goal.
Apply famunion_Subq to the current goal.
Let x be given.
Assume Hx.
rewrite the current goal using Hfg x Hx (from left to right).
Apply Subq_ref to the current goal.
Apply famunion_Subq to the current goal.
Let x be given.
Assume Hx.
rewrite the current goal using Hfg x Hx (from left to right).
Apply Subq_ref to the current goal.
Beginning of Section SepSec
Variable X : set
Variable P : setprop
Let z : setEps_i (λz ⇒ z X P z)
Let F : setsetλx ⇒ if P x then x else z
Definition. We define Sep to be if (∃zX, P z) then {F x|xX} else Empty of type set.
End of Section SepSec
Notation. {xA | B} is notation for Sep Ax . B).
Theorem. (SepI)
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|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 setset.
Assume H1: x X.
Assume H2: P x.
We prove the intermediate claim L1: ∃zX, 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 {xX|P x}.
We will prove x if (∃zX, P z) then {F x|xX} else Empty.
We prove the intermediate claim L2: (if (∃zX, P z) then {F x|xX} else Empty) = {F x|xX}.
An exact proof term for the current goal is (If_i_1 (∃zX, P z) {F x|xX} Empty L1).
rewrite the current goal using L2 (from left to right).
We will prove x {F x|xX}.
We prove the intermediate claim L3: F x = x.
We will prove (if P x then x else z) = 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|xX}.
An exact proof term for the current goal is (ReplI X F x H1).
Theorem. (SepE)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|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 setset.
Apply (xm (∃zX, P z)) to the current goal.
Assume H1: ∃zX, P z.
We will prove (x (if (∃zX, P z) then {F x|xX} else Empty)x X P x).
We prove the intermediate claim L1: (if (∃zX, P z) then {F x|xX} else Empty) = {F x|xX}.
An exact proof term for the current goal is (If_i_1 (∃zX, P z) {F x|xX} Empty H1).
rewrite the current goal using L1 (from left to right).
We will prove x {F x|xX}x X P x.
Assume H2: x {F x|xX}.
Apply (ReplE_impred X F x H2) to the current goal.
Let y be given.
Assume H3: y X.
Assume H4: x = F y.
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.
Assume H5: ¬ P y.
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).
Assume H1: ¬ ∃zX, P z.
We will prove (x (if (∃zX, P z) then {F x|xX} else Empty)x X P x).
We prove the intermediate claim L1: (if (∃zX, P z) then {F x|xX} else Empty) = Empty.
An exact proof term for the current goal is (If_i_0 (∃zX, P z) {F x|xX} Empty H1).
rewrite the current goal using L1 (from left to right).
We will prove x Emptyx X P x.
Assume H2: x Empty.
We will prove False.
An exact proof term for the current goal is (EmptyE x H2).
Theorem. (SepE1)
∀X : set, ∀P : (setprop), ∀x : set, x {xX|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 : (setprop), ∀x : set, x {xX|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)).
Theorem. (Sep_Empty)
∀P : setprop, {xEmpty|P x} = Empty
Proof:
Let P be given.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx.
An exact proof term for the current goal is EmptyE x (SepE1 Empty P x Hx).
Theorem. (Sep_Subq)
∀X : set, ∀P : setprop, {xX|P x} X
Proof:
An exact proof term for the current goal is SepE1.
Theorem. (Sep_In_Power)
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
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{zX|P z}} of type set(setprop)(setset)set.
Notation. {B| xA, C} is notation for ReplSep Ax . C) (λ x . B).
Theorem. (ReplSepI)
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, 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 : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∃x : set, x X P x y = F x
Proof:
Let X, P, F and y be given.
Assume H1: y {F x|x{zX|P z}}.
Apply (ReplE {zX|P z} F y H1) to the current goal.
Let x be given.
Assume H2: x {zX|P z} y = F x.
Apply H2 to the current goal.
Assume H3: x {zX|P z}.
Assume H4: y = F x.
Apply (SepE X P x H3) to the current goal.
Assume H5: x X.
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 : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (∀xX, P xy = F xp)p
Proof:
Let X, P, F and y be given.
Assume H1: y {F x|xX, P x}.
Let p be given.
Assume H2: ∀xX, P xy = F xp.
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 ⇒ {xX|x Y} of type setsetset.
Notation. We use as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
Theorem. (binintersectI)
∀X Y z, z Xz Yz X Y
Proof:
An exact proof term for the current goal is (λX Y z H1 H2 ⇒ SepI X (λx : setx Y) z H1 H2).
Theorem. (binintersectE)
∀X Y z, z X Yz X z Y
Proof:
An exact proof term for the current goal is (λX Y z H1 ⇒ SepE X (λx : setx Y) z H1).
Theorem. (binintersectE1)
∀X Y z, z X Yz X
Proof:
An exact proof term for the current goal is (λX Y z H1 ⇒ SepE1 X (λx : setx Y) z H1).
Theorem. (binintersectE2)
∀X Y z, z X Yz Y
Proof:
An exact proof term for the current goal is (λX Y z H1 ⇒ SepE2 X (λx : setx Y) z H1).
Theorem. (binintersect_Subq_1)
∀X Y : set, X Y X
Proof:
An exact proof term for the current goal is binintersectE1.
Theorem. (binintersect_Subq_2)
∀X Y : set, X Y Y
Proof:
An exact proof term for the current goal is binintersectE2.
Theorem. (binintersect_Subq_eq_1)
∀X Y, X YX Y = X
Proof:
Let X and Y be given.
Assume H1: X Y.
Apply set_ext to the current goal.
Apply binintersect_Subq_1 to the current goal.
Let x be given.
Assume H2: x X.
Apply binintersectI to the current goal.
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.
Theorem. (binintersect_Subq_max)
∀X Y Z : set, Z XZ YZ X Y
Proof:
Let X, Y and Z be given.
Assume H1: Z X.
Assume H2: Z Y.
Let w be given.
Assume H3: w Z.
Apply (binintersectI X Y w) to the current goal.
We will prove w X.
An exact proof term for the current goal is (H1 w H3).
We will prove w Y.
An exact proof term for the current goal is (H2 w H3).
Theorem. (binintersect_com_Subq)
∀X Y : set, X Y Y X
Proof:
Let X and Y be given.
Apply (binintersect_Subq_max Y X (X Y)) to the current goal.
We will prove X Y Y.
Apply binintersect_Subq_2 to the current goal.
We will prove X Y X.
Apply binintersect_Subq_1 to the current goal.
Theorem. (binintersect_com)
∀X Y : set, X Y = Y X
Proof:
Let X and Y be given.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_com_Subq X Y).
An exact proof term for the current goal is (binintersect_com_Subq Y X).
Definition. We define setminus to be λX Y ⇒ Sep X (λx ⇒ x Y) of type setsetset.
Notation. We use as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
Theorem. (setminusI)
∀X Y z, (z X)(z Y)z X Y
Proof:
An exact proof term for the current goal is (λX Y z H1 H2 ⇒ SepI X (λx : setx Y) z H1 H2).
Theorem. (setminusE)
∀X Y z, (z X Y)z X z Y
Proof:
An exact proof term for the current goal is (λX Y z H ⇒ SepE X (λx : setx Y) z H).
Theorem. (setminusE1)
∀X Y z, (z X Y)z X
Proof:
An exact proof term for the current goal is (λX Y z H ⇒ SepE1 X (λx : setx Y) z H).
Theorem. (setminusE2)
∀X Y z, (z X Y)z Y
Proof:
An exact proof term for the current goal is (λX Y z H ⇒ SepE2 X (λx : setx Y) z H).
Theorem. (setminus_Subq)
∀X Y : set, X Y X
Proof:
An exact proof term for the current goal is setminusE1.
Theorem. (setminus_Subq_contra)
∀X Y Z : set, Z YX Y X Z
Proof:
Let X, Y and Z be given.
Assume H1: Z Y.
Let x be given.
Assume H2: x X Y.
Apply (setminusE X Y x H2) to the current goal.
Assume H3: x X.
Assume H4: x Y.
We will prove x X Z.
Apply setminusI to the current goal.
An exact proof term for the current goal is H3.
We will prove x Z.
An exact proof term for the current goal is (Subq_contra Z Y x H1 H4).
Theorem. (setminus_In_Power)
∀A U, A U 𝒫 A
Proof:
Let A and U be given.
Apply PowerI to the current goal.
Apply setminus_Subq to the current goal.
Theorem. (setminus_idr)
∀X, X Empty = X
Proof:
Let X be given.
Apply set_ext to the current goal.
An exact proof term for the current goal is setminus_Subq X Empty.
Let u be given.
Assume Hu: u X.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is EmptyE u.
Theorem. (In_irref)
∀x, x x
Proof:
Apply In_ind to the current goal.
We will prove (∀X : set, (∀x : set, x Xx x)X X).
Let X be given.
Assume IH: ∀x : set, x Xx x.
Assume H: X X.
An exact proof term for the current goal is IH X H H.
Theorem. (In_no2cycle)
∀x y, x yy xFalse
Proof:
Apply In_ind to the current goal.
Let x be given.
Assume IH: ∀z, z x∀y, z yy zFalse.
Let y be given.
Assume H1: x y.
Assume H2: y x.
An exact proof term for the current goal is IH y H2 x H2 H1.
Definition. We define ordsucc to be λx : setx {x} of type setset.
Theorem. (ordsuccI1)
∀x : set, x ordsucc x
Proof:
Let x be given.
An exact proof term for the current goal is (λ(y : set)(H1 : y x) ⇒ binunionI1 x {x} y H1).
Theorem. (ordsuccI2)
∀x : set, x ordsucc x
Proof:
An exact proof term for the current goal is (λx : setbinunionI2 x {x} x (SingI x)).
Theorem. (ordsuccE)
∀x y : set, y ordsucc xy x y = x
Proof:
Let x and y be given.
Assume H1: y x {x}.
Apply (binunionE x {x} y H1) to the current goal.
Assume H2: y x.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Assume H2: y {x}.
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.
Theorem. (neq_0_ordsucc)
∀a : set, 0 ordsucc a
Proof:
Let a be given.
We will prove ¬ (0 = ordsucc a).
Assume H1: 0 = ordsucc a.
We prove the intermediate claim L1: a ordsucc aFalse.
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)).
Theorem. (neq_ordsucc_0)
∀a : set, ordsucc a 0
Proof:
Let a be given.
An exact proof term for the current goal is neq_i_sym 0 (ordsucc a) (neq_0_ordsucc a).
Theorem. (ordsucc_inj)
∀a b : set, ordsucc a = ordsucc ba = b
Proof:
Let a and b be given.
Assume H1: ordsucc a = ordsucc b.
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.
Assume H2: a b.
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.
Assume H3: b a.
We will prove False.
An exact proof term for the current goal is (In_no2cycle a b H2 H3).
Assume H3: b = a.
Use symmetry.
An exact proof term for the current goal is H3.
Assume H2: a = b.
An exact proof term for the current goal is H2.
Theorem. (ordsucc_inj_contra)
∀a b : set, a bordsucc a ordsucc b
Proof:
Let a and b be given.
Assume H1.
We will prove ¬ (ordsucc a = ordsucc b).
Assume H2: ordsucc a = ordsucc b.
An exact proof term for the current goal is H1 (ordsucc_inj a b H2).
Theorem. (In_0_1)
Proof:
An exact proof term for the current goal is (ordsuccI2 0).
Theorem. (In_0_2)
Proof:
An exact proof term for the current goal is (ordsuccI1 1 0 In_0_1).
Theorem. (In_1_2)
Proof:
An exact proof term for the current goal is (ordsuccI2 1).
Theorem. (In_1_3)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_2.
Theorem. (In_2_3)
Proof:
Apply ordsuccI2 to the current goal.
Theorem. (In_1_4)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_3.
Theorem. (In_2_4)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_2_3.
Theorem. (In_3_4)
Proof:
Apply ordsuccI2 to the current goal.
Theorem. (In_1_5)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_4.
Theorem. (In_2_5)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_2_4.
Theorem. (In_3_5)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_3_4.
Theorem. (In_4_5)
Proof:
Apply ordsuccI2 to the current goal.
Theorem. (In_1_6)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_5.
Theorem. (In_1_7)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_6.
Theorem. (In_1_8)
Proof:
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is In_1_7.
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp (ordsucc x))p n of type setprop.
Theorem. (nat_0)
Proof:
An exact proof term for the current goal is (λp H _ ⇒ H).
Theorem. (nat_ordsucc)
∀n : set, nat_p nnat_p (ordsucc n)
Proof:
An exact proof term for the current goal is (λn H1 p H2 H3 ⇒ H3 n (H1 p H2 H3)).
Theorem. (nat_1)
Proof:
An exact proof term for the current goal is (nat_ordsucc 0 nat_0).
Theorem. (nat_2)
Proof:
An exact proof term for the current goal is (nat_ordsucc 1 nat_1).
Theorem. (nat_3)
Proof:
An exact proof term for the current goal is nat_ordsucc 2 nat_2.
Theorem. (nat_4)
Proof:
An exact proof term for the current goal is nat_ordsucc 3 nat_3.
Theorem. (nat_5)
Proof:
An exact proof term for the current goal is nat_ordsucc 4 nat_4.
Theorem. (nat_6)
Proof:
An exact proof term for the current goal is nat_ordsucc 5 nat_5.
Theorem. (nat_7)
Proof:
An exact proof term for the current goal is nat_ordsucc 6 nat_6.
Theorem. (nat_8)
Proof:
An exact proof term for the current goal is nat_ordsucc 7 nat_7.
Theorem. (nat_0_in_ordsucc)
∀n, nat_p n0 ordsucc n
Proof:
Let n be given.
Assume H1.
Apply H1 (λn ⇒ 0 ordsucc n) to the current goal.
We will prove 0 ordsucc 0.
An exact proof term for the current goal is In_0_1.
Let n be given.
Assume IH: 0 ordsucc n.
We will prove 0 ordsucc (ordsucc n).
An exact proof term for the current goal is (ordsuccI1 (ordsucc n) 0 IH).
Theorem. (nat_ordsucc_in_ordsucc)
∀n, nat_p n∀mn, ordsucc m ordsucc n
Proof:
Let n be given.
Assume H1.
Apply (H1 (λn ⇒ ∀mn, ordsucc m ordsucc n)) to the current goal.
We will prove ∀m0, ordsucc m ordsucc 0.
Let m be given.
Assume Hm: m 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume IH: ∀mn, ordsucc m ordsucc n.
We will prove ∀mordsucc n, ordsucc m ordsucc (ordsucc n).
Let m be given.
Assume H2: m ordsucc n.
We will prove ordsucc m ordsucc (ordsucc n).
Apply (ordsuccE n m H2) to the current goal.
Assume H3: m n.
We prove the intermediate claim L1: ordsucc m ordsucc n.
An exact proof term for the current goal is (IH m H3).
An exact proof term for the current goal is (ordsuccI1 (ordsucc n) (ordsucc m) L1).
Assume H3: m = n.
rewrite the current goal using H3 (from left to right).
We will prove ordsucc n ordsucc (ordsucc n).
An exact proof term for the current goal is (ordsuccI2 (ordsucc n)).
Theorem. (nat_ind)
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Proof:
Let p be given.
Assume H1: p 0.
Assume H2: ∀n, nat_p np np (ordsucc n).
We prove the intermediate claim L1: nat_p 0 p 0.
An exact proof term for the current goal is (andI (nat_p 0) (p 0) nat_0 H1).
We prove the intermediate claim L2: ∀n, nat_p n p nnat_p (ordsucc n) p (ordsucc n).
Let n be given.
Assume H3: nat_p n p n.
Apply H3 to the current goal.
Assume H4: nat_p n.
Assume H5: p n.
Apply andI to the current goal.
We will prove nat_p (ordsucc n).
An exact proof term for the current goal is (nat_ordsucc n H4).
We will prove p (ordsucc n).
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).
Theorem. (nat_inv_impred)
∀p : setprop, p 0(∀n, nat_p np (ordsucc n))∀n, nat_p np n
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).
Theorem. (nat_inv)
∀n, nat_p nn = 0 ∃x, nat_p x n = ordsucc x
Proof:
Apply nat_inv_impred to the current goal.
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.
Use reflexivity.
Theorem. (nat_complete_ind)
∀p : setprop, (∀n, nat_p n(∀mn, p m)p n)∀n, nat_p np n
Proof:
Let p be given.
Assume H1: ∀n, nat_p n(∀mn, p m)p n.
We prove the intermediate claim L1: ∀n : set, nat_p n∀mn, p m.
Apply nat_ind to the current goal.
We will prove ∀m0, p m.
Let m be given.
Assume Hm: m 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀mn, p m.
We will prove ∀mordsucc n, p m.
Let m be given.
Assume Hm: m ordsucc n.
We will prove p m.
Apply (ordsuccE n m Hm) to the current goal.
Assume H2: m n.
An exact proof term for the current goal is (IHn m H2).
Assume H2: m = n.
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 np n.
An exact proof term for the current goal is (λn Hn ⇒ H1 n Hn (L1 n Hn)).
Theorem. (nat_p_trans)
∀n, nat_p n∀mn, nat_p m
Proof:
Apply nat_ind to the current goal.
We will prove ∀m0, nat_p m.
Let m be given.
Assume Hm: m 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀mn, nat_p m.
We will prove ∀mordsucc n, nat_p m.
Let m be given.
Assume Hm: m ordsucc n.
Apply (ordsuccE n m Hm) to the current goal.
Assume H1: m n.
An exact proof term for the current goal is (IHn m H1).
Assume H1: m = n.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hn.
Theorem. (nat_trans)
∀n, nat_p n∀mn, m n
Proof:
Apply nat_ind to the current goal.
We will prove ∀m0, m 0.
Let m be given.
Assume Hm: m 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀mn, m n.
We will prove ∀mordsucc n, m ordsucc n.
Let m be given.
Assume Hm: m ordsucc n.
Apply (ordsuccE n m Hm) to the current goal.
Assume H1: m n.
We will prove m ordsucc n.
Apply (Subq_tra m n (ordsucc n)) 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).
Assume H1: m = n.
We will prove m ordsucc n.
rewrite the current goal using H1 (from left to right).
We will prove n ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n).
Theorem. (nat_ordsucc_trans)
∀n, nat_p n∀mordsucc n, m n
Proof:
Let n be given.
Assume Hn: nat_p n.
Let m be given.
Assume Hm: m ordsucc n.
Let k be given.
Assume Hk: k m.
We will prove k n.
Apply (ordsuccE n m Hm) to the current goal.
Assume H1: m n.
An exact proof term for the current goal is nat_trans n Hn m H1 k Hk.
Assume H1: m = n.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hk.
Theorem. (Union_ordsucc_eq)
∀n, nat_p n (ordsucc n) = n
Proof:
Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀mn, (ordsucc m) = m.
We will prove (ordsucc n) = n.
Apply set_ext to the current goal.
Let m be given.
Assume Hm: m (ordsucc n).
Apply (UnionE_impred (ordsucc n) m Hm) to the current goal.
Let k be given.
Assume H1: m k.
Assume H2: k ordsucc n.
We will prove m n.
An exact proof term for the current goal is nat_ordsucc_trans n Hn k H2 m H1.
Let m be given.
Assume Hm: m n.
We will prove m (ordsucc n).
Apply (UnionI (ordsucc n) m n) to the current goal.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is (ordsuccI2 n).
Theorem. (cases_1)
∀i1, ∀p : setprop, p 0p i
Proof:
Let i be given.
Assume Hi.
Let p be given.
Assume Hp0.
Apply ordsuccE 0 i Hi to the current goal.
Assume Hil: i 0.
Apply EmptyE i Hil to the current goal.
Assume Hie: i = 0.
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp0.
Theorem. (cases_2)
∀i2, ∀p : setprop, p 0p 1p i
Proof:
Let i be given.
Assume Hi.
Let p be given.
Assume Hp0 Hp1.
Apply ordsuccE 1 i Hi to the current goal.
Assume Hil: i 1.
An exact proof term for the current goal is cases_1 i Hil p Hp0.
Assume Hie: i = 1.
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp1.
Theorem. (cases_3)
∀i3, ∀p : setprop, p 0p 1p 2p i
Proof:
Let i be given.
Assume Hi.
Let p be given.
Assume Hp0 Hp1 Hp2.
Apply ordsuccE 2 i Hi to the current goal.
Assume Hil: i 2.
An exact proof term for the current goal is cases_2 i Hil p Hp0 Hp1.
Assume Hie: i = 2.
rewrite the current goal using Hie (from left to right).
An exact proof term for the current goal is Hp2.
Theorem. (neq_0_1)
Proof:
An exact proof term for the current goal is (neq_0_ordsucc 0).
Theorem. (neq_1_0)
Proof:
An exact proof term for the current goal is (neq_ordsucc_0 0).
Theorem. (neq_0_2)
Proof:
An exact proof term for the current goal is (neq_0_ordsucc 1).
Theorem. (neq_2_0)
Proof:
An exact proof term for the current goal is (neq_ordsucc_0 1).
Theorem. (neq_1_2)
Proof:
An exact proof term for the current goal is (ordsucc_inj_contra 0 1 neq_0_1).
Theorem. (neq_1_3)
Proof:
Apply ordsucc_inj_contra to the current goal.
An exact proof term for the current goal is neq_0_2.
Theorem. (neq_2_3)
Proof:
Apply ordsucc_inj_contra to the current goal.
An exact proof term for the current goal is neq_1_2.
Theorem. (neq_2_4)
Proof:
Apply ordsucc_inj_contra to the current goal.
An exact proof term for the current goal is neq_1_3.
Theorem. (neq_3_4)
Proof:
Apply ordsucc_inj_contra to the current goal.
An exact proof term for the current goal is neq_2_3.
Theorem. (ZF_closed_E)
∀U, ZF_closed U∀p : prop, (Union_closed UPower_closed URepl_closed Up)p
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))).
Theorem. (ZF_Union_closed)
∀U, ZF_closed U∀XU, X U
Proof:
An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀XU, X U) (λH _ _ ⇒ H)).
Theorem. (ZF_Power_closed)
∀U, ZF_closed U∀XU, 𝒫 X U
Proof:
An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀XU, 𝒫 X U) (λ_ H _ ⇒ H)).
Theorem. (ZF_Repl_closed)
∀U, ZF_closed U∀XU, ∀F : setset, (∀xX, F x U){F x|xX} U
Proof:
An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀XU, ∀F : setset, (∀xX, F x U){F x|xX} U) (λ_ _ H ⇒ H)).
Theorem. (ZF_UPair_closed)
∀U, ZF_closed U∀x yU, {x,y} U
Proof:
Let U be given.
Assume C: ZF_closed U.
Let x be given.
Assume Hx: x U.
Let y be given.
Assume Hy: y U.
We will prove {x,y} U.
We prove the intermediate claim L1: {if x X then x else y|X𝒫 (𝒫 x)} = {x,y}.
Apply set_ext to the current goal.
We will prove {if x X then x else y|X𝒫 (𝒫 x)} {x,y}.
Let z be given.
Assume Hz: z {if x X then x else y|X𝒫 (𝒫 x)}.
We will prove z {x,y}.
Apply (ReplE_impred (𝒫 (𝒫 x)) (λX ⇒ if x X then x else y) z Hz) to the current goal.
Let X be given.
Assume _.
We will prove z = (if x X then x else y)z {x,y}.
Apply (xm (x X)) to the current goal.
Assume H2: x X.
rewrite the current goal using (If_i_1 (x X) x y H2) (from left to right).
We will prove (z = xz {x,y}).
Assume H3: z = x.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is (UPairI1 x y).
Assume H2: x X.
rewrite the current goal using (If_i_0 (x X) x y H2) (from left to right).
We will prove (z = yz {x,y}).
Assume H3: z = y.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is (UPairI2 x y).
We will prove {x,y} {if x X then x else y|X𝒫 (𝒫 x)}.
Let z be given.
Assume Hz: z {x,y}.
We will prove z {if x X then x else y|X𝒫 (𝒫 x)}.
We prove the intermediate claim L1a: (if x (𝒫 x) then x else y) {if x X then x else y|X𝒫 (𝒫 x)}.
Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x X then x else y) (𝒫 x)) to the current goal.
We will prove 𝒫 x 𝒫 (𝒫 x).
An exact proof term for the current goal is (Self_In_Power (𝒫 x)).
We prove the intermediate claim L1b: (if x Empty then x else y) {if x X then x else y|X𝒫 (𝒫 x)}.
Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x X then x else y) Empty) to the current goal.
We will prove Empty 𝒫 (𝒫 x).
An exact proof term for the current goal is (Empty_In_Power (𝒫 x)).
Apply (UPairE z x y Hz) to the current goal.
Assume H1: z = x.
rewrite the current goal using H1 (from left to right).
We will prove x {if x X then x else y|X𝒫 (𝒫 x)}.
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.
Assume H1: z = y.
rewrite the current goal using H1 (from left to right).
We will prove y {if x X then x else y|X𝒫 (𝒫 x)}.
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.
We will prove {x,y} U.
rewrite the current goal using L1 (from right to left).
We will prove {if x X then x else y|X𝒫 (𝒫 x)} U.
We prove the intermediate claim L2: 𝒫 (𝒫 x) U.
An exact proof term for the current goal is (ZF_Power_closed U C (𝒫 x) (ZF_Power_closed U C x Hx)).
We prove the intermediate claim L3: ∀X𝒫 (𝒫 x), (if x X then x else y) U.
Let X be given.
Assume _.
We will prove (if x X then x else y) U.
Apply (xm (x X)) to the current goal.
Assume H1: x X.
rewrite the current goal using (If_i_1 (x X) x y H1) (from left to right).
We will prove x U.
An exact proof term for the current goal is Hx.
Assume H1: x X.
rewrite the current goal using (If_i_0 (x X) x y H1) (from left to right).
We will prove y U.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (ZF_Repl_closed U C (𝒫 (𝒫 x)) L2 (λX ⇒ if x X then x else y) L3).
Theorem. (ZF_Sing_closed)
∀U, ZF_closed U∀xU, {x} U
Proof:
An exact proof term for the current goal is (λU C x H ⇒ ZF_UPair_closed U C x H x H).
Theorem. (ZF_binunion_closed)
∀U, ZF_closed U∀X YU, (X Y) U
Proof:
An exact proof term for the current goal is (λU C X HX Y HY ⇒ ZF_Union_closed U C {X,Y} (ZF_UPair_closed U C X HX Y HY)).
Theorem. (ZF_ordsucc_closed)
∀U, ZF_closed U∀xU, ordsucc x U
Proof:
An exact proof term for the current goal is (λU C x H ⇒ ZF_binunion_closed U C x H {x} (ZF_Sing_closed U C x H)).
Theorem. (nat_p_UnivOf_Empty)
∀n : set, nat_p nn UnivOf Empty
Proof:
Apply nat_ind to the current goal.
We will prove 0 UnivOf Empty.
An exact proof term for the current goal is (UnivOf_In Empty).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: n UnivOf Empty.
We will prove ordsucc n UnivOf Empty.
An exact proof term for the current goal is (ZF_ordsucc_closed (UnivOf Empty) (UnivOf_ZF_closed Empty) n IHn).
Definition. We define ω to be {nUnivOf Empty|nat_p n} of type set.
Theorem. (omega_nat_p)
∀nω, nat_p n
Proof:
An exact proof term for the current goal is (λn H ⇒ SepE2 (UnivOf Empty) nat_p n H).
Theorem. (nat_p_omega)
∀n : set, nat_p nn ω
Proof:
Let n be given.
Assume H: nat_p n.
We will prove n {nUnivOf Empty|nat_p n}.
Apply SepI to the current goal.
We will prove n UnivOf Empty.
An exact proof term for the current goal is (nat_p_UnivOf_Empty n H).
We will prove nat_p n.
An exact proof term for the current goal is H.
Theorem. (omega_ordsucc)
Proof:
Let n be given.
Assume Hn.
Apply nat_p_omega to the current goal.
Apply nat_ordsucc to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hn.
Definition. We define ordinal to be λalpha : setTransSet alpha ∀betaalpha, TransSet beta of type setprop.
Theorem. (ordinal_TransSet)
∀alpha : set, ordinal alphaTransSet alpha
Proof:
An exact proof term for the current goal is (λalpha H ⇒ andEL (TransSet alpha) (∀betaalpha, TransSet beta) H).
Theorem. (ordinal_Empty)
Proof:
We will prove TransSet Empty ∀xEmpty, TransSet x.
Apply andI to the current goal.
Let x be given.
Assume Hx: x Empty.
We will prove False.
An exact proof term for the current goal is (EmptyE x Hx).
Let x be given.
Assume Hx: x Empty.
We will prove False.
An exact proof term for the current goal is (EmptyE x Hx).
Theorem. (ordinal_Hered)
∀alpha : set, ordinal alpha∀betaalpha, ordinal beta
Proof:
Let alpha be given.
Assume H1: TransSet alpha ∀xalpha, TransSet x.
Let beta be given.
Assume H2: beta alpha.
We will prove TransSet beta ∀xbeta, TransSet x.
Apply H1 to the current goal.
Assume H3: TransSet alpha.
Assume H4: ∀xalpha, TransSet x.
Apply andI to the current goal.
An exact proof term for the current goal is (H4 beta H2).
We will prove ∀xbeta, TransSet x.
Let x be given.
Assume Hx: x beta.
We prove the intermediate claim L1: x alpha.
An exact proof term for the current goal is (H3 beta H2 x Hx).
We will prove TransSet x.
An exact proof term for the current goal is (H4 x L1).
Theorem. (TransSet_ordsucc)
∀X : set, TransSet XTransSet (ordsucc X)
Proof:
Let X be given.
Assume H1: TransSet X.
Let x be given.
Assume H2: x ordsucc X.
Let y be given.
Assume H3: y x.
We will prove y ordsucc X.
Apply (ordsuccE X x H2) to the current goal.
Assume H4: x X.
Apply ordsuccI1 to the current goal.
We will prove y X.
An exact proof term for the current goal is (H1 x H4 y H3).
Assume H4: x = X.
Apply ordsuccI1 to the current goal.
We will prove y X.
rewrite the current goal using H4 (from right to left).
We will prove y x.
An exact proof term for the current goal is H3.
Theorem. (ordinal_ordsucc)
∀alpha : set, ordinal alphaordinal (ordsucc alpha)
Proof:
Let alpha be given.
Assume H1: TransSet alpha ∀betaalpha, TransSet beta.
Apply H1 to the current goal.
Assume H2: TransSet alpha.
Assume H3: ∀betaalpha, TransSet beta.
We will prove TransSet (ordsucc alpha) ∀betaordsucc alpha, TransSet beta.
Apply andI to the current goal.
An exact proof term for the current goal is (TransSet_ordsucc alpha H2).
Let beta be given.
Assume H4: beta ordsucc alpha.
We will prove TransSet beta.
Apply (ordsuccE alpha beta H4) to the current goal.
Assume H5: beta alpha.
An exact proof term for the current goal is (H3 beta H5).
Assume H5: beta = alpha.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H2.
Theorem. (nat_p_ordinal)
∀n : set, nat_p nordinal n
Proof:
Apply nat_ind to the current goal.
We will prove ordinal 0.
An exact proof term for the current goal is ordinal_Empty.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ordinal n.
We will prove ordinal (ordsucc n).
An exact proof term for the current goal is (ordinal_ordsucc n IHn).
Theorem. (ordinal_1)
Proof:
An exact proof term for the current goal is nat_p_ordinal 1 nat_1.
Theorem. (ordinal_2)
Proof:
An exact proof term for the current goal is nat_p_ordinal 2 nat_2.
Theorem. (omega_TransSet)
Proof:
Let n be given.
Assume Hn: n ω.
Let m be given.
Assume Hm: m n.
We will prove m ω.
Apply nat_p_omega to the current goal.
We will prove nat_p m.
Apply (nat_p_trans n) to the current goal.
We will prove nat_p n.
An exact proof term for the current goal is (omega_nat_p n Hn).
We will prove m n.
An exact proof term for the current goal is Hm.
Theorem. (omega_ordinal)
Proof:
We will prove TransSet ω ∀nω, TransSet n.
Apply andI to the current goal.
An exact proof term for the current goal is omega_TransSet.
Let n be given.
Assume Hn: n ω.
We will prove TransSet n.
Apply ordinal_TransSet to the current goal.
We will prove ordinal n.
Apply nat_p_ordinal to the current goal.
We will prove nat_p n.
An exact proof term for the current goal is (omega_nat_p n Hn).
Theorem. (ordsucc_omega_ordinal)
Proof:
An exact proof term for the current goal is ordinal_ordsucc ω omega_ordinal.
Theorem. (TransSet_ordsucc_In_Subq)
∀X : set, TransSet X∀xX, ordsucc x X
Proof:
Let X be given.
Assume H1: TransSet X.
Let x be given.
Assume H2: x X.
Let y be given.
Assume H3: y ordsucc x.
We will prove y X.
Apply (ordsuccE x y H3) to the current goal.
Assume H4: y x.
An exact proof term for the current goal is (H1 x H2 y H4).
Assume H4: y = x.
rewrite the current goal using H4 (from left to right).
We will prove x X.
An exact proof term for the current goal is H2.
Theorem. (ordinal_ordsucc_In_Subq)
∀alpha, ordinal alpha∀betaalpha, ordsucc beta alpha
Proof:
Let alpha be given.
Assume H: ordinal alpha.
An exact proof term for the current goal is (TransSet_ordsucc_In_Subq alpha (ordinal_TransSet alpha H)).
Theorem. (ordinal_trichotomy_or)
∀alpha beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha
Proof:
Apply In_ind to the current goal.
Let alpha be given.
Assume IHalpha: ∀gammaalpha, ∀beta : set, ordinal gammaordinal betagamma beta gamma = beta beta gamma.
We will prove ∀beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha.
Apply In_ind to the current goal.
Let beta be given.
Assume IHbeta: ∀deltabeta, ordinal alphaordinal deltaalpha delta alpha = delta delta alpha.
Assume Halpha: ordinal alpha.
Assume Hbeta: ordinal beta.
We will prove alpha beta alpha = beta beta alpha.
Apply (xm (alpha beta)) to the current goal.
Assume H1: alpha beta.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: alpha beta.
Apply (xm (beta alpha)) to the current goal.
Assume H2: beta alpha.
Apply or3I3 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: beta alpha.
Apply or3I2 to the current goal.
We will prove alpha = beta.
Apply set_ext to the current goal.
We will prove alpha beta.
Let gamma be given.
Assume H3: gamma alpha.
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.
Assume H4: gamma beta.
An exact proof term for the current goal is H4.
Assume H4: gamma = beta.
We will prove False.
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.
Assume H4: beta gamma.
We will prove False.
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.
Assume H3: delta beta.
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.
Assume H4: alpha delta.
We will prove False.
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).
Assume H4: alpha = delta.
We will prove False.
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.
Assume H4: delta alpha.
An exact proof term for the current goal is H4.
Theorem. (ordinal_trichotomy_or_impred)
∀alpha beta : set, ordinal alphaordinal beta∀p : prop, (alpha betap)(alpha = betap)(beta alphap)p
Proof:
Let alpha and beta be given.
Assume H1 H2.
An exact proof term for the current goal is (or3E (alpha beta) (alpha = beta) (beta alpha) (ordinal_trichotomy_or alpha beta H1 H2)).
Theorem. (ordinal_In_Or_Subq)
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Proof:
Let alpha and beta be given.
Assume H1: ordinal alpha.
Assume H2: ordinal beta.
Apply (or3E (alpha beta) (alpha = beta) (beta alpha) (ordinal_trichotomy_or alpha beta H1 H2)) to the current goal.
Assume H3: alpha beta.
Apply orIL to the current goal.
An exact proof term for the current goal is H3.
Assume H3: alpha = beta.
Apply orIR to the current goal.
rewrite the current goal using H3 (from left to right).
Apply Subq_ref to the current goal.
Assume H3: beta alpha.
Apply orIR to the current goal.
An exact proof term for the current goal is (ordinal_TransSet alpha H1 beta H3).
Theorem. (ordinal_linear)
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Proof:
Let alpha and beta be given.
Assume H1: ordinal alpha.
Assume H2: ordinal beta.
Apply (ordinal_In_Or_Subq alpha beta H1 H2) to the current goal.
Assume H3: alpha beta.
Apply orIL to the current goal.
An exact proof term for the current goal is (ordinal_TransSet beta H2 alpha H3).
Assume H3: beta alpha.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Theorem. (ordinal_ordsucc_In_eq)
∀alpha beta, ordinal alphabeta alphaordsucc beta alpha alpha = ordsucc beta
Proof:
Let alpha and beta be given.
Assume Ha Hb.
We prove the intermediate claim L1: ordinal (ordsucc beta).
An exact proof term for the current goal is ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb).
Apply ordinal_trichotomy_or alpha (ordsucc beta) Ha L1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H2: alpha ordsucc beta.
We will prove False.
Apply ordsuccE beta alpha H2 to the current goal.
Assume H3: alpha beta.
An exact proof term for the current goal is In_no2cycle alpha beta H3 Hb.
Assume H3: alpha = beta.
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.
Assume H2: alpha = ordsucc beta.
Apply orIR to the current goal.
An exact proof term for the current goal is H2.
Assume H2: ordsucc beta alpha.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Theorem. (ordinal_lim_or_succ)
∀alpha, ordinal alpha(∀betaalpha, ordsucc beta alpha) (∃betaalpha, alpha = ordsucc beta)
Proof:
Let alpha be given.
Assume Ha.
Apply xm (∃betaalpha, 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.
Assume H1: ¬ ∃betaalpha, alpha = ordsucc beta.
Apply orIL to the current goal.
Let beta be given.
Assume H2: beta alpha.
Apply ordinal_ordsucc_In_eq alpha beta Ha H2 to the current goal.
Assume H3: ordsucc beta alpha.
An exact proof term for the current goal is H3.
Assume H3: alpha = ordsucc beta.
We will prove False.
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.
Theorem. (ordinal_ordsucc_In)
∀alpha, ordinal alpha∀betaalpha, ordsucc beta ordsucc alpha
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 ordinal_ordsucc_In_Subq alpha Ha beta Hb.
Apply ordinal_In_Or_Subq (ordsucc beta) alpha (ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb)) Ha to the current goal.
Assume H1: ordsucc beta alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: alpha ordsucc beta.
We prove the intermediate claim L2: ordsucc beta = alpha.
Apply set_ext to the current goal.
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).
Apply ordsuccI2 to the current goal.
Theorem. (ordinal_famunion)
∀X, ∀F : setset, (∀xX, ordinal (F x))ordinal (xXF x)
Proof:
Let X and F be given.
Assume HXF.
We will prove TransSet (xXF x) ∀y(xXF x), TransSet y.
Apply andI to the current goal.
Let y be given.
Assume Hy: y xXF x.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1.
Apply H1 to the current goal.
Assume Hx: x X.
Assume Hy: y F x.
We will prove y xXF 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.
Assume Hz: z y.
We will prove z xXF 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.
Assume Hy: y xXF x.
We will prove TransSet y.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1.
Apply H1 to the current goal.
Assume Hx: x X.
Assume Hy: y F x.
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.
Theorem. (ordinal_binintersect)
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
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 _.
Apply ordinal_In_Or_Subq alpha beta Ha Hb to the current goal.
Assume H1: alpha beta.
rewrite the current goal using binintersect_Subq_eq_1 alpha beta (Hb1 alpha H1) (from left to right).
An exact proof term for the current goal is Ha.
Assume H1: beta alpha.
rewrite the current goal using binintersect_com (from left to right).
rewrite the current goal using binintersect_Subq_eq_1 beta alpha H1 (from left to right).
An exact proof term for the current goal is Hb.
Theorem. (ordinal_binunion)
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
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 _.
Apply ordinal_linear alpha beta Ha Hb to the current goal.
rewrite the current goal using Subq_binunion_eq (from left to right).
Assume H1: alpha beta = beta.
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 Subq_binunion_eq (from left to right).
rewrite the current goal using binunion_com (from left to right).
Assume H1: alpha beta = alpha.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Ha.
Theorem. (ordinal_ind)
∀p : setprop, (∀alpha, ordinal alpha(∀betaalpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Proof:
Let p be given.
Assume H1: ∀alpha, ordinal alpha(∀betaalpha, p beta)p alpha.
Apply In_ind to the current goal.
Let alpha be given.
Assume IH: ∀betaalpha, ordinal betap beta.
Assume H2: ordinal alpha.
We will prove p alpha.
Apply (H1 alpha H2) to the current goal.
Let beta be given.
Assume H3: beta alpha.
We will prove p beta.
Apply (IH beta H3) to the current goal.
We will prove ordinal beta.
An exact proof term for the current goal is (ordinal_Hered alpha H2 beta H3).
Theorem. (least_ordinal_ex)
∀p : setprop, (∃alpha, ordinal alpha p alpha)∃alpha, ordinal alpha p alpha ∀betaalpha, ¬ p beta
Proof:
Let p be given.
Assume H1.
Apply dneg to the current goal.
Assume H2: ¬ ∃alpha, ordinal alpha p alpha ∀betaalpha, ¬ p beta.
We prove the intermediate claim L1: ∀alpha, ordinal alpha¬ p alpha.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha.
Assume IH: ∀betaalpha, ¬ p beta.
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 Ha: ordinal alpha.
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 ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) of type setset(setset)prop.
Definition. We define bij to be λX Y f ⇒ (∀uX, f u Y) (∀u vX, f u = f vu = v) (∀wY, ∃uX, f u = w) of type setset(setset)prop.
Theorem. (bijI)
∀X Y, ∀f : setset, (∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, f u = w)bij X Y f
Proof:
Let X, Y and f be given.
Assume Hf1 Hf2 Hf3.
We will prove (∀uX, f u Y) (∀u vX, f u = f vu = v) (∀wY, ∃uX, 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 : setset, bij X Y f∀p : prop, ((∀uX, f u Y)(∀u vX, f u = f vu = v)(∀wY, ∃uX, 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 : setEps_i (λx ⇒ x X f x = y) of type set(setset)setset.
Theorem. (surj_rinv)
∀X Y, ∀f : setset, (∀wY, ∃uX, f u = w)∀yY, 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.
Assume Hy: y Y.
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 : setset, (∀u vX, f u = f vu = v)∀xX, 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.
Use reflexivity.
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.
Theorem. (bij_inv)
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Proof:
Let X, Y and f be given.
Assume H1.
Apply H1 to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H3: ∀uX, f u Y.
Assume H4: ∀u vX, f u = f vu = v.
Assume H5: ∀wY, ∃uX, f u = w.
Set g to be the term λy ⇒ Eps_i (λx ⇒ x X f x = y) of type setset.
We prove the intermediate claim L1: ∀yY, 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 (∀uY, g u X) (∀u vY, g u = g vu = v) (∀wX, ∃uY, g u = w).
Apply and3I to the current goal.
We will prove ∀uY, 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 vY, g u = g vu = v.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv H6.
We will prove u = v.
Apply L1 u Hu to the current goal.
Assume H7: g u X.
Assume H8: f (g u) = u.
Apply L1 v Hv to the current goal.
Assume H9: g v X.
Assume H10: f (g v) = v.
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 ∀wX, ∃uY, 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.
Theorem. (bij_id)
∀X, bij X X (λx ⇒ x)
Proof:
Let X be given.
We will prove (∀uX, u X) (∀u vX, u = vu = v) (∀wX, ∃uX, 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.
Use reflexivity.
Theorem. (bij_comp)
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij 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 (∀uX, g (f u) Z) (∀u vX, g (f u) = g (f v)u = v) (∀wZ, ∃uX, g (f u) = w).
Apply and3I to the current goal.
Let u be given.
Assume Hu: u X.
An exact proof term for the current goal is (Hg1 (f u) (Hf1 u Hu)).
Let u be given.
Assume Hu: u X.
Let v be given.
Assume Hv: v X.
Assume H1: g (f u) = g (f v).
We will prove u = v.
Apply Hf2 u Hu v Hv to the current goal.
We will prove f u = f v.
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.
Assume Hw: w Z.
Apply Hg3 w Hw to the current goal.
Let y be given.
Assume Hy12.
Apply Hy12 to the current goal.
Assume Hy1: y Y.
Assume Hy2: g y = w.
Apply Hf3 y Hy1 to the current goal.
Let u be given.
Assume Hu12.
Apply Hu12 to the current goal.
Assume Hu1: u X.
Assume Hu2: f u = y.
We will prove ∃uX, 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 : setset, bij X Y f of type setsetprop.
Theorem. (equip_ref)
∀X, equip X X
Proof:
Let X be given.
We will prove ∃f : setset, bij X X f.
We use (λx : setx) to witness the existential quantifier.
An exact proof term for the current goal is bij_id X.
Theorem. (equip_sym)
∀X Y, equip X Yequip Y X
Proof:
Let X and Y be given.
Assume H1.
Apply H1 to the current goal.
Let f be given.
Assume H2: bij X Y f.
We will prove ∃g : setset, 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.
Theorem. (equip_tra)
∀X Y Z, equip X Yequip Y Zequip X Z
Proof:
Let X, Y and Z be given.
Assume H1 H2.
Apply H1 to the current goal.
Let f be given.
Assume H3: bij X Y f.
Apply H2 to the current goal.
Let g be given.
Assume H4: bij Y Z g.
We will prove ∃h : setset, bij X Z h.
We use (λx : setg (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.
Theorem. (equip_0_Empty)
∀X, equip X 0X = 0
Proof:
Let X be given.
Assume H1.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx.
We will prove False.
Apply H1 to the current goal.
Let f be given.
Assume Hf: bij X 0 f.
Apply bijE X 0 f Hf to the current goal.
Assume Hf1: ∀xX, f x 0.
We will prove False.
An exact proof term for the current goal is EmptyE (f x) (Hf1 x Hx).
Beginning of Section SchroederBernstein
Theorem. (KnasterTarski_set)
∀A, ∀F : setset, (∀U𝒫 A, F U 𝒫 A)(∀U V𝒫 A, U VF U F V)∃Y𝒫 A, F Y = Y
Proof:
Let A and F be given.
Assume H1 H2.
Set Y to be the term {uA|∀X𝒫 A, F X Xu X} of type set.
We prove the intermediate claim L1: Y 𝒫 A.
Apply Sep_In_Power to the current goal.
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 XY X.
Let X be given.
Assume HX: X 𝒫 A.
Assume H3: F X X.
Let y be given.
Assume Hy: y Y.
An exact proof term for the current goal is SepE2 A (λu ⇒ ∀X𝒫 A, F X Xu X) y Hy X HX H3.
We prove the intermediate claim L4: F Y Y.
Let u be given.
Assume H3: u F Y.
We will prove u Y.
Apply SepI to the current goal.
We will prove u A.
An exact proof term for the current goal is PowerE A (F Y) L2 u H3.
Let X be given.
Assume HX: X 𝒫 A.
Assume H4: F X X.
We will prove u X.
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.
We will prove u X.
Apply H4 to the current goal.
We will prove u F X.
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.
Apply set_ext to the current goal.
An exact proof term for the current goal is L4.
We will prove Y F Y.
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.
Theorem. (image_In_Power)
∀A B, ∀f : setset, (∀xA, f x B)∀U𝒫 A, {f x|xU} 𝒫 B
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.
Assume Hy: y {f x|xU}.
Apply ReplE_impred U f y Hy to the current goal.
Let x be given.
Assume Hx: x U.
Assume H1: y = f x.
rewrite the current goal using H1 (from left to right).
Apply Hf to the current goal.
We will prove x A.
Apply PowerE A U HU to the current goal.
An exact proof term for the current goal is Hx.
Theorem. (image_monotone)
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Proof:
Let f, U and V be given.
Assume HUV.
Let y be given.
Assume Hy: y {f x|xU}.
Apply ReplE_impred U f y Hy to the current goal.
Let x be given.
Assume Hx: x U.
Assume H1: y = f x.
rewrite the current goal using H1 (from left to right).
We will prove f x {f x|xV}.
Apply ReplI to the current goal.
Apply HUV to the current goal.
An exact proof term for the current goal is Hx.
Theorem. (setminus_antimonotone)
∀A U V, U VA V A U
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.
Apply setminusI to the current goal.
An exact proof term for the current goal is H1.
Assume H3: x U.
Apply H2 to the current goal.
We will prove x V.
An exact proof term for the current goal is HUV x H3.
Theorem. (SchroederBernstein)
∀A B, ∀f g : setset, inj A B finj B A gequip A B
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|yB {f x|xA X}} of type setset.
We prove the intermediate claim L1: ∀U𝒫 A, F U 𝒫 A.
Let U be given.
Assume HU.
We will prove {g y|yB {f x|xA U}} 𝒫 A.
Apply image_In_Power B A g Hg1 to the current goal.
We will prove B {f x|xA U} 𝒫 B.
Apply setminus_In_Power to the current goal.
We prove the intermediate claim L2: ∀U V𝒫 A, U VF U F V.
Let U be given.
Assume HU.
Let V be given.
Assume HV HUV.
We will prove {g y|yB {f x|xA U}} {g y|yB {f x|xA V}}.
Apply image_monotone g to the current goal.
We will prove B {f x|xA U} B {f x|xA V}.
Apply setminus_antimonotone to the current goal.
We will prove {f x|xA V} {f x|xA U}.
Apply image_monotone f to the current goal.
We will prove A V A U.
Apply setminus_antimonotone to the current goal.
An exact proof term for the current goal is HUV.
Apply KnasterTarski_set A F L1 L2 to the current goal.
Let Y be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: Y 𝒫 A.
Assume H2: F Y = Y.
Set h to be the term λx ⇒ if x Y then inv B g x else f x of type setset.
We will prove ∃f : setset, bij A B f.
We use h to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx.
We will prove (if x Y then inv B g x else f x) B.
Apply xm (x Y) to the current goal.
Assume H3: x Y.
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.
Apply ReplE_impred (B {f x|xA Y}) g x L1 to the current goal.
Let y be given.
Assume H4: y B {f x|xA Y}.
Assume H5: x = g y.
We prove the intermediate claim L2: y B.
An exact proof term for the current goal is setminusE1 B {f x|xA 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).
We will prove y B.
An exact proof term for the current goal is L2.
Assume H3: x Y.
rewrite the current goal using If_i_0 (x Y) (inv B g x) (f x) H3 (from left to right).
We will prove f x B.
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.
We will prove (if x Y then inv B g x else f x) = (if y Y then inv B g y else f y)x = y.
Apply xm (x Y) to the current goal.
Assume H3: x Y.
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 = (if y Y then inv B g y else f y)x = y.
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.
Apply ReplE_impred (B {f x|xA Y}) g x Lx to the current goal.
Let z be given.
Assume Hz1: z B {f x|xA Y}.
Assume Hz2: x = g z.
Apply setminusE B {f x|xA Y} z Hz1 to the current goal.
Assume Hz1a Hz1b.
Apply xm (y Y) to the current goal.
Assume H4: y Y.
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 yx = 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.
Apply ReplE_impred (B {f x|xA Y}) g y Ly to the current goal.
Let w be given.
Assume Hw1: w B {f x|xA Y}.
Assume Hw2: y = g w.
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).
rewrite the current goal using inj_linv B g Hg2 w (setminusE1 B {f x|xA Y} w Hw1) (from left to right).
Assume H5: z = w.
We will prove g z = g w.
Use f_equal.
An exact proof term for the current goal is H5.
Assume H4: y Y.
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 yx = 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 yg z = y.
Assume H5: z = f y.
We will prove False.
Apply Hz1b to the current goal.
We will prove z {f x|xA Y}.
rewrite the current goal using H5 (from left to right).
Apply ReplI to the current goal.
We will prove y A Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is H4.
Assume H3: x Y.
rewrite the current goal using If_i_0 (x Y) (inv B g x) (f x) H3 (from left to right).
We will prove f x = (if y Y then inv B g y else f y)x = y.
Apply xm (y Y) to the current goal.
Assume H4: y Y.
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 yx = 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.
Apply ReplE_impred (B {f x|xA Y}) g y Ly to the current goal.
Let w be given.
Assume Hw1: w B {f x|xA Y}.
Assume Hw2: y = g w.
Apply setminusE B {f x|xA Y} w Hw1 to the current goal.
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).
Assume H5: f x = w.
We will prove False.
Apply Hw1b to the current goal.
We will prove w {f x|xA Y}.
rewrite the current goal using H5 (from right to left).
Apply ReplI to the current goal.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H3.
Assume H4: y Y.
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 yx = y.
An exact proof term for the current goal is Hf2 x Hx y Hy.
Let w be given.
Assume Hw: w B.
Apply xm (w {f x|xA Y}) to the current goal.
Assume H3: w {f x|xA Y}.
Apply ReplE_impred (A Y) f w H3 to the current goal.
Let x be given.
Assume H4: x A Y.
Assume H5: w = f x.
Apply setminusE A Y x H4 to the current goal.
Assume H6: x A.
Assume H7: x Y.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6.
We will prove (if x Y then inv B g x else f x) = w.
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.
Assume H3: w {f x|xA Y}.
We prove the intermediate claim Lgw: g w Y.
rewrite the current goal using H2 (from right to left).
We will prove g w F Y.
We will prove g w {g y|yB {f x|xA Y}}.
Apply ReplI to the current goal.
Apply setminusI to the current goal.
We will prove w B.
An exact proof term for the current goal is Hw.
We will prove w {f x|xA 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.
We will prove g w A.
Apply Hg1 to the current goal.
An exact proof term for the current goal is Hw.
We will prove (if g w Y then inv B g (g w) else f (g w)) = w.
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
Theorem. (PigeonHole_nat)
∀n, nat_p n∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j)
Proof:
Apply nat_ind (λn ⇒ ∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j)) to the current goal.
We will prove ∀f : setset, (∀i1, f i 0)¬ (∀i j1, f i = f ji = j).
Let f be given.
Assume H1.
Apply EmptyE (f 0) (H1 0 In_0_1) to the current goal.
Let n be given.
Assume Hn: nat_p n.
Assume IH: ∀f : setset, (∀iordsucc n, f i n)¬ (∀i jordsucc n, f i = f ji = j).
Let f be given.
Assume H1: ∀iordsucc (ordsucc n), f i ordsucc n.
Assume H2: ∀i jordsucc (ordsucc n), f i = f ji = j.
Apply xm (∃iordsucc (ordsucc n), f i = n) to the current goal.
Assume H3.
Apply H3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Assume Hk1: k ordsucc (ordsucc n).
Assume Hk2: f k = n.
Set f' to be the term λi : setif k i then f (ordsucc i) else f i.
Apply IH f' to the current goal.
We will prove ∀iordsucc n, f' i n.
Let i be given.
Assume Hi: i ordsucc n.
Apply xm (k i) to the current goal.
Assume H4: k i.
We will prove (if k i then f (ordsucc i) else f i) n.
rewrite the current goal using If_i_1 (k i) (f (ordsucc i)) (f i) H4 (from left to right).
We will prove f (ordsucc i) n.
We prove the intermediate claim L1: ordsucc i ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hi.
Apply ordsuccE n (f (ordsucc i)) (H1 (ordsucc i) L1) to the current goal.
Assume H5: f (ordsucc i) n.
An exact proof term for the current goal is H5.
Assume H5: f (ordsucc i) = n.
We will prove False.
Apply In_irref i to the current goal.
We will prove i i.
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).
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H4 i L3.
Assume H4: ¬ (k i).
We will prove (if k i then f (ordsucc i) else f i) n.
rewrite the current goal using If_i_0 (k i) (f (ordsucc i)) (f i) H4 (from left to right).
We will prove f i n.
Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.
Assume H5: f i n.
An exact proof term for the current goal is H5.
Assume H5: f i = n.
We will prove False.
Apply H4 to the current goal.
We will prove k i.
We prove the intermediate claim L2: k = 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 ordsuccI1 (ordsucc n) i Hi.
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 jordsucc n, f' i = f' ji = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
We will prove (if k i then f (ordsucc i) else f i) = (if k j then f (ordsucc j) else f j)i = j.
We prove the intermediate claim Li1: i ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Li2: ordsucc i ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Lj1: j ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
We prove the intermediate claim Lj2: ordsucc j ordsucc (ordsucc n).
Apply nat_ordsucc_in_ordsucc to the current goal.
Apply nat_ordsucc to the current goal.
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.
Assume H4: k i.
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.
Assume H5: k j.
rewrite the current goal using If_i_1 (k j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f (ordsucc i) = f (ordsucc j)i = j.
Assume H6.
Apply ordsucc_inj to the current goal.
We will prove ordsucc i = ordsucc j.
An exact proof term for the current goal is H2 (ordsucc i) Li2 (ordsucc j) Lj2 H6.
Assume H5: ¬ (k j).
rewrite the current goal using If_i_0 (k j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f (ordsucc i) = f ji = j.
Assume H6.
We will prove False.
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.
Assume Hx: x k.
Apply ordsuccI1 to the current goal.
Apply H4 to the current goal.
An exact proof term for the current goal is Hx.
Assume H4: ¬ (k i).
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.
Assume H5: k j.
rewrite the current goal using If_i_1 (k j) (f (ordsucc j)) (f j) H5 (from left to right).
We will prove f i = f (ordsucc j)i = j.
Assume H6.
We will prove False.
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.
Assume Hx: x k.
Apply ordsuccI1 to the current goal.
Apply H5 to the current goal.
An exact proof term for the current goal is Hx.
Assume H5: ¬ (k j).
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 ji = 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.
Assume H3: ¬ (∃iordsucc (ordsucc n), f i = n).
Apply IH f to the current goal.
We will prove ∀iordsucc n, f i n.
Let i be given.
Assume Hi: i ordsucc n.
Apply ordsuccE n (f i) (H1 i (ordsuccI1 (ordsucc n) i Hi)) to the current goal.
Assume Hfi: f i n.
An exact proof term for the current goal is Hfi.
Assume Hfi: f i = n.
Apply H3 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI1 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 jordsucc n, f i = f ji = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Apply H2 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
Theorem. (PigeonHole_nat_bij)
∀n, nat_p n∀f : setset, (∀in, f i n)(∀i jn, f i = f ji = j)bij n n f
Proof:
Let n be given.
Assume Hn.
Let f be given.
Assume Hf1 Hf2.
We will prove (∀in, f i n) (∀i jn, f i = f ji = j) (∀jn, ∃in, 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.
Assume Hj: j n.
Apply dneg to the current goal.
Assume H1: ¬ ∃in, f i = j.
Set f' to be the term λi : setif i = n then j else f i.
Apply PigeonHole_nat n Hn f' to the current goal.
We will prove ∀iordsucc n, f' i n.
Let i be given.
Assume Hi.
We will prove (if i = n then j else f i) n.
Apply xm (i = n) to the current goal.
Assume H1: i = n.
rewrite the current goal using If_i_1 (i = n) j (f i) H1 (from left to right).
We will prove j n.
An exact proof term for the current goal is Hj.
Assume H1: i n.
rewrite the current goal using If_i_0 (i = n) j (f i) H1 (from left to right).
We will prove f i n.
Apply Hf1 to the current goal.
Apply ordsuccE n i Hi to the current goal.
Assume H2: i n.
An exact proof term for the current goal is H2.
Assume H2: i = n.
Apply H1 H2 to the current goal.
We will prove ∀i kordsucc n, f' i = f' ki = k.
Let i be given.
Assume Hi.
Let k be given.
Assume Hk.
We prove the intermediate claim Li: i ni n.
Assume Hin: 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 nk n.
Assume Hkn: 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.
We will prove (if i = n then j else f i) = (if k = n then j else f k)i = k.
Apply xm (i = n) to the current goal.
Assume H2: i = n.
Apply xm (k = n) to the current goal.
Assume H3: k = n.
Assume _.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is H2.
Assume H3: k n.
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).
Assume H4: j = f k.
Apply H1 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
We will prove k n.
An exact proof term for the current goal is Lk H3.
Use symmetry.
An exact proof term for the current goal is H4.
Assume H2: i n.
Apply xm (k = n) to the current goal.
Assume H3: k = n.
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).
Assume H4: f i = j.
Apply H1 to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
We will prove i n.
An exact proof term for the current goal is Li H2.
An exact proof term for the current goal is H4.
Assume H3: k n.
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 ki = k.
Apply Hf2 to the current goal.
We will prove i n.
An exact proof term for the current goal is Li H2.
We will prove k n.
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 setprop.
Theorem. (finite_ind)
∀p : setprop, p Empty(∀X y, finite Xy Xp Xp (X {y}))∀X, finite Xp X
Proof:
Let p be given.
Assume H1 H2.
We prove the intermediate claim L1: ∀n, nat_p n∀X, equip X np X.
Apply nat_ind to the current goal.
Let X be given.
Assume H3: equip X 0.
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.
Assume IHn: ∀X, equip X np X.
Let X be given.
Assume H3: equip X (ordsucc n).
Apply equip_sym X (ordsucc n) H3 to the current goal.
Let f be given.
Assume Hf: bij (ordsucc n) X f.
Apply bijE (ordsucc n) X f Hf to the current goal.
Assume Hf1: ∀iordsucc n, f i X.
Assume Hf2: ∀i jordsucc n, f i = f ji = j.
Assume Hf3: ∀xX, ∃iordsucc n, f i = x.
Set Z to be the term {f i|in}.
Set y to be the term f n.
We prove the intermediate claim L1a: X = Z {y}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x X.
Apply Hf3 x Hx to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ordsucc n.
Assume H4: f i = x.
Apply ordsuccE n i Hi to the current goal.
Assume H5: i n.
Apply binunionI1 to the current goal.
We will prove x Z.
rewrite the current goal using H4 (from right to left).
We will prove f i Z.
Apply ReplI to the current goal.
An exact proof term for the current goal is H5.
Assume H5: i = n.
Apply binunionI2 to the current goal.
We will prove x {y}.
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.
Assume Hx: x Z {y}.
Apply binunionE Z {y} x Hx to the current goal.
Assume H4: x Z.
Apply ReplE_impred n f x H4 to the current goal.
Let i be given.
Assume Hi: i n.
Assume H5: x = f i.
We will prove x X.
rewrite the current goal using H5 (from left to right).
We will prove f i X.
An exact proof term for the current goal is Hf1 i (ordsuccI1 n i Hi).
Assume H4: x {y}.
rewrite the current goal using SingE y x H4 (from left to right).
We will prove f n X.
An exact proof term for the current goal is Hf1 n (ordsuccI2 n).
We prove the intermediate claim L1b: equip Z n.
Apply equip_sym to the current goal.
We will prove ∃f : setset, 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|in}.
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.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
Apply ReplE' to the current goal.
Let i be given.
Assume Hi: i n.
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.
Use reflexivity.
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 will prove finite Z.
We will prove ∃nω, equip Z n.
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.
We will prove y Z.
Assume H4: y Z.
Apply ReplE_impred n f y H4 to the current goal.
Let i be given.
Assume Hi: i n.
Assume H5: y = f i.
Apply In_irref n to the current goal.
We will prove n n.
rewrite the current goal using Hf2 n (ordsuccI2 n) i (ordsuccI1 n i Hi) H5 (from left to right) at position 1.
We will prove i n.
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.
Assume Hn: n ω.
Assume H4: equip X n.
An exact proof term for the current goal is L1 n (omega_nat_p n Hn) X H4.
Theorem. (finite_Empty)
Proof:
We will prove ∃nω, equip 0 n.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is nat_p_omega 0 nat_0.
Apply equip_ref to the current goal.
Theorem. (adjoin_finite)
∀X y, finite Xfinite (X {y})
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.
Assume Hn: n ω.
Assume H2: equip X n.
Apply equip_sym X n H2 to the current goal.
Let f be given.
Assume Hf: bij n X f.
Apply bijE n X f Hf to the current goal.
Assume Hf1: ∀in, f i X.
Assume Hf2: ∀i jn, f i = f ji = j.
Assume Hf3: ∀xX, ∃in, f i = x.
Apply xm (y X) to the current goal.
Assume H3: y X.
We prove the intermediate claim L1: X {y} = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx.
Apply binunionE X {y} x Hx to the current goal.
Assume H4.
An exact proof term for the current goal is H4.
Assume H4: x {y}.
rewrite the current goal using SingE y x H4 (from left to right).
An exact proof term for the current goal is H3.
Apply binunion_Subq_1 to the current goal.
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H1.
Assume H3: y X.
We will prove ∃mω, equip (X {y}) m.
We use ordsucc n to witness the existential quantifier.
Apply andI to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
We will prove equip (X {y}) (ordsucc n).
Apply equip_sym to the current goal.
We will prove ∃g : setset, bij (ordsucc n) (X {y}) g.
We prove the intermediate claim Lg: ∃g : setset, (∀in, g i = f i) g n = y.
We use (λi : setif 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.
We will prove ∀iordsucc n, g i X {y}.
Let i be given.
Assume Hi.
Apply ordsuccE n i Hi to the current goal.
Assume H4: i n.
Apply binunionI1 to the current goal.
rewrite the current goal using Hg1 i H4 (from left to right).
We will prove f i X.
An exact proof term for the current goal is Hf1 i H4.
Assume H4: i = n.
Apply binunionI2 to the current goal.
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 jordsucc n, g i = g ji = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Apply ordsuccE n i Hi to the current goal.
Assume H4: i n.
rewrite the current goal using Hg1 i H4 (from left to right).
Apply ordsuccE n j Hj to the current goal.
Assume H5: j n.
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.
Assume H5: j = n.
rewrite the current goal using H5 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Assume H6: f i = y.
We will prove False.
Apply H3 to the current goal.
We will prove y X.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hf1 i H4.
Assume H4: i = n.
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.
Assume H5: j n.
rewrite the current goal using Hg1 j H5 (from left to right).
Assume H6: y = f j.
We will prove False.
Apply H3 to the current goal.
We will prove y X.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hf1 j H5.
Assume H5: j = n.
rewrite the current goal using H5 (from left to right).
Assume _.
We will prove n = n.
Use reflexivity.
We will prove ∀xX {y}, ∃iordsucc n, g i = x.
Let x be given.
Assume Hx.
Apply binunionE X {y} x Hx to the current goal.
Assume H4: x X.
Apply Hf3 x H4 to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i n.
Assume H5: f i = x.
We use i to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove g i = x.
rewrite the current goal using Hg1 i Hi (from left to right).
An exact proof term for the current goal is H5.
Assume H4: x {y}.
We use n to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI2 to the current goal.
We will prove g n = x.
rewrite the current goal using SingE y x H4 (from left to right).
An exact proof term for the current goal is Hg2.
Theorem. (binunion_finite)
∀X, finite X∀Y, finite Yfinite (X Y)
Proof:
Let X be given.
Assume HX.
Apply finite_ind to the current goal.
We will prove finite (X 0).
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.
Assume HY: finite Y.
Assume Hz: z Y.
Assume IH: finite (X Y).
We will prove finite (X (Y {z})).
rewrite the current goal using binunion_asso (from left to right).
We will prove finite ((X Y) {z}).
Apply adjoin_finite to the current goal.
An exact proof term for the current goal is IH.
Theorem. (famunion_nat_finite)
∀X : setset, ∀n, nat_p n(∀in, finite (X i))finite (inX i)
Proof:
Let X be given.
Apply nat_ind to the current goal.
Assume _.
We will prove finite (i0X i).
rewrite the current goal using famunion_Empty (from left to right).
An exact proof term for the current goal is finite_Empty.
Let n be given.
Assume Hn.
Assume IHn: (∀in, finite (X i))finite (inX i).
Assume H1: ∀iordsucc n, finite (X i).
We will prove finite (iordsucc nX i).
We prove the intermediate claim L1: (iordsucc nX i) = (inX i) X n.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z iordsucc nX i.
Apply famunionE_impred (ordsucc n) X z Hz to the current goal.
Let i be given.
Assume Hi: i ordsucc n.
Assume H2: z X i.
Apply ordsuccE n i Hi to the current goal.
Assume H3: i n.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is famunionI n X i z H3 H2.
Assume H3: i = n.
Apply binunionI2 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H2.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz.
Apply famunionE_impred n X z Hz to the current goal.
Let i be given.
Assume Hi: i n.
Assume H2: z X i.
Apply famunionI (ordsucc n) X i z to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is H2.
Assume Hz.
Apply famunionI (ordsucc n) X n z to the current goal.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is Hz.
rewrite the current goal using L1 (from left to right).
We will prove finite ((inX i) X n).
Apply binunion_finite to the current goal.
Apply IHn to the current goal.
Let i be given.
Assume Hi: i n.
Apply H1 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply H1 n to the current goal.
Apply ordsuccI2 to the current goal.
Theorem. (Subq_finite)
∀X, finite X∀Y, Y Xfinite Y
Proof:
Apply finite_ind to the current goal.
Let Y be given.
Assume H1: Y 0.
We will prove finite Y.
rewrite the current goal using Empty_Subq_eq Y H1 (from left to right).
An exact proof term for the current goal is finite_Empty.
Let X and z be given.
Assume HX: finite X.
Assume Hz: z X.
Assume IH: ∀Y, Y Xfinite Y.
Let Y be given.
Assume H1: Y X {z}.
We will prove finite Y.
Apply xm (z Y) to the current goal.
Assume H2: z Y.
We prove the intermediate claim L1: Y = (Y {z}) {z}.
Apply set_ext to the current goal.
Let w be given.
Assume Hw: w Y.
Apply xm (w {z}) to the current goal.
Assume H3: w {z}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H3.
Assume H3: w {z}.
Apply binunionI1 to the current goal.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw: w (Y {z}) {z}.
Apply binunionE (Y {z}) {z} w Hw to the current goal.
Assume H3: w Y {z}.
An exact proof term for the current goal is setminusE1 Y {z} w H3.
Assume H3: w {z}.
We will prove w Y.
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 adjoin_finite to the current goal.
We will prove finite (Y {z}).
Apply IH to the current goal.
Let y be given.
Assume Hy: y Y {z}.
Apply setminusE Y {z} y Hy to the current goal.
Assume Hy1: y Y.
Assume Hy2: y {z}.
We will prove y X.
Apply binunionE X {z} y (H1 y Hy1) to the current goal.
Assume H3: y X.
An exact proof term for the current goal is H3.
Assume H3: y {z}.
We will prove False.
Apply Hy2 to the current goal.
An exact proof term for the current goal is H3.
Assume H2: z Y.
Apply IH to the current goal.
Let y be given.
Assume Hy: y Y.
We will prove y X.
Apply binunionE X {z} y (H1 y Hy) to the current goal.
Assume H3: y X.
An exact proof term for the current goal is H3.
Assume H3: y {z}.
We will prove False.
Apply H2 to the current goal.
We will prove z Y.
rewrite the current goal using SingE z y H3 (from right to left).
An exact proof term for the current goal is Hy.
Theorem. (TransSet_In_ordsucc_Subq)
∀x y, TransSet yx ordsucc yx y
Proof:
Let x and y be given.
Assume H1 H2.
Apply ordsuccE y x H2 to the current goal.
Assume H3: x y.
An exact proof term for the current goal is H1 x H3.
Assume H3: x = y.
rewrite the current goal using H3 (from left to right).
Apply Subq_ref to the current goal.
Theorem. (exandE_i)
∀P Q : setprop, (∃x, P x Q x)∀r : prop, (∀x, P xQ xr)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 : (setset)prop, (∃x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)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 : (setsetset)prop, (∃x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)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 : (setsetsetset)prop, (∃x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)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 : (setset)prop
Definition. We define Descr_ii to be λx : setEps_i (λy ⇒ ∀h : setset, P hh x = y) of type setset.
Hypothesis Pex : ∃f : setset, P f
Hypothesis Puniq : ∀f g : setset, P fP gf = 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 = Descr_ii x.
We will prove f x = Eps_i (λy ⇒ ∀h : setset, P hh x = y).
We prove the intermediate claim L2: ∀h : setset, P hh 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 : setset, P hh x = Descr_ii x.
An exact proof term for the current goal is Eps_i_ax (λy ⇒ ∀h : setset, P hh 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 : (setsetset)prop
Definition. We define Descr_iii to be λx y : setEps_i (λz ⇒ ∀h : setsetset, P hh x y = z) of type setsetset.
Hypothesis Pex : ∃f : setsetset, P f
Hypothesis Puniq : ∀f g : setsetset, P fP gf = 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 (setset) 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 = Descr_iii x y.
We will prove f x y = Eps_i (λz ⇒ ∀h : setsetset, P hh x y = z).
We prove the intermediate claim L2: ∀h : setsetset, P hh 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 : setsetset, P hh x y = Descr_iii x y.
An exact proof term for the current goal is Eps_i_ax (λz ⇒ ∀h : setsetset, P hh 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
Variable P : Vo 1prop
Definition. We define Descr_Vo1 to be λx : set∀h : setprop, P hh x of type Vo 1.
Hypothesis Pex : ∃f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P fP gf = 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.
We will prove f x = Descr_Vo1 x.
Apply prop_ext_2 to the current goal.
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.
Assume H1: Descr_Vo1 x.
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 : setset
Definition. We define If_ii to be λx ⇒ if p then f x else g x of type setset.
Proof:
Assume H1.
Apply func_ext set set to the current goal.
Let x be given.
We will prove If_ii x = f x.
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.
We will prove If_ii x = g x.
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 : setsetset
Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type setsetset.
Proof:
Assume H1.
Apply func_ext set (setset) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
We will prove If_iii x y = f x y.
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 (setset) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
We will prove If_iii x y = g x y.
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(setset)set
Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : setsetprop, (∀X : set, ∀f : setset, (∀xX, R x (f x))R X (F X f))R X Y of type setsetprop.
Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type setset.
Theorem. (In_rec_i_G_c)
∀X : set, ∀f : setset, (∀xX, In_rec_i_G x (f x))In_rec_i_G X (F X f)
Proof:
Let X of type set be given.
Let f of type setset be given.
Assume H1: ∀xX, In_rec_i_G x (f x).
We will prove In_rec_i_G X (F X f).
Let R of type setsetprop be given.
Assume H2: ∀X : set, ∀f : setset, (∀xX, R x (f x))R X (F X f).
We will prove R X (F X f).
Apply (H2 X f) to the current goal.
We will prove ∀xX, R x (f x).
Let x of type set be given.
Assume H3: x X.
We will prove R x (f x).
An exact proof term for the current goal is (H1 x H3 R H2).
Theorem. (In_rec_i_G_inv)
∀X : set, ∀Y : set, In_rec_i_G X Y∃f : setset, (∀xX, In_rec_i_G x (f x)) Y = F X f
Proof:
Let X and Y be given.
Assume H1: In_rec_i_G X Y.
Set R to be the term (λX : setλY : set∃f : setset, (∀xX, In_rec_i_G x (f x)) Y = F X f).
Apply (H1 R) to the current goal.
We will prove ∀Z : set, ∀g : setset, (∀zZ, R z (g z))R Z (F Z g).
Let Z and g be given.
Assume IH: ∀zZ, ∃f : setset, (∀xz, In_rec_i_G x (f x)) g z = F z f.
We will prove ∃f : setset, (∀xZ, 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.
Assume H2: z Z.
Apply (exandE_ii (λf ⇒ ∀xz, In_rec_i_G x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.
Let f of type setset be given.
Assume H3: ∀xz, In_rec_i_G x (f x).
Assume H4: g z = F z f.
We will prove In_rec_i_G z (g z).
rewrite the current goal using H4 (from left to right).
We will prove In_rec_i_G z (F z f).
An exact proof term for the current goal is (In_rec_i_G_c z f H3).
Use reflexivity.
Hypothesis Fr : ∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Theorem. (In_rec_i_G_f)
∀X : set, ∀Y Z : set, In_rec_i_G X YIn_rec_i_G X ZY = Z
Proof:
Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀xX, ∀y z : set, In_rec_i_G x yIn_rec_i_G x zy = z.
Let Y and Z be given.
Assume H1: In_rec_i_G X Y.
Assume H2: In_rec_i_G X Z.
We will prove Y = Z.
We prove the intermediate claim L1: ∃f : setset, (∀xX, In_rec_i_G x (f x)) Y = F X f.
An exact proof term for the current goal is (In_rec_i_G_inv X Y H1).
We prove the intermediate claim L2: ∃f : setset, (∀xX, In_rec_i_G x (f x)) Z = F X f.
An exact proof term for the current goal is (In_rec_i_G_inv X Z H2).
Apply (exandE_ii (λf ⇒ ∀xX, In_rec_i_G x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.
Let g be given.
Assume H3: ∀xX, In_rec_i_G x (g x).
Assume H4: Y = F X g.
Apply (exandE_ii (λf ⇒ ∀xX, In_rec_i_G x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.
Let h be given.
Assume H5: ∀xX, In_rec_i_G x (h x).
Assume H6: Z = F X h.
We will prove Y = Z.
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 ∀xX, g x = h x.
Let x be given.
Assume H7: x X.
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.
Assume IH: ∀xX, In_rec_i_G x (In_rec_i x).
We will prove In_rec_i_G X (In_rec_i X).
We will prove In_rec_i_G X (Eps_i (In_rec_i_G X)).
Apply (Eps_i_ax (In_rec_i_G X) (F X In_rec_i)) to the current goal.
We will prove In_rec_i_G X (F X In_rec_i).
An exact proof term for the current goal is (In_rec_i_G_c X In_rec_i IH).
Proof:
Let X and R be given.
Assume H1: ∀X : set, ∀f : setset, (∀xX, R x (f x))R X (F X f).
Apply (H1 X In_rec_i) to the current goal.
Let x be given.
Assume _.
An exact proof term for the current goal is (In_rec_i_G_In_rec_i x R H1).
Proof:
An exact proof term for the current goal is (λX : setIn_rec_i_G_f X (In_rec_i X) (F X In_rec_i) (In_rec_i_G_In_rec_i X) (In_rec_i_G_In_rec_i_d X)).
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set(set(setset))(setset)
Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set(setset)prop, (∀X : set, ∀f : set(setset), (∀xX, R x (f x))R X (F X f))R X Y of type set(setset)prop.
Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set(setset).
Theorem. (In_rec_G_ii_c)
∀X : set, ∀f : set(setset), (∀xX, In_rec_G_ii x (f x))In_rec_G_ii X (F X f)
Proof:
Let X of type set be given.
Let f of type set(setset) be given.
Assume H1: ∀xX, In_rec_G_ii x (f x).
We will prove In_rec_G_ii X (F X f).
Let R of type set(setset)prop be given.
Assume H2: ∀X : set, ∀f : set(setset), (∀xX, R x (f x))R X (F X f).
We will prove R X (F X f).
Apply (H2 X f) to the current goal.
We will prove ∀xX, R x (f x).
Let x of type set be given.
Assume H3: x X.
We will prove R x (f x).
An exact proof term for the current goal is (H1 x H3 R H2).
Theorem. (In_rec_G_ii_inv)
∀X : set, ∀Y : (setset), In_rec_G_ii X Y∃f : set(setset), (∀xX, In_rec_G_ii x (f x)) Y = F X f
Proof:
Let X and Y be given.
Assume H1: In_rec_G_ii X Y.
Set R to be the term (λX : setλY : (setset)∃f : set(setset), (∀xX, 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(setset), (∀zZ, R z (g z))R Z (F Z g).
Let Z and g be given.
Assume IH: ∀zZ, ∃f : set(setset), (∀xz, In_rec_G_ii x (f x)) g z = F z f.
We will prove ∃f : set(setset), (∀xZ, 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.
Assume H2: z Z.
Apply (exandE_iii (λf ⇒ ∀xz, In_rec_G_ii x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.
Let f of type set(setset) be given.
Assume H3: ∀xz, In_rec_G_ii x (f x).
Assume H4: g z = F z f.
We will prove In_rec_G_ii z (g z).
rewrite the current goal using H4 (from left to right).
We will prove In_rec_G_ii z (F z f).
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(setset), (∀xX, g x = h x)F X g = F X h
Theorem. (In_rec_G_ii_f)
∀X : set, ∀Y Z : (setset), In_rec_G_ii X YIn_rec_G_ii X ZY = Z
Proof:
Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀xX, ∀y z : (setset), In_rec_G_ii x yIn_rec_G_ii x zy = z.
Let Y and Z be given.
Assume H1: In_rec_G_ii X Y.
Assume H2: In_rec_G_ii X Z.
We will prove Y = Z.
We prove the intermediate claim L1: ∃f : set(setset), (∀xX, In_rec_G_ii x (f x)) Y = F X f.
An exact proof term for the current goal is (In_rec_G_ii_inv X Y H1).
We prove the intermediate claim L2: ∃f : set(setset), (∀xX, In_rec_G_ii x (f x)) Z = F X f.
An exact proof term for the current goal is (In_rec_G_ii_inv X Z H2).
Apply (exandE_iii (λf ⇒ ∀xX, In_rec_G_ii x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.
Let g be given.
Assume H3: ∀xX, In_rec_G_ii x (g x).
Assume H4: Y = F X g.
Apply (exandE_iii (λf ⇒ ∀xX, In_rec_G_ii x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.
Let h be given.
Assume H5: ∀xX, In_rec_G_ii x (h x).
Assume H6: Z = F X h.
We will prove Y = Z.
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 ∀xX, g x = h x.
Let x be given.
Assume H7: x X.
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.
Assume IH: ∀xX, In_rec_G_ii x (In_rec_ii x).
We will prove In_rec_G_ii X (In_rec_ii X).
We will prove In_rec_G_ii X (Descr_ii (In_rec_G_ii X)).
Apply (Descr_ii_prop (In_rec_G_ii X)) to the current goal.
We use (F X In_rec_ii) to witness the existential quantifier.
We will prove In_rec_G_ii X (F X In_rec_ii).
An exact proof term for the current goal is (In_rec_G_ii_c X In_rec_ii IH).
An exact proof term for the current goal is In_rec_G_ii_f X.
Proof:
Let X and R be given.
Assume H1: ∀X : set, ∀f : set(setset), (∀xX, R x (f x))R X (F X f).
Apply (H1 X In_rec_ii) to the current goal.
Let x be given.
Assume _.
An exact proof term for the current goal is (In_rec_G_ii_In_rec_ii x R H1).
Proof:
An exact proof term for the current goal is (λX : setIn_rec_G_ii_f X (In_rec_ii X) (F X In_rec_ii) (In_rec_G_ii_In_rec_ii X) (In_rec_G_ii_In_rec_ii_d X)).
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set(set(setsetset))(setsetset)
Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set(setsetset)prop, (∀X : set, ∀f : set(setsetset), (∀xX, R x (f x))R X (F X f))R X Y of type set(setsetset)prop.
Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set(setsetset).
Theorem. (In_rec_G_iii_c)
∀X : set, ∀f : set(setsetset), (∀xX, In_rec_G_iii x (f x))In_rec_G_iii X (F X f)
Proof:
Let X of type set be given.
Let f of type set(setsetset) be given.
Assume H1: ∀xX, In_rec_G_iii x (f x).
We will prove In_rec_G_iii X (F X f).
Let R of type set(setsetset)prop be given.
Assume H2: ∀X : set, ∀f : set(setsetset), (∀xX, R x (f x))R X (F X f).
We will prove R X (F X f).
Apply (H2 X f) to the current goal.
We will prove ∀xX, R x (f x).
Let x of type set be given.
Assume H3: x X.
We will prove R x (f x).
An exact proof term for the current goal is (H1 x H3 R H2).
Theorem. (In_rec_G_iii_inv)
∀X : set, ∀Y : (setsetset), In_rec_G_iii X Y∃f : set(setsetset), (∀xX, In_rec_G_iii x (f x)) Y = F X f
Proof:
Let X and Y be given.
Assume H1: In_rec_G_iii X Y.
Set R to be the term (λX : setλY : (setsetset)∃f : set(setsetset), (∀xX, 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(setsetset), (∀zZ, R z (g z))R Z (F Z g).
Let Z and g be given.
Assume IH: ∀zZ, ∃f : set(setsetset), (∀xz, In_rec_G_iii x (f x)) g z = F z f.
We will prove ∃f : set(setsetset), (∀xZ, 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.
Assume H2: z Z.
Apply (exandE_iiii (λf ⇒ ∀xz, In_rec_G_iii x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.
Let f of type set(setsetset) be given.
Assume H3: ∀xz, In_rec_G_iii x (f x).
Assume H4: g z = F z f.
We will prove In_rec_G_iii z (g z).
rewrite the current goal using H4 (from left to right).
We will prove In_rec_G_iii z (F z f).
An exact proof term for the current goal is (In_rec_G_iii_c z f H3).
An exact proof term for the current goal is (λq H ⇒ H).
Hypothesis Fr : ∀X : set, ∀g h : set(setsetset), (∀xX, g x = h x)F X g = F X h
Theorem. (In_rec_G_iii_f)
∀X : set, ∀Y Z : (setsetset), In_rec_G_iii X YIn_rec_G_iii X ZY = Z
Proof:
Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀xX, ∀y z : (setsetset), In_rec_G_iii x yIn_rec_G_iii x zy = z.
Let Y and Z be given.
Assume H1: In_rec_G_iii X Y.
Assume H2: In_rec_G_iii X Z.
We will prove Y = Z.
We prove the intermediate claim L1: ∃f : set(setsetset), (∀xX, In_rec_G_iii x (f x)) Y = F X f.
An exact proof term for the current goal is (In_rec_G_iii_inv X Y H1).
We prove the intermediate claim L2: ∃f : set(setsetset), (∀xX, In_rec_G_iii x (f x)) Z = F X f.
An exact proof term for the current goal is (In_rec_G_iii_inv X Z H2).
Apply (exandE_iiii (λf ⇒ ∀xX, In_rec_G_iii x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.
Let g be given.
Assume H3: ∀xX, In_rec_G_iii x (g x).
Assume H4: Y = F X g.
Apply (exandE_iiii (λf ⇒ ∀xX, In_rec_G_iii x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.
Let h be given.
Assume H5: ∀xX, In_rec_G_iii x (h x).
Assume H6: Z = F X h.
We will prove Y = Z.
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 ∀xX, g x = h x.
Let x be given.
Assume H7: x X.
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.
Assume IH: ∀xX, In_rec_G_iii x (In_rec_iii x).
We will prove In_rec_G_iii X (In_rec_iii X).
We will prove In_rec_G_iii X (Descr_iii (In_rec_G_iii X)).
Apply (Descr_iii_prop (In_rec_G_iii X)) to the current goal.
We use (F X In_rec_iii) to witness the existential quantifier.
We will prove In_rec_G_iii X (F X In_rec_iii).
An exact proof term for the current goal is (In_rec_G_iii_c X In_rec_iii IH).
An exact proof term for the current goal is In_rec_G_iii_f X.
Proof:
Let X and R be given.
Assume H1: ∀X : set, ∀f : set(setsetset), (∀xX, R x (f x))R X (F X f).
Apply (H1 X In_rec_iii) to the current goal.
Let x be given.
Assume _.
An exact proof term for the current goal is (In_rec_G_iii_In_rec_iii x R H1).
Proof:
An exact proof term for the current goal is (λX : setIn_rec_G_iii_f X (In_rec_iii X) (F X In_rec_iii) (In_rec_G_iii_In_rec_iii X) (In_rec_G_iii_In_rec_iii_d X)).
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)setλn g ⇒ if n n then f ( n) (g ( n)) else z
Definition. We define nat_primrec to be In_rec_i F of type setset.
Theorem. (nat_primrec_r)
∀X : set, ∀g h : setset, (∀xX, g x = h x)F X g = F X h
Proof:
Let X, g and h be given.
Assume H1: ∀xX, g x = h x.
We will prove F X g = F X h.
Apply xm ( X X) to the current goal.
Assume H2: ( X X).
We will prove (if X X then f ( X) (g ( X)) else z) = (if X X then f ( X) (h ( X)) else z).
rewrite the current goal using (H1 ( X) H2) (from left to right).
We will prove (if X X then f ( X) (h ( X)) else z) = (if X X then f ( X) (h ( X)) else z).
An exact proof term for the current goal is (λq H ⇒ H).
Assume H2: ¬ ( X X).
We will prove (if X X then f ( X) (g ( X)) else z) = (if X X then f ( X) (h ( X)) else z).
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.
Proof:
We will prove (In_rec_i F 0 = z).
rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right).
We will prove F 0 (In_rec_i F) = z.
We will prove (if 0 0 then f ( 0) (In_rec_i F ( 0)) else z) = z.
An exact proof term for the current goal is (If_i_0 ( 0 0) (f ( 0) (In_rec_i F ( 0))) z (EmptyE ( 0))).
Proof:
Let n be given.
Assume Hn: nat_p n.
We will prove (In_rec_i F (ordsucc n) = f n (In_rec_i F n)).
rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right) at position 1.
We will prove F (ordsucc n) (In_rec_i F) = f n (In_rec_i F n).
We will prove (if (ordsucc n) ordsucc n then f ( (ordsucc n)) (In_rec_i F ( (ordsucc n))) else z) = f n (In_rec_i F n).
rewrite the current goal using (Union_ordsucc_eq n Hn) (from left to right).
We will prove (if n ordsucc n then f n (In_rec_i F n) else z) = f n (In_rec_i F n).
An exact proof term for the current goal is (If_i_1 (n ordsucc n) (f n (In_rec_i F n)) z (ordsuccI2 n)).
End of Section NatRec
Beginning of Section NatArith
Definition. We define add_nat to be λn m : setnat_primrec n (λ_ r ⇒ ordsucc r) m of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Theorem. (add_nat_0R)
∀n : set, n + 0 = n
Proof:
Let n be given.
An exact proof term for the current goal is (nat_primrec_0 n (λ_ r ⇒ ordsucc r)).
Theorem. (add_nat_SR)
∀n m : set, nat_p mn + ordsucc m = ordsucc (n + m)
Proof:
Let n and m be given.
Assume Hm.
An exact proof term for the current goal is (nat_primrec_S n (λ_ r ⇒ ordsucc r) m Hm).
Theorem. (add_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n + m)
Proof:
Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove nat_p (n + 0).
rewrite the current goal using (add_nat_0R n) (from left to right).
We will prove nat_p n.
An exact proof term for the current goal is Hn.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: nat_p (n + m).
We will prove nat_p (n + ordsucc m).
rewrite the current goal using (add_nat_SR n m Hm) (from left to right).
We will prove nat_p (ordsucc (n + m)).
Apply nat_ordsucc to the current goal.
We will prove nat_p (n + m).
An exact proof term for the current goal is IHm.
Proof:
Use symmetry.
We will prove ordsucc 1 = 1 + ordsucc 0.
rewrite the current goal using add_nat_SR 1 0 nat_0 (from left to right).
We will prove ordsucc 1 = ordsucc (1 + 0).
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).
Theorem. (add_nat_0L)
∀m : set, nat_p m0 + m = m
Proof:
Apply nat_ind to the current goal.
We will prove 0 + 0 = 0.
Apply add_nat_0R to the current goal.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: 0 + m = m.
We will prove 0 + ordsucc m = ordsucc m.
rewrite the current goal using (add_nat_SR 0 m Hm) (from left to right).
We will prove ordsucc (0 + m) = ordsucc m.
rewrite the current goal using IHm (from left to right).
Use reflexivity.
Theorem. (add_nat_SL)
∀n : set, nat_p n∀m : set, nat_p mordsucc n + m = ordsucc (n + m)
Proof:
Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove ordsucc n + 0 = ordsucc (n + 0).
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.
Assume Hm: nat_p m.
Assume IHm: ordsucc n + m = ordsucc (n + m).
We will prove ordsucc n + ordsucc m = ordsucc (n + ordsucc m).
rewrite the current goal using (add_nat_SR (ordsucc n) m Hm) (from left to right).
We will prove ordsucc (ordsucc n + m) = ordsucc (n + ordsucc m).
rewrite the current goal using (add_nat_SR n m Hm) (from left to right).
We will prove ordsucc (ordsucc n + m) = ordsucc (ordsucc (n + m)).
rewrite the current goal using IHm (from left to right).
Use reflexivity.
Theorem. (add_nat_com)
∀n : set, nat_p n∀m : set, nat_p mn + m = m + n
Proof:
Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
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.
Assume Hm: nat_p m.
Assume IHm: n + m = m + n.
We will prove n + ordsucc m = ordsucc m + n.
rewrite the current goal using (add_nat_SL m Hm n Hn) (from left to right).
We will prove n + ordsucc m = ordsucc (m + n).
rewrite the current goal using IHm (from right to left).
We will prove n + ordsucc m = ordsucc (n + m).
An exact proof term for the current goal is (add_nat_SR n m Hm).
Theorem. (nat_Subq_add_ex)
∀n, nat_p n∀m, nat_p mn m∃k, nat_p k m = k + n
Proof:
Apply nat_ind to the current goal.
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.
We will prove m = m + 0.
Use symmetry.
An exact proof term for the current goal is add_nat_0R m.
Let n be given.
Assume Hn.
Assume IH: ∀m, nat_p mn m∃k, nat_p k m = k + n.
Apply nat_inv_impred to the current goal.
Assume Hnm: ordsucc n 0.
We will prove False.
Apply EmptyE n to the current goal.
We will prove n 0.
Apply Hnm to the current goal.
Apply ordsuccI2 to the current goal.
Let m be given.
Assume Hm: nat_p m.
Assume Hnm: ordsucc n ordsucc m.
We prove the intermediate claim Lnm: n m.
Apply ordinal_In_Or_Subq m n (nat_p_ordinal m Hm) (nat_p_ordinal n Hn) to the current goal.
Assume H1: m n.
We will prove False.
Apply In_irref (ordsucc m) to the current goal.
Apply Hnm to the current goal.
We will prove ordsucc m ordsucc n.
An exact proof term for the current goal is nat_ordsucc_in_ordsucc n Hn m H1.
Assume H1: n m.
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.
Assume Hk: nat_p k.
Assume H1: m = k + n.
We will prove ∃k, nat_p k ordsucc m = k + ordsucc n.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We will prove ordsucc m = k + ordsucc n.
rewrite the current goal using add_nat_SR k n Hn (from left to right).
We will prove ordsucc m = ordsucc (k + n).
Use f_equal.
An exact proof term for the current goal is H1.
Definition. We define mul_nat to be λn m : setnat_primrec 0 (λ_ r ⇒ n + r) m of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Theorem. (mul_nat_0R)
∀n : set, n * 0 = 0
Proof:
Let n be given.
An exact proof term for the current goal is (nat_primrec_0 0 (λ_ r ⇒ n + r)).
Theorem. (mul_nat_SR)
∀n m : set, nat_p mn * ordsucc m = n + n * m
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).
Theorem. (mul_nat_p)
∀n : set, nat_p n∀m : set, nat_p mnat_p (n * m)
Proof:
Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove nat_p (n * 0).
rewrite the current goal using (mul_nat_0R n) (from left to right).
We will prove nat_p 0.
An exact proof term for the current goal is nat_0.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: nat_p (n * m).
We will prove nat_p (n * ordsucc m).
rewrite the current goal using (mul_nat_SR n m Hm) (from left to right).
We will prove nat_p (n + n * m).
An exact proof term for the current goal is (add_nat_p n Hn (n * m) IHm).
End of Section NatArith
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} {f x|xX}) of type setset.
Theorem. (Inj1_eq)
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Proof:
We prove the intermediate claim L1: ∀X : set, ∀g h : setset, (∀xX, g x = h x){0} {g x|xX} = {0} {h x|xX}.
Let X, g and h be given.
Assume H: ∀xX, g x = h x.
We prove the intermediate claim L1a: {g x|xX} = {h x|xX}.
An exact proof term for the current goal is (ReplEq_ext X g h H).
We will prove {0} {g x|xX} = {0} {h x|xX}.
rewrite the current goal using L1a (from left to right).
Use reflexivity.
An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {0} {f x|xX}) L1).
Theorem. (Inj1I1)
∀X : set, 0 Inj1 X
Proof:
Let X be given.
rewrite the current goal using (Inj1_eq X) (from left to right).
We will prove 0 {0} {Inj1 x|xX}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
Theorem. (Inj1I2)
∀X x : set, x XInj1 x Inj1 X
Proof:
Let X and x be given.
Assume H: x X.
rewrite the current goal using (Inj1_eq X) (from left to right).
We will prove Inj1 x {0} {Inj1 x|xX}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (ReplI X Inj1 x H).
Theorem. (Inj1E)
∀X y : set, y Inj1 Xy = 0 ∃xX, y = Inj1 x
Proof:
Let X and y be given.
rewrite the current goal using (Inj1_eq X) (from left to right).
Assume H1: y {0} {Inj1 x|xX}.
We will prove y = 0 ∃xX, y = Inj1 x.
Apply (binunionE {0} {Inj1 x|xX} y H1) to the current goal.
Assume H2: y {0}.
Apply orIL to the current goal.
An exact proof term for the current goal is (SingE 0 y H2).
Assume H2: y {Inj1 x|xX}.
Apply orIR to the current goal.
We will prove ∃xX, y = Inj1 x.
An exact proof term for the current goal is (ReplE X Inj1 y H2).
Theorem. (Inj1NE1)
∀x : set, Inj1 x 0
Proof:
Let x be given.
Assume H1: Inj1 x = 0.
Apply (EmptyE 0) to the current goal.
We will prove 0 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 Inj1 x.
An exact proof term for the current goal is (Inj1I1 x).
Theorem. (Inj1NE2)
∀x : set, Inj1 x {0}
Proof:
Let x be given.
Assume H1: Inj1 x {0}.
An exact proof term for the current goal is (Inj1NE1 x (SingE 0 (Inj1 x) H1)).
Definition. We define Inj0 to be λX ⇒ {Inj1 x|xX} of type setset.
Theorem. (Inj0I)
∀X x : set, x XInj1 x Inj0 X
Proof:
An exact proof term for the current goal is (λX x H ⇒ ReplI X Inj1 x H).
Theorem. (Inj0E)
∀X y : set, y Inj0 X∃x : set, x X y = Inj1 x
Proof:
An exact proof term for the current goal is (λX y H ⇒ ReplE X Inj1 y H).
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX {0}}) of type setset.
Theorem. (Unj_eq)
∀X : set, Unj X = {Unj x|xX {0}}
Proof:
We prove the intermediate claim L1: ∀X : set, ∀g h : setset, (∀xX, g x = h x){g x|xX {0}} = {h x|xX {0}}.
Let X, g and h be given.
Assume H1: ∀xX, g x = h x.
We will prove {g x|xX {0}} = {h x|xX {0}}.
Apply (ReplEq_ext (X {0}) g h) to the current goal.
Let x be given.
Assume H2: x X {0}.
We will prove g x = h x.
Apply H1 to the current goal.
We will prove x X.
An exact proof term for the current goal is (setminusE1 X {0} x H2).
An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {f x|xX {0}}) L1).
Theorem. (Unj_Inj1_eq)
∀X : set, Unj (Inj1 X) = X
Proof:
Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀xX, Unj (Inj1 x) = x.
We will prove Unj (Inj1 X) = X.
rewrite the current goal using Unj_eq (from left to right).
We will prove {Unj x|xInj1 X {0}} = X.
Apply set_ext to the current goal.
We will prove {Unj x|xInj1 X {0}} X.
Let x be given.
Assume H1: x {Unj x|xInj1 X {0}}.
We will prove x X.
Apply (ReplE_impred (Inj1 X {0}) Unj x H1) to the current goal.
Let y be given.
Assume H2: y Inj1 X {0}.
Assume H3: x = Unj y.
rewrite the current goal using H3 (from left to right).
We will prove Unj y X.
Apply (setminusE (Inj1 X) {0} y H2) to the current goal.
Assume H4: y Inj1 X.
Assume H5: y {0}.
Apply (Inj1E X y H4) to the current goal.
Assume H6: y = 0.
We will prove False.
Apply H5 to the current goal.
rewrite the current goal using H6 (from left to right).
We will prove 0 {0}.
Apply SingI to the current goal.
Assume H6: ∃xX, y = Inj1 x.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ y = Inj1 x) H6) to the current goal.
Let z be given.
Assume H7: z X.
Assume H8: y = Inj1 z.
rewrite the current goal using H8 (from left to right).
We will prove Unj (Inj1 z) X.
rewrite the current goal using (IH z H7) (from left to right).
We will prove z X.
An exact proof term for the current goal is H7.
We will prove X {Unj x|xInj1 X {0}}.
Let x be given.
Assume H1: x X.
We will prove x {Unj x|xInj1 X {0}}.
rewrite the current goal using (IH x H1) (from right to left).
We will prove Unj (Inj1 x) {Unj x|xInj1 X {0}}.
Apply (ReplI (Inj1 X {0}) Unj) to the current goal.
We will prove Inj1 x Inj1 X {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is (Inj1I2 X x H1).
We will prove Inj1 x {0}.
An exact proof term for the current goal is (Inj1NE2 x).
Theorem. (Inj1_inj)
∀X Y : set, Inj1 X = Inj1 YX = Y
Proof:
Let X and Y be given.
Assume H1: Inj1 X = Inj1 Y.
We will prove X = Y.
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.
Theorem. (Unj_Inj0_eq)
∀X : set, Unj (Inj0 X) = X
Proof:
Let X be given.
rewrite the current goal using (Unj_eq (Inj0 X)) (from left to right).
We will prove {Unj x|xInj0 X {0}} = X.
Apply set_ext to the current goal.
We will prove {Unj x|xInj0 X {0}} X.
Let x be given.
Assume H1: x {Unj x|xInj0 X {0}}.
We will prove x X.
Apply (ReplE_impred (Inj0 X {0}) Unj x H1) to the current goal.
Let y be given.
Assume H2: y Inj0 X {0}.
Assume H3: x = Unj y.
Apply (setminusE (Inj0 X) {0} y H2) to the current goal.
Assume H4: y {Inj1 x|xX}.
Assume H5: y {0}.
Apply (ReplE_impred X Inj1 y H4) to the current goal.
Let z be given.
Assume H6: z X.
Assume H7: y = Inj1 z.
We prove the intermediate claim L1: x = z.
rewrite the current goal using H3 (from left to right).
We will prove Unj y = z.
rewrite the current goal using H7 (from left to right).
We will prove Unj (Inj1 z) = z.
An exact proof term for the current goal is (Unj_Inj1_eq z).
We will prove x X.
rewrite the current goal using L1 (from left to right).
We will prove z X.
An exact proof term for the current goal is H6.
We will prove X {Unj x|xInj0 X {0}}.
Let x be given.
Assume H1: x X.
We will prove x {Unj x|xInj0 X {0}}.
rewrite the current goal using (Unj_Inj1_eq x) (from right to left).
We will prove Unj (Inj1 x) {Unj x|xInj0 X {0}}.
Apply (ReplI (Inj0 X {0}) Unj) to the current goal.
We will prove Inj1 x Inj0 X {0}.
Apply setminusI to the current goal.
We will prove Inj1 x {Inj1 x|xX}.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1.
We will prove Inj1 x {0}.
An exact proof term for the current goal is (Inj1NE2 x).
Theorem. (Inj0_inj)
∀X Y : set, Inj0 X = Inj0 YX = Y
Proof:
Let X and Y be given.
Assume H1: Inj0 X = Inj0 Y.
We will prove X = Y.
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.
Theorem. (Inj0_0)
Proof:
An exact proof term for the current goal is (Repl_Empty Inj1).
Theorem. (Inj0_Inj1_neq)
∀X Y : set, Inj0 X Inj1 Y
Proof:
Let X and Y be given.
Assume H1: Inj0 X = Inj1 Y.
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.
Assume H2: x X 0 = Inj1 x.
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.
Definition. We define setsum to be λX Y ⇒ {Inj0 x|xX} {Inj1 y|yY} of type setsetset.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Theorem. (Inj0_setsum)
∀X Y x : set, x XInj0 x X + Y
Proof:
Let X, Y and x be given.
Assume H: x X.
We will prove Inj0 x {Inj0 x|xX} {Inj1 y|yY}.
Apply binunionI1 to the current goal.
We will prove Inj0 x {Inj0 x|xX}.
Apply ReplI to the current goal.
An exact proof term for the current goal is H.
Theorem. (Inj1_setsum)
∀X Y y : set, y YInj1 y X + Y
Proof:
Let X, Y and y be given.
Assume H: y Y.
We will prove Inj1 y {Inj0 x|xX} {Inj1 y|yY}.
Apply binunionI2 to the current goal.
We will prove Inj1 y {Inj1 y|yY}.
Apply ReplI to the current goal.
An exact proof term for the current goal is H.
Theorem. (setsum_Inj_inv)
∀X Y z : set, z X + Y(∃xX, z = Inj0 x) (∃yY, z = Inj1 y)
Proof:
Let X, Y and z be given.
Assume H1: z {Inj0 x|xX} {Inj1 y|yY}.
Apply (binunionE {Inj0 x|xX} {Inj1 y|yY} z H1) to the current goal.
Assume H2: z {Inj0 x|xX}.
Apply orIL to the current goal.
An exact proof term for the current goal is (ReplE X Inj0 z H2).
Assume H2: z {Inj1 y|yY}.
Apply orIR to the current goal.
An exact proof term for the current goal is (ReplE Y Inj1 z H2).
Theorem. (Inj0_setsum_0L)
∀X : set, 0 + X = Inj0 X
Proof:
Let X be given.
Apply set_ext to the current goal.
Let z be given.
Assume H1: z 0 + X.
We will prove z Inj0 X.
Apply (setsum_Inj_inv 0 X z H1) to the current goal.
Assume H2: ∃x0, z = Inj0 x.
Apply (exandE_i (λx ⇒ x 0) (λx ⇒ z = Inj0 x) H2) to the current goal.
Let x be given.
Assume H3: x 0.
We will prove False.
An exact proof term for the current goal is (EmptyE x H3).
Assume H2: ∃xX, z = Inj1 x.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ z = Inj1 x) H2) to the current goal.
Let x be given.
Assume H3: x X.
Assume H4: z = Inj1 x.
rewrite the current goal using H4 (from left to right).
We will prove Inj1 x Inj0 X.
An exact proof term for the current goal is (Inj0I X x H3).
Let z be given.
Assume H1: z Inj0 X.
We will prove z 0 + X.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ z = Inj1 x) (Inj0E X z H1)) to the current goal.
Let x be given.
Assume H2: x X.
Assume H3: z = Inj1 x.
rewrite the current goal using H3 (from left to right).
We will prove Inj1 x 0 + X.
Apply Inj1_setsum to the current goal.
An exact proof term for the current goal is H2.
Theorem. (Subq_1_Sing0)
Proof:
Let x be given.
Assume H1: x 1.
We will prove x {0}.
Apply ordsuccE 0 x H1 to the current goal.
Assume H2: x 0.
We will prove False.
An exact proof term for the current goal is (EmptyE x H2).
Assume H2: x = 0.
rewrite the current goal using H2 (from left to right).
We will prove 0 {0}.
An exact proof term for the current goal is (SingI 0).
Theorem. (Subq_Sing0_1)
Proof:
An exact proof term for the current goal is (λx H1 ⇒ SingE 0 x H1 (λs _ : setx ordsucc s) (ordsuccI2 x)).
Theorem. (eq_1_Sing0)
Proof:
An exact proof term for the current goal is (set_ext 1 (Sing 0) Subq_1_Sing0 Subq_Sing0_1).
Theorem. (Inj1_setsum_1L)
∀X : set, 1 + X = Inj1 X
Proof:
Let X be given.
Apply set_ext to the current goal.
Let z be given.
Assume H1: z 1 + X.
We will prove z Inj1 X.
Apply (setsum_Inj_inv 1 X z H1) to the current goal.
Assume H2: ∃x1, z = Inj0 x.
Apply (exandE_i (λx ⇒ x 1) (λx ⇒ z = Inj0 x) H2) to the current goal.
Let x be given.
Assume H3: x 1.
Assume H4: z = Inj0 x.
rewrite the current goal using H4 (from left to right).
We will prove Inj0 x Inj1 X.
We prove the intermediate claim L1: x = 0.
An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H3)).
rewrite the current goal using L1 (from left to right).
We will prove Inj0 0 Inj1 X.
rewrite the current goal using Inj0_0 (from left to right).
We will prove 0 Inj1 X.
An exact proof term for the current goal is (Inj1I1 X).
Assume H2: ∃xX, z = Inj1 x.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ z = Inj1 x) H2) to the current goal.
Let x be given.
Assume H3: x X.
Assume H4: z = Inj1 x.
rewrite the current goal using H4 (from left to right).
We will prove Inj1 x Inj1 X.
An exact proof term for the current goal is (Inj1I2 X x H3).
Let z be given.
Assume H1: z Inj1 X.
We will prove z 1 + X.
Apply (Inj1E X z H1) to the current goal.
Assume H2: z = 0.
rewrite the current goal using H2 (from left to right).
We will prove 0 1 + X.
rewrite the current goal using Inj0_0 (from right to left) at position 1.
We will prove Inj0 0 1 + X.
Apply Inj0_setsum to the current goal.
We will prove 0 1.
An exact proof term for the current goal is In_0_1.
Assume H2: ∃xX, z = Inj1 x.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ z = Inj1 x) H2) to the current goal.
Let x be given.
Assume H2: x X.
Assume H3: z = Inj1 x.
rewrite the current goal using H3 (from left to right).
We will prove Inj1 x 1 + X.
Apply Inj1_setsum to the current goal.
An exact proof term for the current goal is H2.
Theorem. (nat_setsum1_ordsucc)
∀n : set, nat_p n1 + n = ordsucc n
Proof:
We prove the intermediate claim L: ∀n : set, nat_p nInj1 n = ordsucc n.
Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀mn, Inj1 m = ordsucc m.
We will prove Inj1 n = ordsucc n.
Apply set_ext to the current goal.
We will prove Inj1 n ordsucc n.
Let z be given.
Assume H1: z Inj1 n.
We will prove z ordsucc n.
Apply (Inj1E n z H1) to the current goal.
Assume H2: z = 0.
rewrite the current goal using H2 (from left to right).
We will prove 0 ordsucc n.
An exact proof term for the current goal is (nat_0_in_ordsucc n Hn).
Assume H2: ∃mn, z = Inj1 m.
Apply (exandE_i (λm ⇒ m n) (λm ⇒ z = Inj1 m) H2) to the current goal.
Let m be given.
Assume H3: m n.
Assume H4: z = Inj1 m.
rewrite the current goal using H4 (from left to right).
We will prove Inj1 m ordsucc n.
rewrite the current goal using (IHn m H3) (from left to right).
We will prove ordsucc m ordsucc n.
An exact proof term for the current goal is (nat_ordsucc_in_ordsucc n Hn m H3).
We will prove ordsucc n Inj1 n.
Let m be given.
Assume H1: m ordsucc n.
We will prove m Inj1 n.
Apply (ordsuccE n m H1) to the current goal.
Assume H2: m n.
Apply (nat_inv m (nat_p_trans n Hn m H2)) to the current goal.
Assume H3: m = 0.
rewrite the current goal using H3 (from left to right).
We will prove 0 Inj1 n.
An exact proof term for the current goal is (Inj1I1 n).
Assume H3: ∃k, nat_p k m = ordsucc k.
Apply (exandE_i nat_p (λk ⇒ m = ordsucc k) H3) to the current goal.
Let k be given.
Assume H4: nat_p k.
Assume H5: m = ordsucc k.
rewrite the current goal using H5 (from left to right).
We will prove ordsucc k Inj1 n.
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).
We will prove Inj1 k Inj1 n.
An exact proof term for the current goal is (Inj1I2 n k L2).
Assume H2: m = n.
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.
Assume H3: n = 0.
rewrite the current goal using H3 (from left to right) at position 1.
We will prove 0 Inj1 n.
An exact proof term for the current goal is (Inj1I1 n).
Assume H3: ∃k, nat_p k n = ordsucc k.
Apply (exandE_i nat_p (λk ⇒ n = ordsucc k) H3) to the current goal.
Let k be given.
Assume H4: nat_p k.
Assume H5: n = ordsucc k.
rewrite the current goal using H5 (from left to right) at position 1.
We will prove ordsucc k Inj1 n.
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).
We will prove Inj1 k Inj1 n.
An exact proof term for the current goal is (Inj1I2 n k L1).
Let n be given.
Assume Hn: nat_p n.
We will prove 1 + n = ordsucc n.
rewrite the current goal using Inj1_setsum_1L (from left to right).
We will prove Inj1 n = ordsucc n.
An exact proof term for the current goal is (L n Hn).
Theorem. (setsum_0_0)
0 + 0 = 0
Proof:
rewrite the current goal using (Inj0_setsum_0L 0) (from left to right).
We will prove Inj0 0 = 0.
An exact proof term for the current goal is Inj0_0.
Theorem. (setsum_1_0_1)
1 + 0 = 1
Proof:
An exact proof term for the current goal is (nat_setsum1_ordsucc 0 nat_0).
Theorem. (setsum_1_1_2)
1 + 1 = 2
Proof:
An exact proof term for the current goal is (nat_setsum1_ordsucc 1 nat_1).
Beginning of Section pair_setsum
Let pair ≝ setsum
Definition. We define proj0 to be λZ ⇒ {Unj z|zZ, ∃x : set, Inj0 x = z} of type setset.
Definition. We define proj1 to be λZ ⇒ {Unj z|zZ, ∃y : set, Inj1 y = z} of type setset.
Proof:
Apply (func_ext set set) to the current goal.
Let x be given.
Use symmetry.
We will prove 0 + x = Inj0 x.
An exact proof term for the current goal is (Inj0_setsum_0L x).
Proof:
Apply (func_ext set set) to the current goal.
Let x be given.
Use symmetry.
We will prove 1 + x = Inj1 x.
An exact proof term for the current goal is (Inj1_setsum_1L x).
Theorem. (pairI0)
∀X Y x, x Xpair 0 x pair X Y
Proof:
rewrite the current goal using Inj0_pair_0_eq (from right to left).
An exact proof term for the current goal is Inj0_setsum.
Theorem. (pairI1)
∀X Y y, y Ypair 1 y pair X Y
Proof:
rewrite the current goal using Inj1_pair_1_eq (from right to left).
An exact proof term for the current goal is Inj1_setsum.
Theorem. (pairE)
∀X Y z, z pair X Y(∃xX, z = pair 0 x) (∃yY, z = pair 1 y)
Proof:
rewrite the current goal using Inj0_pair_0_eq (from right to left).
rewrite the current goal using Inj1_pair_1_eq (from right to left).
An exact proof term for the current goal is setsum_Inj_inv.
Theorem. (pairE0)
∀X Y x, pair 0 x pair X Yx X
Proof:
Let X, Y and x be given.
Assume H1: pair 0 x pair X Y.
We will prove x X.
Apply (pairE X Y (pair 0 x) H1) to the current goal.
rewrite the current goal using Inj0_pair_0_eq (from right to left).
Assume H2: ∃x'X, Inj0 x = Inj0 x'.
Apply (exandE_i (λx' ⇒ x' X) (λx' ⇒ Inj0 x = Inj0 x') H2) to the current goal.
Let x' be given.
Assume H3: x' X.
Assume H4: Inj0 x = Inj0 x'.
We will prove x X.
rewrite the current goal using (Inj0_inj x x' H4) (from left to right).
We will prove x' X.
An exact proof term for the current goal is H3.
rewrite the current goal using Inj0_pair_0_eq (from right to left).
rewrite the current goal using Inj1_pair_1_eq (from right to left).
Assume H2: ∃yY, Inj0 x = Inj1 y.
We will prove False.
Apply (exandE_i (λy ⇒ y Y) (λy ⇒ Inj0 x = Inj1 y) H2) to the current goal.
Let y be given.
Assume _.
Assume H3: Inj0 x = Inj1 y.
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 Yy Y
Proof:
Let X, Y and y be given.
Assume H1: pair 1 y pair X Y.
We will prove y Y.
Apply (pairE X Y (pair 1 y) H1) to the current goal.
rewrite the current goal using Inj0_pair_0_eq (from right to left).
rewrite the current goal using Inj1_pair_1_eq (from right to left).
Assume H2: ∃xX, Inj1 y = Inj0 x.
We will prove False.
Apply (exandE_i (λx ⇒ x X) (λx ⇒ Inj1 y = Inj0 x) H2) to the current goal.
Let x be given.
Assume _.
Assume H3: Inj1 y = Inj0 x.
Apply (Inj0_Inj1_neq x y) to the current goal.
Use symmetry.
An exact proof term for the current goal is H3.
rewrite the current goal using Inj1_pair_1_eq (from right to left).
Assume H2: ∃y'Y, Inj1 y = Inj1 y'.
Apply (exandE_i (λy' ⇒ y' Y) (λy' ⇒ Inj1 y = Inj1 y') H2) to the current goal.
Let y' be given.
Assume H3: y' Y.
Assume H4: Inj1 y = Inj1 y'.
We will prove y Y.
rewrite the current goal using (Inj1_inj y y' H4) (from left to right).
We will prove y' Y.
An exact proof term for the current goal is H3.
Theorem. (proj0I)
∀w u : set, pair 0 u wu proj0 w
Proof:
rewrite the current goal using Inj0_pair_0_eq (from right to left).
Let w and u be given.
Assume H1: Inj0 u w.
We will prove u {Unj z|zw, ∃x : set, Inj0 x = z}.
rewrite the current goal using (Unj_Inj0_eq u) (from right to left).
We will prove Unj (Inj0 u) {Unj z|zw, ∃x : set, Inj0 x = z}.
Apply (ReplSepI w (λz ⇒ ∃x : set, Inj0 x = z) Unj (Inj0 u)) to the current goal.
We will prove Inj0 u w.
An exact proof term for the current goal is H1.
We will prove ∃x, Inj0 x = Inj0 u.
We use u to witness the existential quantifier.
Use reflexivity.
Theorem. (proj0E)
∀w u : set, u proj0 wpair 0 u w
Proof:
Let w and u be given.
Assume H1: u {Unj z|zw, ∃x : set, Inj0 x = z}.
rewrite the current goal using Inj0_pair_0_eq (from right to left).
We will prove Inj0 u w.
Apply (ReplSepE_impred w (λz ⇒ ∃x : set, Inj0 x = z) Unj u H1) to the current goal.
Let z be given.
Assume H2: z w.
Assume H3: ∃x, Inj0 x = z.
Assume H4: u = Unj z.
Apply H3 to the current goal.
Let x be given.
Assume H5: Inj0 x = z.
We will prove Inj0 u w.
rewrite the current goal using H4 (from left to right).
We will prove Inj0 (Unj z) w.
rewrite the current goal using H5 (from right to left).
We will prove Inj0 (Unj (Inj0 x)) w.
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.
Theorem. (proj1I)
∀w u : set, pair 1 u wu proj1 w
Proof:
rewrite the current goal using Inj1_pair_1_eq (from right to left).
Let w and u be given.
Assume H1: Inj1 u w.
We will prove u {Unj z|zw, ∃y : set, Inj1 y = z}.
rewrite the current goal using (Unj_Inj1_eq u) (from right to left).
We will prove Unj (Inj1 u) {Unj z|zw, ∃y : set, Inj1 y = z}.
Apply (ReplSepI w (λz ⇒ ∃y : set, Inj1 y = z) Unj (Inj1 u)) to the current goal.
We will prove Inj1 u w.
An exact proof term for the current goal is H1.
We will prove ∃y, Inj1 y = Inj1 u.
We use u to witness the existential quantifier.
Use reflexivity.
Theorem. (proj1E)
∀w u : set, u proj1 wpair 1 u w
Proof:
Let w and u be given.
Assume H1: u {Unj z|zw, ∃y : set, Inj1 y = z}.
rewrite the current goal using Inj1_pair_1_eq (from right to left).
We will prove Inj1 u w.
Apply (ReplSepE_impred w (λz ⇒ ∃y : set, Inj1 y = z) Unj u H1) to the current goal.
Let z be given.
Assume H2: z w.
Assume H3: ∃y, Inj1 y = z.
Assume H4: u = Unj z.
Apply H3 to the current goal.
Let y be given.
Assume H5: Inj1 y = z.
We will prove Inj1 u w.
rewrite the current goal using H4 (from left to right).
We will prove Inj1 (Unj z) w.
rewrite the current goal using H5 (from right to left).
We will prove Inj1 (Unj (Inj1 y)) w.
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.
Theorem. (proj0_pair_eq)
∀X Y : set, proj0 (pair X Y) = X
Proof:
Let X and Y be given.
Apply set_ext to the current goal.
We will prove proj0 (pair X Y) X.
Let u be given.
Assume H1: u proj0 (pair X Y).
We will prove u X.
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.
Assume H1: u X.
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.
We will prove u X.
An exact proof term for the current goal is H1.
Theorem. (proj1_pair_eq)
∀X Y : set, proj1 (pair X Y) = Y
Proof:
Let X and Y be given.
Apply set_ext to the current goal.
We will prove proj1 (pair X Y) Y.
Let u be given.
Assume H1: u proj1 (pair X Y).
We will prove u Y.
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.
Assume H1: u Y.
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.
We will prove u Y.
An exact proof term for the current goal is H1.
Definition. We define Sigma to be λX Y ⇒ xX{pair x y|yY x} of type set(setset)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 : setset, ∀xX, ∀yY x, pair x y xX, Y x
Proof:
Let X, Y and x be given.
Assume Hx: x X.
Let y be given.
Assume Hy: y Y x.
We will prove pair x y xX{pair x y|yY x}.
Apply (famunionI X (λx ⇒ {pair x y|yY x}) x (pair x y)) to the current goal.
We will prove x X.
An exact proof term for the current goal is Hx.
We will prove pair x y {pair x y|yY x}.
Apply ReplI to the current goal.
We will prove y Y x.
An exact proof term for the current goal is Hy.
Theorem. (Sigma_eta_proj0_proj1)
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z proj0 z X proj1 z Y (proj0 z)
Proof:
Let X, Y and z be given.
Assume H1: z xX, Y x.
We prove the intermediate claim L1: ∃xX, z {pair x y|yY x}.
An exact proof term for the current goal is (famunionE X (λx ⇒ {pair x y|yY x}) z H1).
Apply (exandE_i (λx ⇒ x X) (λx ⇒ z {pair x y|yY x}) L1) to the current goal.
Let x be given.
Assume H2: x X.
Assume H3: z {pair x y|yY x}.
Apply (ReplE_impred (Y x) (pair x) z H3) to the current goal.
Let y be given.
Assume H4: y Y x.
Assume H5: z = pair x y.
rewrite the current goal using H5 (from left to right).
We will prove pair (proj0 (pair x y)) (proj1 (pair x y)) = pair x y proj0 (pair x y) X proj1 (pair x y) Y (proj0 (pair x y)).
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.
We will prove x X.
An exact proof term for the current goal is H2.
We will prove y Y x.
An exact proof term for the current goal is H4.
Theorem. (proj_Sigma_eta)
∀X : set, ∀Y : setset, ∀z(xX, Y x), pair (proj0 z) (proj1 z) = z
Proof:
Let X, Y and z be given.
Assume H1: z xX, Y x.
Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z X) (proj1 z Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.
Assume H2 _ _.
An exact proof term for the current goal is H2.
Theorem. (proj0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj0 z X
Proof:
Let X, Y and z be given.
Assume H1: z xX, Y x.
Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z X) (proj1 z Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.
Assume _ H2 _.
An exact proof term for the current goal is H2.
Theorem. (proj1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Proof:
Let X, Y and z be given.
Assume H1: z xX, Y x.
Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z X) (proj1 z Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z H1)) to the current goal.
Assume _ _ H2.
An exact proof term for the current goal is H2.
Theorem. (pair_Sigma_E1)
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Proof:
Let X, Y, x and y be given.
Assume H1: pair x y xX, Y x.
We will prove y Y x.
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.
We will prove proj1 (pair x y) Y (proj0 (pair x y)).
An exact proof term for the current goal is (proj1_Sigma X Y (pair x y) H1).
Theorem. (Sigma_E)
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)∃xX, ∃yY x, z = pair x y
Proof:
Let X, Y and z be given.
Assume Hz: z xX, Y x.
Apply (and3E (pair (proj0 z) (proj1 z) = z) (proj0 z X) (proj1 z Y (proj0 z)) (Sigma_eta_proj0_proj1 X Y z Hz)) to the current goal.
Assume H1: pair (proj0 z) (proj1 z) = z.
Assume H2: proj0 z X.
Assume H3: proj1 z Y (proj0 z).
We use (proj0 z) to witness the existential quantifier.
Apply andI to the current goal.
We will prove proj0 z X.
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.
We will prove proj1 z Y (proj0 z).
An exact proof term for the current goal is H3.
We will prove z = pair (proj0 z) (proj1 z).
Use symmetry.
An exact proof term for the current goal is H1.
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {proj1 z|zf, ∃y : set, z = pair x y} of type setsetset.
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set Sigma Ax : 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 : setset, ∀xX, ∀yF x, pair x y λxXF x
Proof:
An exact proof term for the current goal is pair_Sigma.
Theorem. (lamE)
∀X : set, ∀F : setset, ∀z : set, z (λxXF x)∃xX, ∃yF 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 fy f x
Proof:
Let f, x and y be given.
Assume H1: pair x y f.
We will prove y {proj1 z|zf, ∃y : set, z = pair x y}.
rewrite the current goal using (proj1_pair_eq x y) (from right to left).
We will prove proj1 (pair x y) {proj1 z|zf, ∃y : set, z = pair x y}.
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 xpair x y f
Proof:
Let f, x and y be given.
Assume H1: y {proj1 z|zf, ∃y : set, z = pair x y}.
We will prove pair x y f.
Apply (ReplSepE_impred f (λz ⇒ ∃y : set, z = pair x y) proj1 y H1) to the current goal.
Let z be given.
Assume Hz: z f.
Assume H1: ∃y : set, z = pair x y.
Assume H2: y = proj1 z.
Apply H1 to the current goal.
Let v be given.
Assume H3: z = pair x v.
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.
Apply proj1_pair_eq to the current goal.
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 : setset, ∀x : set, x X(λxXF x) x = F x
Proof:
Let X, F and x be given.
Assume Hx: x X.
Apply set_ext to the current goal.
Let w be given.
Assume Hw: w (λxXF x) x.
We prove the intermediate claim L1: pair x w (λxXF x).
An exact proof term for the current goal is (apE (λxXF 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.
Assume Hw: w F x.
We will prove w (λxXF x) x.
Apply apI to the current goal.
We will prove pair x w λxXF x.
We will prove pair x w xX, F x.
Apply pair_Sigma to the current goal.
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.
Apply set_ext to the current goal.
Let w be given.
Assume H1: w proj0 u.
We will prove w u 0.
Apply apI to the current goal.
We will prove pair 0 w u.
Apply proj0E to the current goal.
We will prove w proj0 u.
An exact proof term for the current goal is H1.
Let w be given.
Assume H1: w u 0.
We will prove w proj0 u.
Apply proj0I to the current goal.
We will prove pair 0 w u.
Apply apE to the current goal.
We will prove w u 0.
An exact proof term for the current goal is H1.
Proof:
Let u be given.
Apply set_ext to the current goal.
Let w be given.
Assume H1: w proj1 u.
We will prove w u 1.
Apply apI to the current goal.
We will prove pair 1 w u.
Apply proj1E to the current goal.
We will prove w proj1 u.
An exact proof term for the current goal is H1.
Let w be given.
Assume H1: w u 1.
We will prove w proj1 u.
Apply proj1I to the current goal.
We will prove pair 1 w u.
Apply apE to the current goal.
We will prove w u 1.
An exact proof term for the current goal is H1.
Theorem. (pair_ap_0)
∀x y : set, (pair x y) 0 = x
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.
Apply proj0_pair_eq to the current goal.
Theorem. (pair_ap_1)
∀x y : set, (pair x y) 1 = y
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.
Apply proj1_pair_eq to the current goal.
Theorem. (ap0_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, 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).
Apply proj0_Sigma to the current goal.
Theorem. (ap1_Sigma)
∀X : set, ∀Y : setset, ∀z : set, z (xX, 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).
Apply proj1_Sigma to the current goal.
Definition. We define pair_p to be λu : setpair (u 0) (u 1) = u of type setprop.
Theorem. (pair_p_I)
∀x y, pair_p (pair x y)
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.
Assume H1: x 2.
Apply ordsuccE 1 x H1 to the current goal.
Assume H2: x 1.
We prove the intermediate claim L1: x = 0.
An exact proof term for the current goal is (SingE 0 x (Subq_1_Sing0 x H2)).
We will prove x {0,1}.
rewrite the current goal using L1 (from left to right).
We will prove 0 {0,1}.
An exact proof term for the current goal is (UPairI1 0 1).
Assume H2: x = 1.
We will prove x {0,1}.
rewrite the current goal using H2 (from left to right).
We will prove 1 {0,1}.
An exact proof term for the current goal is (UPairI2 0 1).
Theorem. (tuple_pair)
∀x y : set, pair x y = (x,y)
Proof:
Let x and y be given.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z pair x y.
Apply (pairE x y z Hz) to the current goal.
Assume H1: ∃ux, z = pair 0 u.
Apply (exandE_i (λu ⇒ u x) (λu ⇒ z = pair 0 u) H1) to the current goal.
Let u be given.
Assume Hu: u x.
Assume H2: z = pair 0 u.
We will prove z (x,y).
We will prove z λi2if i = 0 then x else y.
rewrite the current goal using H2 (from left to right).
We will prove pair 0 u λi2if i = 0 then x else y.
Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 0 In_0_2 u) to the current goal.
We will prove u if 0 = 0 then x else y.
rewrite the current goal using (If_i_1 (0 = 0) x y (λq H ⇒ H)) (from left to right).
We will prove u x.
An exact proof term for the current goal is Hu.
Assume H1: ∃uy, z = pair 1 u.
Apply (exandE_i (λu ⇒ u y) (λu ⇒ z = pair 1 u) H1) to the current goal.
Let u be given.
Assume Hu: u y.
Assume H2: z = pair 1 u.
We will prove z (x,y).
We will prove z λi2if i = 0 then x else y.
rewrite the current goal using H2 (from left to right).
We will prove pair 1 u λi2if i = 0 then x else y.
Apply (lamI 2 (λi ⇒ if i = 0 then x else y) 1 In_1_2 u) to the current goal.
We will prove u if 1 = 0 then x else y.
rewrite the current goal using (If_i_0 (1 = 0) x y neq_1_0) (from left to right).
We will prove u y.
An exact proof term for the current goal is Hu.
Let z be given.
Assume Hz: z (x,y).
We will prove z pair x y.
We prove the intermediate claim L1: ∃i2, ∃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).
Apply (exandE_i (λi ⇒ i 2) (λi ⇒ ∃w(if i = 0 then x else y), z = pair i w) L1) to the current goal.
Let i be given.
Assume Hi: i 2.
Assume H1: ∃w(if i = 0 then x else y), z = pair i w.
Apply (exandE_i (λw ⇒ w if i = 0 then x else y) (λw ⇒ z = pair i w) H1) to the current goal.
Let w be given.
Assume Hw: w if i = 0 then x else y.
Assume H2: z = pair i w.
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}.
An exact proof term for the current goal is (Subq_2_UPair01 i Hi).
Apply (UPairE i 0 1 L2) to the current goal.
Assume Hi0: i = 0.
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 will prove w x.
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.
Assume Hi1: i = 1.
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 will prove w y.
We prove the intermediate claim L3: (if i = 0 then x else y) = y.
rewrite the current goal using Hi1 (from left to right).
An exact proof term for the current goal is (If_i_0 (1 = 0) x y neq_1_0).
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𝒫 (xX, (Y x))|∀xX, f x Y x} of type set(setset)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 : setset, ∀f : set, (∀uf, pair_p u u 0 X)(∀xX, f x Y x)f xX, Y x
Proof:
Let X, Y and f be given.
Assume H1: ∀uf, pair_p u u 0 X.
Assume H2: ∀xX, f x Y x.
We will prove f {f𝒫 (xX, (Y x))|∀xX, f x Y x}.
Apply SepI to the current goal.
We will prove f 𝒫 (xX, (Y x)).
Apply PowerI to the current goal.
We will prove f xX, (Y x).
Let z be given.
Assume Hz: z f.
We will prove z xX, (Y x).
Apply (H1 z Hz) to the current goal.
Assume H3: pair (z 0) (z 1) = z.
Assume H4: z 0 X.
rewrite the current goal using H3 (from right to left).
We will prove pair (z 0) (z 1) xX, (Y x).
Apply pair_Sigma to the current goal.
We will prove z 0 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 ∀xX, f x Y x.
An exact proof term for the current goal is H2.
Theorem. (lam_Pi)
∀X : set, ∀Y : setset, ∀F : setset, (∀xX, F x Y x)(λxXF x) (xX, Y x)
Proof:
Let X, Y and F be given.
Assume H1: ∀xX, F x Y x.
We will prove (λxXF x) (xX, Y x).
Apply PiI to the current goal.
We will prove ∀u(λxXF x), pair_p u u 0 X.
Let u be given.
Assume Hu: u λxXF x.
We prove the intermediate claim L1: ∃xX, ∃yF 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 ⇒ ∃yF x, u = pair x y) L1) to the current goal.
Let x be given.
Assume Hx: x X.
Assume H2: ∃yF x, u = pair x y.
Apply (exandE_i (λy ⇒ y F x) (λy ⇒ u = pair x y) H2) to the current goal.
Let y be given.
Assume Hy: y F x.
Assume H3: u = pair x y.
Apply andI to the current goal.
We will prove pair_p u.
rewrite the current goal using H3 (from left to right).
Apply pair_p_I to the current goal.
We will prove u 0 X.
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).
We will prove x X.
An exact proof term for the current goal is Hx.
We will prove ∀xX, (λxXF x) x Y x.
Let x be given.
Assume Hx: x X.
rewrite the current goal using (beta X F x Hx) (from left to right).
We will prove F x Y x.
An exact proof term for the current goal is (H1 x Hx).
Theorem. (ap_Pi)
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Proof:
Let X, Y, f and x be given.
Assume Hf: f xX, Y x.
An exact proof term for the current goal is (SepE2 (𝒫 (xX, (Y x))) (λf ⇒ ∀xX, f x Y x) f Hf x).
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Theorem. (pair_tuple_fun)
pair = (λx y ⇒ (x,y))
Proof:
Apply func_ext set (setset) 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).
Apply tuple_pair to the current goal.
Theorem. (lamI2)
∀X, ∀F : setset, ∀xX, ∀yF x, (x,y) λxXF x
Proof:
We will prove (∀X, ∀F : setset, ∀xX, ∀yF x, ((λx y : set(x,y)) x y) λxXF x).
rewrite the current goal using pair_tuple_fun (from right to left).
An exact proof term for the current goal is lamI.
Beginning of Section Tuples
Variable x0 x1 : set
Proof:
rewrite the current goal using beta 2 (λi ⇒ if i = 0 then x0 else x1) 0 In_0_2 (from left to right).
Apply If_i_1 to the current goal.
Use reflexivity.
Proof:
rewrite the current goal using beta 2 (λi ⇒ if i = 0 then x0 else x1) 1 In_1_2 (from left to right).
Apply If_i_0 to the current goal.
Apply neq_1_0 to the current goal.
End of Section Tuples
Theorem. (ReplEq_setprod_ext)
∀X Y, ∀F G : setsetset, (∀xX, ∀yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Proof:
Let X, Y, F and G be given.
Assume H1: ∀xX, ∀yY, F x y = G x y.
Apply ReplEq_ext (X Y) (λw ⇒ F (w 0) (w 1)) (λw ⇒ G (w 0) (w 1)) to the current goal.
We will prove ∀wX Y, F (w 0) (w 1) = G (w 0) (w 1).
Let w be given.
Assume Hw: w X Y.
Apply H1 to the current goal.
We will prove w 0 X.
An exact proof term for the current goal is ap0_Sigma X (λ_ ⇒ Y) w Hw.
We will prove w 1 Y.
An exact proof term for the current goal is ap1_Sigma X (λ_ ⇒ Y) w Hw.
Theorem. (tuple_2_Sigma)
∀X : set, ∀Y : setset, ∀xX, ∀yY x, (x,y) xX, Y x
Proof:
An exact proof term for the current goal is lamI2.
Theorem. (tuple_2_setprod)
∀X : set, ∀Y : set, ∀xX, ∀yY, (x,y) X Y
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