We will prove ∃code : set → set, inj (finite_subcollections ω) ω code.
Set S to be the term ∑n ∈ ω, 𝒫 n.
We prove the intermediate claim Homega_countable: countable ω.
We will prove ∃f : set → set, inj ω ω f.
We use (λn ⇒ n) to witness the existential quantifier.
Apply (injI ω ω (λn ⇒ n)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
We will prove (λn0 : set ⇒ n0) n ∈ ω.
An exact proof term for the current goal is Hn.
Let a be given.
Assume Ha: a ∈ ω.
Let b be given.
Assume Hb: b ∈ ω.
Assume Heq: (λn0 : set ⇒ n0) a = (λn0 : set ⇒ n0) b.
We will prove a = b.
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hpow_countable: ∀n : set, n ∈ ω → countable (𝒫 n).
Let n be given.
Assume Hn: n ∈ ω.
We will prove countable (𝒫 n).
Apply (finite_countable (𝒫 n)) to the current goal.
We will prove finite (𝒫 n).
We will prove ∃m ∈ ω, equip (𝒫 n) m.
We prove the intermediate claim Hn_nat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n Hn).
We prove the intermediate claim HequipPow: equip (𝒫 n) (exp_nat 2 n).
An exact proof term for the current goal is (equip_Power_nat n Hn_nat).
We prove the intermediate claim Hpow_nat: nat_p (exp_nat 2 n).
An exact proof term for the current goal is (exp_nat_p 2 nat_2 n Hn_nat).
We prove the intermediate claim Hpow_omega: (exp_nat 2 n) ∈ ω.
An exact proof term for the current goal is (nat_p_omega (exp_nat 2 n) Hpow_nat).
We use (exp_nat 2 n) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hpow_omega.
An exact proof term for the current goal is HequipPow.
We prove the intermediate claim HS_countable: countable S.
An exact proof term for the current goal is (Sigma_countable ω Homega_countable (λn : set ⇒ 𝒫 n) Hpow_countable).
We prove the intermediate claim finite_sub_omega_bounded: ∀F : set, F ⊆ ω → finite F → ∃n ∈ ω, ∀m ∈ F, m ∈ n.
Let F be given.
Assume HFsub: F ⊆ ω.
Assume HFfin: finite F.
We prove the intermediate claim Hp0: (Empty ⊆ ω → ∃n ∈ ω, ∀m ∈ Empty, m ∈ n).
Assume Hsub0: Empty ⊆ ω.
We will prove ∃n ∈ ω, ∀m ∈ Empty, m ∈ 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).
Let m be given.
Assume Hm: m ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE m Hm).
We prove the intermediate claim Hpstep: ∀A y, finite A → y ∉ A → (A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n) → (A ∪ {y} ⊆ ω → ∃n0 ∈ ω, ∀m : set, m ∈ A ∪ {y} → m ∈ n0).
Let A and y be given.
Assume HAfin: finite A.
Assume HyA: y ∉ A.
Assume HpA: (A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n).
Assume HsubAy: A ∪ {y} ⊆ ω.
We prove the intermediate claim HsubA: A ⊆ ω.
An exact proof term for the current goal is (Subq_tra A (A ∪ {y}) ω (binunion_Subq_1 A {y}) HsubAy).
We prove the intermediate claim Hexn: ∃n ∈ ω, ∀m ∈ A, m ∈ n.
An exact proof term for the current goal is (HpA HsubA).
Apply Hexn to the current goal.
Let n be given.
Assume Hnand.
We prove the intermediate claim Hn: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (∀m ∈ A, m ∈ n) Hnand).
We prove the intermediate claim Hnprop: ∀m ∈ A, m ∈ n.
An exact proof term for the current goal is (andER (n ∈ ω) (∀m ∈ A, m ∈ n) Hnand).
We will prove ∃n0 ∈ ω, ∀m : set, m ∈ A ∪ {y} → m ∈ n0.
We prove the intermediate claim Hy_in_union: y ∈ A ∪ {y}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (SingI y).
We prove the intermediate claim Hy_omega: y ∈ ω.
An exact proof term for the current goal is (HsubAy y Hy_in_union).
We prove the intermediate claim Hysucc_omega: ordsucc y ∈ ω.
An exact proof term for the current goal is (omega_ordsucc y Hy_omega).
We prove the intermediate claim Hn_union_omega: n ∪ ordsucc y ∈ ω.
An exact proof term for the current goal is (omega_binunion n (ordsucc y) Hn Hysucc_omega).
Set n0 to be the term ordsucc (n ∪ ordsucc y).
We prove the intermediate claim Hn0_omega: n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (n ∪ ordsucc y) Hn_union_omega).
We use n0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn0_omega.
Let m be given.
Assume Hm: m ∈ A ∪ {y}.
We will prove m ∈ n0.
Apply (binunionE A {y} m Hm) to the current goal.
Assume HmA: m ∈ A.
We prove the intermediate claim Hmn: m ∈ n.
An exact proof term for the current goal is (Hnprop m HmA).
We prove the intermediate claim HmnU: m ∈ n ∪ ordsucc y.
An exact proof term for the current goal is (binunionI1 n (ordsucc y) m Hmn).
An exact proof term for the current goal is (ordsuccI1 (n ∪ ordsucc y) m HmnU).
Assume HmY: m ∈ {y}.
We prove the intermediate claim Hmy: m = y.
An exact proof term for the current goal is (SingE y m HmY).
rewrite the current goal using Hmy (from left to right).
We prove the intermediate claim Hy_in_succ: y ∈ ordsucc y.
An exact proof term for the current goal is (ordsuccI2 y).
We prove the intermediate claim Hy_in_U: y ∈ n ∪ ordsucc y.
An exact proof term for the current goal is (binunionI2 n (ordsucc y) y Hy_in_succ).
An exact proof term for the current goal is (ordsuccI1 (n ∪ ordsucc y) y Hy_in_U).
We prove the intermediate claim HpF: (F ⊆ ω → ∃n ∈ ω, ∀m ∈ F, m ∈ n).
An exact proof term for the current goal is (finite_ind (λA ⇒ A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n) Hp0 Hpstep F HFfin).
Apply HpF to the current goal.
An exact proof term for the current goal is HFsub.
Apply HS_countable to the current goal.
Let codeS of type set → set be given.
Assume HcodeS: inj S ω codeS.
Set bound to be the term λF ⇒ Eps_i (λn ⇒ n ∈ ω ∧ ∀m : set, m ∈ F → m ∈ n) of type set → set.
Set emb to be the term λF ⇒ (bound F,F) of type set → set.
Set code to be the term λF ⇒ codeS (emb F) of type set → set.
We use code to witness the existential quantifier.
Apply (injI (finite_subcollections ω) ω code) to the current goal.
Let F be given.
Assume HF: F ∈ finite_subcollections ω.
We will prove code F ∈ ω.
We prove the intermediate claim HFpow: F ∈ 𝒫 ω.
An exact proof term for the current goal is (SepE1 (𝒫 ω) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFsub: F ⊆ ω.
An exact proof term for the current goal is (PowerE ω F HFpow).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 ω) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim Hexb: ∃n ∈ ω, ∀m ∈ F, m ∈ n.
An exact proof term for the current goal is (finite_sub_omega_bounded F HFsub HFfin).
We prove the intermediate claim Hboundprop: bound F ∈ ω ∧ ∀m : set, m ∈ F → m ∈ bound F.
An exact proof term for the current goal is (Eps_i_ex (λn ⇒ n ∈ ω ∧ ∀m : set, m ∈ F → m ∈ n) Hexb).
We prove the intermediate claim Hbound_omega: bound F ∈ ω.
An exact proof term for the current goal is (andEL (bound F ∈ ω) (∀m : set, m ∈ F → m ∈ bound F) Hboundprop).
We prove the intermediate claim Hbound_sub: ∀m : set, m ∈ F → m ∈ bound F.
An exact proof term for the current goal is (andER (bound F ∈ ω) (∀m : set, m ∈ F → m ∈ bound F) Hboundprop).
We prove the intermediate claim HFpowB: F ∈ 𝒫 (bound F).
We prove the intermediate claim Hsub: F ⊆ bound F.
Let m be given.
Assume Hm: m ∈ F.
An exact proof term for the current goal is (Hbound_sub m Hm).
An exact proof term for the current goal is (PowerI (bound F) F Hsub).
We prove the intermediate claim HembS: emb F ∈ S.
An exact proof term for the current goal is (tuple_2_Sigma ω (λn : set ⇒ 𝒫 n) (bound F) Hbound_omega F HFpowB).
We prove the intermediate claim Hmap: ∀u ∈ S, codeS u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ S, codeS u ∈ ω) (∀u v ∈ S, codeS u = codeS v → u = v) HcodeS).
We prove the intermediate claim Hdef: code F = codeS (emb F).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (Hmap (emb F) HembS).
Let F1 be given.
Assume HF1: F1 ∈ finite_subcollections ω.
Let F2 be given.
Assume HF2: F2 ∈ finite_subcollections ω.
Assume Heq: code F1 = code F2.
We will prove F1 = F2.
We prove the intermediate claim HF1pow: F1 ∈ 𝒫 ω.
An exact proof term for the current goal is (SepE1 (𝒫 ω) (λF0 : set ⇒ finite F0) F1 HF1).
We prove the intermediate claim HF2pow: F2 ∈ 𝒫 ω.
An exact proof term for the current goal is (SepE1 (𝒫 ω) (λF0 : set ⇒ finite F0) F2 HF2).
We prove the intermediate claim HF1sub: F1 ⊆ ω.
An exact proof term for the current goal is (PowerE ω F1 HF1pow).
We prove the intermediate claim HF2sub: F2 ⊆ ω.
An exact proof term for the current goal is (PowerE ω F2 HF2pow).
We prove the intermediate claim HF1fin: finite F1.
An exact proof term for the current goal is (SepE2 (𝒫 ω) (λF0 : set ⇒ finite F0) F1 HF1).
We prove the intermediate claim HF2fin: finite F2.
An exact proof term for the current goal is (SepE2 (𝒫 ω) (λF0 : set ⇒ finite F0) F2 HF2).
We prove the intermediate claim Hexb1: ∃n ∈ ω, ∀m ∈ F1, m ∈ n.
An exact proof term for the current goal is (finite_sub_omega_bounded F1 HF1sub HF1fin).
We prove the intermediate claim Hexb2: ∃n ∈ ω, ∀m ∈ F2, m ∈ n.
An exact proof term for the current goal is (finite_sub_omega_bounded F2 HF2sub HF2fin).
We prove the intermediate claim Hb1: bound F1 ∈ ω ∧ ∀m : set, m ∈ F1 → m ∈ bound F1.
An exact proof term for the current goal is (Eps_i_ex (λn ⇒ n ∈ ω ∧ ∀m : set, m ∈ F1 → m ∈ n) Hexb1).
We prove the intermediate claim Hb2: bound F2 ∈ ω ∧ ∀m : set, m ∈ F2 → m ∈ bound F2.
An exact proof term for the current goal is (Eps_i_ex (λn ⇒ n ∈ ω ∧ ∀m : set, m ∈ F2 → m ∈ n) Hexb2).
We prove the intermediate claim Hbound1: bound F1 ∈ ω.
An exact proof term for the current goal is (andEL (bound F1 ∈ ω) (∀m : set, m ∈ F1 → m ∈ bound F1) Hb1).
We prove the intermediate claim Hbound2: bound F2 ∈ ω.
An exact proof term for the current goal is (andEL (bound F2 ∈ ω) (∀m : set, m ∈ F2 → m ∈ bound F2) Hb2).
We prove the intermediate claim HF1powB: F1 ∈ 𝒫 (bound F1).
We prove the intermediate claim Hsub: F1 ⊆ bound F1.
Let m be given.
Assume Hm: m ∈ F1.
We prove the intermediate claim Hsubm: ∀m0 : set, m0 ∈ F1 → m0 ∈ bound F1.
An exact proof term for the current goal is (andER (bound F1 ∈ ω) (∀m0 : set, m0 ∈ F1 → m0 ∈ bound F1) Hb1).
An exact proof term for the current goal is (Hsubm m Hm).
An exact proof term for the current goal is (PowerI (bound F1) F1 Hsub).
We prove the intermediate claim HF2powB: F2 ∈ 𝒫 (bound F2).
We prove the intermediate claim Hsub: F2 ⊆ bound F2.
Let m be given.
Assume Hm: m ∈ F2.
We prove the intermediate claim Hsubm: ∀m0 : set, m0 ∈ F2 → m0 ∈ bound F2.
An exact proof term for the current goal is (andER (bound F2 ∈ ω) (∀m0 : set, m0 ∈ F2 → m0 ∈ bound F2) Hb2).
An exact proof term for the current goal is (Hsubm m Hm).
An exact proof term for the current goal is (PowerI (bound F2) F2 Hsub).
We prove the intermediate claim Hemb1: emb F1 ∈ S.
An exact proof term for the current goal is (tuple_2_Sigma ω (λn : set ⇒ 𝒫 n) (bound F1) Hbound1 F1 HF1powB).
We prove the intermediate claim Hemb2: emb F2 ∈ S.
An exact proof term for the current goal is (tuple_2_Sigma ω (λn : set ⇒ 𝒫 n) (bound F2) Hbound2 F2 HF2powB).
We prove the intermediate claim Hcodeinj: ∀u v ∈ S, codeS u = codeS v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ S, codeS u ∈ ω) (∀u v ∈ S, codeS u = codeS v → u = v) HcodeS).
We prove the intermediate claim Hdef1: code F1 = codeS (emb F1).
Use reflexivity.
We prove the intermediate claim Hdef2: code F2 = codeS (emb F2).
Use reflexivity.
We prove the intermediate claim HeqS: codeS (emb F1) = codeS (emb F2).
rewrite the current goal using Hdef1 (from right to left).
rewrite the current goal using Hdef2 (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim HembEq: emb F1 = emb F2.
An exact proof term for the current goal is (Hcodeinj (emb F1) Hemb1 (emb F2) Hemb2 HeqS).
We prove the intermediate claim HF1Eq: F1 = F2.
We prove the intermediate claim Hemb1def: emb F1 = (bound F1,F1).
Use reflexivity.
We prove the intermediate claim Hemb2def: emb F2 = (bound F2,F2).
Use reflexivity.
We prove the intermediate claim Hproj1: (emb F1) 1 = F1.
rewrite the current goal using Hemb1def (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq (bound F1) F1).
We prove the intermediate claim Hproj2: (emb F2) 1 = F2.
rewrite the current goal using Hemb2def (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq (bound F2) F2).
We prove the intermediate claim HapEq: (emb F1) 1 = (emb F2) 1.
rewrite the current goal using HembEq (from left to right).
Use reflexivity.
rewrite the current goal using Hproj1 (from right to left).
rewrite the current goal using Hproj2 (from right to left).
An exact proof term for the current goal is HapEq.
An exact proof term for the current goal is HF1Eq.
∎