Theorem. (KnasterTarski_set) The following is provable:
∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y
Proof:
Let A and F be given.
Assume H1 H2.
Set Y to be the term {u ∈ A|∀X ∈ 𝒫 A, F X ⊆ X → u ∈ X} of type set.
We prove the intermediate claim L1: Y ∈ 𝒫 A.
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 ⊆ X → Y ⊆ 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 ⊆ X → u ∈ 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) The following is provable:
∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 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|x ∈ U}.
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) The following is provable:
∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}
Proof:
Let f, U and V be given.
Assume HUV.
Let y be given.
Assume Hy: y ∈ {f x|x ∈ U}.
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|x ∈ V}.
Apply ReplI to the current goal.
Apply HUV to the current goal.
An exact proof term for the current goal is Hx.
∎
Theorem. (setminus_In_Power) The following is provable:
∀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_antimonotone) The following is provable:
∀A U V, U ⊆ V → A ∖ 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) The following is provable:
∀A B, ∀f g : set → set, inj A B f → inj B A g → equip 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|y ∈ B ∖ {f x|x ∈ A ∖ X}} of type set → set.
We prove the intermediate claim L1: ∀U ∈ 𝒫 A, F U ∈ 𝒫 A.
Let U be given.
Assume HU.
We will prove {g y|y ∈ B ∖ {f x|x ∈ A ∖ U}} ∈ 𝒫 A.
Apply image_In_Power B A g Hg1 to the current goal.
We will prove B ∖ {f x|x ∈ A ∖ U} ∈ 𝒫 B.
Apply setminus_In_Power to the current goal.
We prove the intermediate claim L2: ∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V.
Let U be given.
Assume HU.
Let V be given.
Assume HV HUV.
We will prove {g y|y ∈ B ∖ {f x|x ∈ A ∖ U}} ⊆ {g y|y ∈ B ∖ {f x|x ∈ A ∖ V}}.
Apply image_monotone g to the current goal.
We will prove B ∖ {f x|x ∈ A ∖ U} ⊆ B ∖ {f x|x ∈ A ∖ V}.
Apply setminus_antimonotone to the current goal.
We will prove {f x|x ∈ A ∖ V} ⊆ {f x|x ∈ A ∖ 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 set → set.
We will prove ∃f : set → set, bij A B f.
We use h to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx.
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|x ∈ A ∖ Y}) g x L1 to the current goal.
Let y be given.
Assume H4: y ∈ B ∖ {f x|x ∈ A ∖ 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|x ∈ A ∖ Y} y H4.
rewrite the current goal using H5 (from left to right).
We will prove inv B g (g y) ∈ B.
rewrite the current goal using inj_linv B A 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|x ∈ A ∖ Y}) g x Lx to the current goal.
Let z be given.
Assume Hz1: z ∈ B ∖ {f x|x ∈ A ∖ Y}.
Assume Hz2: x = g z.
Apply setminusE B {f x|x ∈ A ∖ 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 y → x = y.
We prove the intermediate claim Ly: y ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4.
Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g y Ly to the current goal.
Let w be given.
Assume Hw1: w ∈ B ∖ {f x|x ∈ A ∖ 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 A g Hg2 z Hz1a (from left to right).
rewrite the current goal using inj_linv B A g Hg2 w (setminusE1 B {f x|x ∈ A ∖ 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 y → x = y.
rewrite the current goal using Hz2 (from left to right).
rewrite the current goal using inj_linv B A g Hg2 z Hz1a (from left to right).
We will prove z = f y → g z = y.
Assume H5: z = f y.
We will prove False.
Apply Hz1b to the current goal.
We will prove z ∈ {f x|x ∈ A ∖ Y}.
rewrite the current goal using H5 (from left to right).
Apply ReplI to the current goal.
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 y → x = y.
We prove the intermediate claim Ly: y ∈ F Y.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H4.
Apply ReplE_impred (B ∖ {f x|x ∈ A ∖ Y}) g y Ly to the current goal.
Let w be given.
Assume Hw1: w ∈ B ∖ {f x|x ∈ A ∖ Y}.
Assume Hw2: y = g w.
Apply setminusE B {f x|x ∈ A ∖ 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 A 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|x ∈ A ∖ 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 y → x = 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|x ∈ A ∖ Y}) to the current goal.
Assume H3: w ∈ {f x|x ∈ A ∖ 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|x ∈ A ∖ 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|y ∈ B ∖ {f x|x ∈ A ∖ 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|x ∈ A ∖ Y}.
An exact proof term for the current goal is H3.
We use (g w) to witness the existential quantifier.
Apply andI to the current goal.
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 A g Hg2 w Hw.
∎