We will prove ¬ countable_set binary_sequences_Romega.
Assume Hcount: countable_set binary_sequences_Romega.
Apply Hcount to the current goal.
Let g be given.
Assume Hg: inj binary_sequences_Romega ω g.
Set F to be the term (λA : set ⇒ graph ω (λn : set ⇒ if n ∈ A then 1 else 0)).
We prove the intermediate claim HF_inj: inj (𝒫 ω) binary_sequences_Romega F.
We will prove (∀A ∈ 𝒫 ω, F A ∈ binary_sequences_Romega) ∧ (∀A B ∈ 𝒫 ω, F A = F B → A = B).
Apply andI to the current goal.
Let A be given.
Assume HA: A ∈ 𝒫 ω.
We will prove F A ∈ binary_sequences_Romega.
Apply (SepI real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) (F A)) to the current goal.
Set h to be the term (λn : set ⇒ if n ∈ A then 1 else 0).
We prove the intermediate claim Hsub: graph ω h ⊆ setprod ω R.
Let p be given.
Assume Hp: p ∈ graph ω h.
We will prove p ∈ setprod ω R.
Apply (ReplE_impred ω (λi : set ⇒ (i,h i)) p Hp (p ∈ setprod ω R)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume Hpdef: p = (i,h i).
rewrite the current goal using Hpdef (from left to right).
We prove the intermediate claim HhiR: h i ∈ R.
Apply (xm (i ∈ A) (h i ∈ R)) to the current goal.
Assume HiA: i ∈ A.
We prove the intermediate claim Heq: h i = 1.
An exact proof term for the current goal is (If_i_1 (i ∈ A) 1 0 HiA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_1.
Assume HniA: ¬ (i ∈ A).
We prove the intermediate claim Heq: h i = 0.
An exact proof term for the current goal is (If_i_0 (i ∈ A) 1 0 HniA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω R i (h i) Hi HhiR).
We prove the intermediate claim Hpow: graph ω h ∈ 𝒫 (setprod ω R).
An exact proof term for the current goal is (PowerI (setprod ω R) (graph ω h) Hsub).
We prove the intermediate claim Htot: total_function_on (graph ω h) ω R.
We will prove function_on (graph ω h) ω R ∧ ∀i : set, i ∈ ω → ∃y : set, y ∈ R ∧ (i,y) ∈ (graph ω h).
Apply andI to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (graph ω h) i ∈ R.
We prove the intermediate claim Happ: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
Apply (xm (i ∈ A) (h i ∈ R)) to the current goal.
Assume HiA: i ∈ A.
We prove the intermediate claim Heq: h i = 1.
An exact proof term for the current goal is (If_i_1 (i ∈ A) 1 0 HiA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_1.
Assume HniA: ¬ (i ∈ A).
We prove the intermediate claim Heq: h i = 0.
An exact proof term for the current goal is (If_i_0 (i ∈ A) 1 0 HniA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_0.
Let i be given.
Assume Hi: i ∈ ω.
We use (h i) to witness the existential quantifier.
We will prove (h i ∈ R ∧ (i,h i) ∈ graph ω h).
Apply andI to the current goal.
Apply (xm (i ∈ A) (h i ∈ R)) to the current goal.
Assume HiA: i ∈ A.
We prove the intermediate claim Heq: h i = 1.
An exact proof term for the current goal is (If_i_1 (i ∈ A) 1 0 HiA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_1.
Assume HniA: ¬ (i ∈ A).
We prove the intermediate claim Heq: h i = 0.
An exact proof term for the current goal is (If_i_0 (i ∈ A) 1 0 HniA).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ (k,h k)) i Hi).
We prove the intermediate claim Hfg: functional_graph (graph ω h).
An exact proof term for the current goal is (functional_graph_graph ω h).
An exact proof term for the current goal is (SepI (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) (graph ω h) Hpow (andI (total_function_on (graph ω h) ω R) (functional_graph (graph ω h)) Htot Hfg)).
Let n be given.
Assume Hn: n ∈ ω.
We will prove apply_fun (F A) n ∈ {0,1}.
We prove the intermediate claim Happ: apply_fun (F A) n = if n ∈ A then 1 else 0.
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ if k ∈ A then 1 else 0) n Hn).
rewrite the current goal using Happ (from left to right).
Apply (xm (n ∈ A) ((if n ∈ A then 1 else 0) ∈ {0,1})) to the current goal.
Assume HnA: n ∈ A.
rewrite the current goal using (If_i_1 (n ∈ A) 1 0 HnA) (from left to right).
An exact proof term for the current goal is (UPairI2 0 1).
Assume HnnotA: ¬ (n ∈ A).
rewrite the current goal using (If_i_0 (n ∈ A) 1 0 HnnotA) (from left to right).
An exact proof term for the current goal is (UPairI1 0 1).
Let A be given.
Assume HA: A ∈ 𝒫 ω.
Let B be given.
Assume HB: B ∈ 𝒫 ω.
Assume Heq: F A = F B.
We will prove A = B.
Apply set_ext to the current goal.
Let n be given.
Assume HnA: n ∈ A.
We will prove n ∈ B.
Apply (xm (n ∈ B) (n ∈ B)) to the current goal.
Assume HnB: n ∈ B.
An exact proof term for the current goal is HnB.
Assume HnnotB: ¬ (n ∈ B).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (PowerE ω A HA n HnA).
We prove the intermediate claim HAval: apply_fun (F A) n = 1.
We prove the intermediate claim HFdef: F A = graph ω (λk : set ⇒ if k ∈ A then 1 else 0).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k ∈ A then 1 else 0) n HnO) (from left to right).
rewrite the current goal using (If_i_1 (n ∈ A) 1 0 HnA) (from left to right).
Use reflexivity.
We prove the intermediate claim HBval: apply_fun (F B) n = 0.
We prove the intermediate claim HFdef: F B = graph ω (λk : set ⇒ if k ∈ B then 1 else 0).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k ∈ B then 1 else 0) n HnO) (from left to right).
rewrite the current goal using (If_i_0 (n ∈ B) 1 0 HnnotB) (from left to right).
Use reflexivity.
We prove the intermediate claim HappEq: apply_fun (F A) n = apply_fun (F B) n.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim H1: 1 = apply_fun (F B) n.
rewrite the current goal using HappEq (from right to left).
Use symmetry.
An exact proof term for the current goal is HAval.
We prove the intermediate claim Hcontra: 1 = 0.
rewrite the current goal using HBval (from right to left) at position 2.
An exact proof term for the current goal is H1.
We prove the intermediate claim H01: 0 = 1.
Use symmetry.
An exact proof term for the current goal is Hcontra.
An exact proof term for the current goal is (FalseE (neq_0_1 H01) (n ∈ B)).
Let n be given.
Assume HnB: n ∈ B.
We will prove n ∈ A.
Apply (xm (n ∈ A) (n ∈ A)) to the current goal.
Assume HnA: n ∈ A.
An exact proof term for the current goal is HnA.
Assume HnnotA: ¬ (n ∈ A).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (PowerE ω B HB n HnB).
We prove the intermediate claim HBval: apply_fun (F B) n = 1.
We prove the intermediate claim HFdef: F B = graph ω (λk : set ⇒ if k ∈ B then 1 else 0).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k ∈ B then 1 else 0) n HnO) (from left to right).
rewrite the current goal using (If_i_1 (n ∈ B) 1 0 HnB) (from left to right).
Use reflexivity.
We prove the intermediate claim HAval: apply_fun (F A) n = 0.
We prove the intermediate claim HFdef: F A = graph ω (λk : set ⇒ if k ∈ A then 1 else 0).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k ∈ A then 1 else 0) n HnO) (from left to right).
rewrite the current goal using (If_i_0 (n ∈ A) 1 0 HnnotA) (from left to right).
Use reflexivity.
We prove the intermediate claim HappEqAB: apply_fun (F A) n = apply_fun (F B) n.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim HappEq: apply_fun (F B) n = apply_fun (F A) n.
Use symmetry.
An exact proof term for the current goal is HappEqAB.
We prove the intermediate claim H1: 1 = apply_fun (F A) n.
rewrite the current goal using HappEq (from right to left).
Use symmetry.
An exact proof term for the current goal is HBval.
We prove the intermediate claim Hcontra: 1 = 0.
rewrite the current goal using HAval (from right to left) at position 2.
An exact proof term for the current goal is H1.
We prove the intermediate claim H01: 0 = 1.
Use symmetry.
An exact proof term for the current goal is Hcontra.
An exact proof term for the current goal is (FalseE (neq_0_1 H01) (n ∈ A)).
Set h to be the term (λA : set ⇒ g (F A)).
We prove the intermediate claim HinjPow: inj (𝒫 ω) ω h.
An exact proof term for the current goal is (inj_comp (𝒫 ω) binary_sequences_Romega ω F g HF_inj Hg).
An exact proof term for the current goal is (form100_22_v2 h HinjPow).
∎