Set f to be the term λu ⇒ {2 * n|n ∈ ω, n ∈ u} ∪ {2 * n + 1|n ∈ ω, n ' ∈ u} of type set → set.
We prove the intermediate claim L1: ∀u v, SNoLev u ⊆ ω → u ⊆ SNoElts_ (SNoLev u) → f u = f v → u ⊆ v.
Let u and v be given.
Assume HLuo: SNoLev u ⊆ ω.
Assume HuELu: u ⊆ SNoElts_ (SNoLev u).
Assume Huv: f u = f v.
Let x be given.
Assume Hx: x ∈ u.
We will prove x ∈ v.
Apply binunionE (SNoLev u) {n '|n ∈ SNoLev u} x (HuELu x Hx) to the current goal.
Assume H1: x ∈ SNoLev u.
We prove the intermediate claim Lx: x ∈ ω.
An exact proof term for the current goal is HLuo x H1.
We prove the intermediate claim L2x: 2 * x ∈ f v.
rewrite the current goal using Huv (from right to left).
We will prove 2 * x ∈ f u.
We will prove 2 * x ∈ {2 * n|n ∈ ω, n ∈ u} ∪ {2 * n + 1|n ∈ ω, n ' ∈ u}.
Apply binunionI1 to the current goal.
Apply ReplSepI to the current goal.
We will prove x ∈ ω.
An exact proof term for the current goal is Lx.
We will prove x ∈ u.
An exact proof term for the current goal is Hx.
Apply binunionE {2 * n|n ∈ ω, n ∈ v} {2 * n + 1|n ∈ ω, n ' ∈ v} (2 * x) L2x to the current goal.
Assume H2: 2 * x ∈ {2 * n|n ∈ ω, n ∈ v}.
Apply ReplSepE_impred ω (λn ⇒ n ∈ v) (λn ⇒ 2 * n) (2 * x) H2 to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hnv: n ∈ v.
Assume H2x2n: 2 * x = 2 * n.
We prove the intermediate claim Lxn: x = n.
An exact proof term for the current goal is mul_SNo_nonzero_cancel_L 2 x n SNo_2 neq_2_0 (omega_SNo x Lx) (omega_SNo n Hn) H2x2n.
We will prove x ∈ v.
rewrite the current goal using Lxn (from left to right).
An exact proof term for the current goal is Hnv.
Assume H2: 2 * x ∈ {2 * n + 1|n ∈ ω, n ' ∈ v}.
We will prove False.
Apply ReplSepE_impred ω (λn ⇒ n ' ∈ v) (λn ⇒ 2 * n + 1) (2 * x) H2 to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hnv: n ' ∈ v.
Assume H2x2n1: 2 * x = 2 * n + 1.
We prove the intermediate claim L2nomega: 2 * n ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega 2 (nat_p_omega 2 nat_2) n Hn.
We prove the intermediate claim L2no: ordinal (2 * n).
Apply nat_p_ordinal to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is L2nomega.
We will prove False.
An exact proof term for the current goal is not_eq_2m_2n1 x (Subq_omega_int x Lx) n (Subq_omega_int n Hn) H2x2n1.
Assume H1: x ∈ {n '|n ∈ SNoLev u}.
Apply ReplE_impred (SNoLev u) (λn ⇒ n ') x H1 to the current goal.
Let n be given.
Assume Hn: n ∈ SNoLev u.
Assume Hxn: x = n '.
We prove the intermediate claim Lnomega: n ∈ ω.
An exact proof term for the current goal is HLuo n Hn.
We prove the intermediate claim L2nomega: 2 * n ∈ ω.
An exact proof term for the current goal is mul_SNo_In_omega 2 (nat_p_omega 2 nat_2) n Lnomega.
We prove the intermediate claim L2no: ordinal (2 * n).
Apply nat_p_ordinal to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is L2nomega.
We prove the intermediate claim Ln'u: n ' ∈ u.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim L2x1: 2 * n + 1 ∈ f v.
rewrite the current goal using Huv (from right to left).
We will prove 2 * n + 1 ∈ {2 * n|n ∈ ω, n ∈ u} ∪ {2 * n + 1|n ∈ ω, n ' ∈ u}.
Apply binunionI2 to the current goal.
We will prove 2 * n + 1 ∈ {2 * n + 1|n ∈ ω, n ' ∈ u}.
An exact proof term for the current goal is ReplSepI ω (λn ⇒ n ' ∈ u) (λn ⇒ 2 * n + 1) n Lnomega Ln'u.
Apply binunionE {2 * n|n ∈ ω, n ∈ v} {2 * n + 1|n ∈ ω, n ' ∈ v} (2 * n + 1) L2x1 to the current goal.
Assume H2: 2 * n + 1 ∈ {2 * n|n ∈ ω, n ∈ v}.
We will prove False.
Apply ReplSepE_impred ω (λn ⇒ n ∈ v) (λn ⇒ 2 * n) (2 * n + 1) H2 to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hmv: m ∈ v.
Assume H2n12m: 2 * n + 1 = 2 * m.
We will prove False.
Apply not_eq_2m_2n1 m (Subq_omega_int m Hm) n (Subq_omega_int n Lnomega) to the current goal.
We will prove 2 * m = 2 * n + 1.
Use symmetry.
An exact proof term for the current goal is H2n12m.
Assume H2: 2 * n + 1 ∈ {2 * n + 1|n ∈ ω, n ' ∈ v}.
Apply ReplSepE_impred ω (λn ⇒ n ' ∈ v) (λn ⇒ 2 * n + 1) (2 * n + 1) H2 to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hmv: m ' ∈ v.
Assume H2n12m1: 2 * n + 1 = 2 * m + 1.
We prove the intermediate claim Lnm: n = m.
Apply mul_SNo_nonzero_cancel_L 2 n m SNo_2 neq_2_0 (omega_SNo n Lnomega) (omega_SNo m Hm) to the current goal.
We will prove 2 * n = 2 * m.
An exact proof term for the current goal is add_SNo_cancel_R (2 * n) 1 (2 * m) (omega_SNo (2 * n) L2nomega) SNo_1 (SNo_mul_SNo 2 m SNo_2 (omega_SNo m Hm)) H2n12m1.
We will prove x ∈ v.
rewrite the current goal using Hxn (from left to right).
We will prove n ' ∈ v.
An exact proof term for the current goal is Lnm (λ_ u ⇒ u ' ∈ v) Hmv.
We will prove ∃f : set → set, inj (SNoS_ (ordsucc ω)) (𝒫 ω) f.
We use f to witness the existential quantifier.
We will prove (∀u ∈ SNoS_ (ordsucc ω), f u ∈ 𝒫 ω) ∧ (∀u v ∈ SNoS_ (ordsucc ω), f u = f v → u = v).
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ SNoS_ (ordsucc ω).
We will prove f u ∈ 𝒫 ω.
Apply PowerI to the current goal.
We will prove {2 * n|n ∈ ω, n ∈ u} ∪ {2 * n + 1|n ∈ ω, n ' ∈ u} ⊆ ω.
Apply binunion_Subq_min to the current goal.
We will prove {2 * n|n ∈ ω, n ∈ u} ⊆ ω.
Let x be given.
Assume Hx.
Apply ReplSepE_impred ω (λn ⇒ n ∈ u) (λn ⇒ 2 * n) x Hx to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hnu: n ∈ u.
Assume Hx2n: x = 2 * n.
We will prove x ∈ ω.
rewrite the current goal using Hx2n (from left to right).
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
An exact proof term for the current goal is Hn.
We will prove {2 * n + 1|n ∈ ω, n ' ∈ u} ⊆ ω.
Let x be given.
Assume Hx.
Apply ReplSepE_impred ω (λn ⇒ n ' ∈ u) (λn ⇒ 2 * n + 1) x Hx to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hnu: n ' ∈ u.
Assume Hx2n1: x = 2 * n + 1.
We will prove x ∈ ω.
rewrite the current goal using Hx2n1 (from left to right).
Apply add_SNo_In_omega to the current goal.
We will prove 2 * n ∈ ω.
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
An exact proof term for the current goal is Hn.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
Let u be given.
Assume Hu: u ∈ SNoS_ (ordsucc ω).
Let v be given.
Assume Hv: v ∈ SNoS_ (ordsucc ω).
Assume Huv: f u = f v.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal u Hu to the current goal.
Assume Hu1: SNoLev u ∈ ordsucc ω.
Assume Hu2: ordinal (SNoLev u).
Assume Hu3: SNo u.
Assume Hu4: SNo_ (SNoLev u) u.
Apply Hu4 to the current goal.
Assume Hu4a: u ⊆ SNoElts_ (SNoLev u).
Assume _.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal v Hv to the current goal.
Assume Hv1: SNoLev v ∈ ordsucc ω.
Assume Hv2: ordinal (SNoLev v).
Assume Hv3: SNo v.
Assume Hv4: SNo_ (SNoLev v) v.
Apply Hv4 to the current goal.
Assume Hv4a: v ⊆ SNoElts_ (SNoLev v).
Assume _.
We prove the intermediate claim LLuo: SNoLev u ⊆ ω.
Apply TransSet_In_ordsucc_Subq to the current goal.
We will prove TransSet ω.
An exact proof term for the current goal is omega_TransSet.
We will prove SNoLev u ∈ ordsucc ω.
An exact proof term for the current goal is Hu1.
We prove the intermediate claim LLvo: SNoLev v ⊆ ω.
Apply TransSet_In_ordsucc_Subq to the current goal.
We will prove TransSet ω.
An exact proof term for the current goal is omega_TransSet.
We will prove SNoLev v ∈ ordsucc ω.
An exact proof term for the current goal is Hv1.
We will prove u = v.
Apply set_ext to the current goal.
We will prove u ⊆ v.
An exact proof term for the current goal is L1 u v LLuo Hu4a Huv.
We will prove v ⊆ u.
An exact proof term for the current goal is L1 v u LLvo Hv4a (λq ⇒ Huv (λx y ⇒ q y x)).
∎