Let k be given.
Assume HkO: k ∈ ω.
We will prove homeomorphism (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) (Romega_tilde (ordsucc k)) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))) (Romega_extend_map k).
We will prove continuous_map (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) (Romega_tilde (ordsucc k)) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))) (Romega_extend_map k) ∧ ∃g : set, continuous_map (Romega_tilde (ordsucc k)) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))) (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) g ∧ (∀x : set, x ∈ setprod (Romega_tilde k) R → apply_fun g (apply_fun (Romega_extend_map k) x) = x) ∧ (∀y : set, y ∈ Romega_tilde (ordsucc k) → apply_fun (Romega_extend_map k) (apply_fun g y) = y).
Apply andI to the current goal.
An exact proof term for the current goal is (Romega_extend_map_continuous_to_Romega_tilde_succ k HkO).
We use (Romega_split_map k) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove topology_on (Romega_tilde (ordsucc k)) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))) ∧ topology_on (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) ∧ function_on (Romega_split_map k) (Romega_tilde (ordsucc k)) (setprod (Romega_tilde k) R) ∧ (∀V : set, V ∈ product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology → preimage_of (Romega_tilde (ordsucc k)) (Romega_split_map k) V ∈ subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HtopRomega: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
An exact proof term for the current goal is (subspace_topology_is_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k)) HtopRomega (Romega_tilde_sub_Romega (ordsucc k))).
We prove the intermediate claim HtopRomega: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HtopTildek: topology_on (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)).
An exact proof term for the current goal is (subspace_topology_is_topology R_omega_space R_omega_product_topology (Romega_tilde k) HtopRomega (Romega_tilde_sub_Romega k)).
We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
An exact proof term for the current goal is (product_topology_is_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology HtopTildek HtopR).
An exact proof term for the current goal is (Romega_split_map_function_on k HkO).
Let V be given.
Assume HV: V ∈ product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology.
An exact proof term for the current goal is (continuous_map_preimage (Romega_tilde (ordsucc k)) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde (ordsucc k))) (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) (Romega_split_map k) (Romega_split_map_continuous k HkO) V HV).
Let x be given.
Assume Hx: x ∈ setprod (Romega_tilde k) R.
We will prove apply_fun (Romega_split_map k) (apply_fun (Romega_extend_map k) x) = x.
Set x0 to be the term x 0.
Set x1 to be the term x 1.
We prove the intermediate claim Heta: x = (x0,x1).
An exact proof term for the current goal is (setprod_eta (Romega_tilde k) R x Hx).
rewrite the current goal using Heta (from left to right) at position 2.
We prove the intermediate claim Himg: apply_fun (Romega_extend_map k) x ∈ Romega_tilde (ordsucc k).
An exact proof term for the current goal is (Romega_extend_map_function_on_tilde_succ k HkO x Hx).
rewrite the current goal using (Romega_split_map_apply k (apply_fun (Romega_extend_map k) x) HkO Himg) (from left to right).
We prove the intermediate claim Hx0def: x0 = x 0.
Use reflexivity.
We prove the intermediate claim Hx1def: x1 = x 1.
Use reflexivity.
We prove the intermediate claim Hx0tilde: x0 ∈ Romega_tilde k.
rewrite the current goal using Hx0def (from left to right).
An exact proof term for the current goal is (ap0_Sigma (Romega_tilde k) (λ_ : set ⇒ R) x Hx).
We prove the intermediate claim Hx0X: x0 ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega k x0 Hx0tilde).
We prove the intermediate claim HextX: apply_fun (Romega_extend_map k) x ∈ R_omega_space.
An exact proof term for the current goal is (Romega_extend_map_function_on k HkO x Hx).
We prove the intermediate claim HrestTilde: Romega_restrict_seq k (apply_fun (Romega_extend_map k) x) ∈ Romega_tilde k.
An exact proof term for the current goal is (Romega_restrict_seq_in_Romega_tilde k (apply_fun (Romega_extend_map k) x) HkO HextX).
We prove the intermediate claim HrestX: Romega_restrict_seq k (apply_fun (Romega_extend_map k) x) ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (Romega_restrict_seq k (apply_fun (Romega_extend_map k) x)) HrestTilde).
We prove the intermediate claim HrestEq: Romega_restrict_seq k (apply_fun (Romega_extend_map k) x) = x0.
Apply (R_omega_space_ext (Romega_restrict_seq k (apply_fun (Romega_extend_map k) x)) x0 HrestX Hx0X) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (Romega_restrict_seq k (apply_fun (Romega_extend_map k) x)) i = apply_fun x0 i.
rewrite the current goal using (Romega_restrict_seq_apply k (apply_fun (Romega_extend_map k) x) i HkO HextX Hi) (from left to right).
Apply (xm (k ∈ i)) to the current goal.
Assume Hki: k ∈ i.
rewrite the current goal using (If_i_1 (k ∈ i) 0 (apply_fun (apply_fun (Romega_extend_map k) x) i) Hki) (from left to right).
We prove the intermediate claim Hx0prop: ∀j : set, j ∈ ω → k ∈ j → apply_fun x0 j = 0.
We prove the intermediate claim HdefT: Romega_tilde k = {f0 ∈ R_omega_space|∀j : set, j ∈ ω → k ∈ j → apply_fun f0 j = 0}.
Use reflexivity.
We prove the intermediate claim Hx0tilde2: x0 ∈ {f0 ∈ R_omega_space|∀j : set, j ∈ ω → k ∈ j → apply_fun f0 j = 0}.
rewrite the current goal using HdefT (from right to left).
An exact proof term for the current goal is Hx0tilde.
An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ ∀j : set, j ∈ ω → k ∈ j → apply_fun f0 j = 0) x0 Hx0tilde2).
rewrite the current goal using (Hx0prop i Hi Hki) (from left to right).
Use reflexivity.
Assume Hnki: ¬ (k ∈ i).
rewrite the current goal using (If_i_0 (k ∈ i) 0 (apply_fun (apply_fun (Romega_extend_map k) x) i) Hnki) (from left to right).
We prove the intermediate claim HnEq: ¬ (i = ordsucc k).
Assume Heq: i = ordsucc k.
We will prove False.
Apply Hnki to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (ordsuccI2 k).
We prove the intermediate claim HnSuccIn: ¬ (ordsucc k ∈ i).
Assume Hsi: ordsucc k ∈ i.
We will prove False.
Apply Hnki to the current goal.
We prove the intermediate claim Hordi: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i Hi).
We prove the intermediate claim HTi: TransSet i.
An exact proof term for the current goal is (ordinal_TransSet i Hordi).
We prove the intermediate claim Hsub: ordsucc k ⊆ i.
An exact proof term for the current goal is (HTi (ordsucc k) Hsi).
An exact proof term for the current goal is (Hsub k (ordsuccI2 k)).
rewrite the current goal using (Romega_extend_map_apply k x HkO Hx) (from left to right).
rewrite the current goal using (Romega_extend_seq_apply k x i Hi) (from left to right).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (x 1) (apply_fun (x 0) i)) HnSuccIn) (from left to right).
rewrite the current goal using (If_i_0 (i = ordsucc k) (x 1) (apply_fun (x 0) i) HnEq) (from left to right).
rewrite the current goal using Hx0def (from left to right).
Use reflexivity.
We prove the intermediate claim HcoordEq: apply_fun (apply_fun (Romega_extend_map k) x) (ordsucc k) = x1.
rewrite the current goal using (Romega_extend_map_apply k x HkO Hx) (from left to right).
We prove the intermediate claim HsuccO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
rewrite the current goal using (Romega_extend_seq_apply k x (ordsucc k) HsuccO) (from left to right).
We prove the intermediate claim Hnself: ¬ (ordsucc k ∈ ordsucc k).
An exact proof term for the current goal is (In_irref (ordsucc k)).
rewrite the current goal using (If_i_0 (ordsucc k ∈ ordsucc k) 0 (If_i (ordsucc k = ordsucc k) (x 1) (apply_fun (x 0) (ordsucc k))) Hnself) (from left to right).
We prove the intermediate claim Heq: ordsucc k = ordsucc k.
Use reflexivity.
rewrite the current goal using (If_i_1 (ordsucc k = ordsucc k) (x 1) (apply_fun (x 0) (ordsucc k)) Heq) (from left to right).
rewrite the current goal using Hx1def (from left to right).
Use reflexivity.
rewrite the current goal using HrestEq (from left to right).
rewrite the current goal using HcoordEq (from left to right).
Use reflexivity.
Let y be given.
Assume Hy: y ∈ Romega_tilde (ordsucc k).
We will prove apply_fun (Romega_extend_map k) (apply_fun (Romega_split_map k) y) = y.
We prove the intermediate claim Himg: apply_fun (Romega_split_map k) y ∈ setprod (Romega_tilde k) R.
An exact proof term for the current goal is (Romega_split_map_function_on k HkO y Hy).
rewrite the current goal using (Romega_extend_map_apply k (apply_fun (Romega_split_map k) y) HkO Himg) (from left to right).
Set p to be the term apply_fun (Romega_split_map k) y.
We prove the intermediate claim Hpdef: p = (Romega_restrict_seq k y,apply_fun y (ordsucc k)).
rewrite the current goal using (Romega_split_map_apply k y HkO Hy) (from left to right).
Use reflexivity.
We prove the intermediate claim HyX: y ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k) y Hy).
We prove the intermediate claim HsuccO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
We prove the intermediate claim HordSucc: ordinal (ordsucc k).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (ordsucc k) HsuccO).
We prove the intermediate claim HpX: Romega_extend_seq k p ∈ R_omega_space.
We prove the intermediate claim Hptilde: Romega_extend_seq k p ∈ Romega_tilde (ordsucc k).
We prove the intermediate claim HpEq: p = apply_fun (Romega_split_map k) y.
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (Romega_extend_seq_in_Romega_tilde_succ k (apply_fun (Romega_split_map k) y) HkO Himg).
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k) (Romega_extend_seq k p) Hptilde).
Apply (R_omega_space_ext (Romega_extend_seq k p) y HpX HyX) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (Romega_extend_seq k p) i = apply_fun y i.
We prove the intermediate claim Hordi: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i Hi).
Apply (ordinal_trichotomy_or_impred (ordsucc k) i HordSucc Hordi (apply_fun (Romega_extend_seq k p) i = apply_fun y i)) to the current goal.
Assume Hsi: ordsucc k ∈ i.
rewrite the current goal using (Romega_extend_seq_apply k p i Hi) (from left to right).
rewrite the current goal using (If_i_1 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) Hsi) (from left to right).
We prove the intermediate claim Hyprop: ∀j : set, j ∈ ω → ordsucc k ∈ j → apply_fun y j = 0.
We prove the intermediate claim HdefT: Romega_tilde (ordsucc k) = {f0 ∈ R_omega_space|∀j : set, j ∈ ω → ordsucc k ∈ j → apply_fun f0 j = 0}.
Use reflexivity.
We prove the intermediate claim Hy2: y ∈ {f0 ∈ R_omega_space|∀j : set, j ∈ ω → ordsucc k ∈ j → apply_fun f0 j = 0}.
rewrite the current goal using HdefT (from right to left).
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ ∀j : set, j ∈ ω → ordsucc k ∈ j → apply_fun f0 j = 0) y Hy2).
rewrite the current goal using (Hyprop i Hi Hsi) (from left to right).
Use reflexivity.
Assume Heq: ordsucc k = i.
rewrite the current goal using Heq (from right to left).
rewrite the current goal using (Romega_extend_seq_apply k p (ordsucc k) HsuccO) (from left to right).
We prove the intermediate claim Hnself: ¬ (ordsucc k ∈ ordsucc k).
An exact proof term for the current goal is (In_irref (ordsucc k)).
rewrite the current goal using (If_i_0 (ordsucc k ∈ ordsucc k) 0 (If_i (ordsucc k = ordsucc k) (p 1) (apply_fun (p 0) (ordsucc k))) Hnself) (from left to right).
We prove the intermediate claim Heqkk: ordsucc k = ordsucc k.
Use reflexivity.
rewrite the current goal using (If_i_1 (ordsucc k = ordsucc k) (p 1) (apply_fun (p 0) (ordsucc k)) Heqkk) (from left to right).
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (tuple_2_1_eq (Romega_restrict_seq k y) (apply_fun y (ordsucc k))) (from left to right).
Use reflexivity.
Assume His: i ∈ ordsucc k.
rewrite the current goal using (Romega_extend_seq_apply k p i Hi) (from left to right).
We prove the intermediate claim Hnsi: ¬ (ordsucc k ∈ i).
Assume Hsi: ordsucc k ∈ i.
An exact proof term for the current goal is (In_no2cycle i (ordsucc k) His Hsi).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) Hnsi) (from left to right).
We prove the intermediate claim Hneq: ¬ (i = ordsucc k).
Assume Heq: i = ordsucc k.
We will prove False.
We prove the intermediate claim Hself: ordsucc k ∈ ordsucc k.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is His.
An exact proof term for the current goal is (In_irref (ordsucc k) Hself).
rewrite the current goal using (If_i_0 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hneq) (from left to right).
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (tuple_2_0_eq (Romega_restrict_seq k y) (apply_fun y (ordsucc k))) (from left to right).
rewrite the current goal using (Romega_restrict_seq_apply k y i HkO HyX Hi) (from left to right).
We prove the intermediate claim Hnki: ¬ (k ∈ i).
Apply (ordsuccE k i His) to the current goal.
Assume Hik: i ∈ k.
We will prove ¬ (k ∈ i).
Assume Hki: k ∈ i.
An exact proof term for the current goal is (In_no2cycle i k Hik Hki).
Assume Hieq: i = k.
We will prove ¬ (k ∈ i).
Assume Hki: k ∈ i.
We prove the intermediate claim Hkk: k ∈ k.
rewrite the current goal using Hieq (from right to left) at position 2.
An exact proof term for the current goal is Hki.
An exact proof term for the current goal is (In_irref k Hkk).
rewrite the current goal using (If_i_0 (k ∈ i) 0 (apply_fun y i) Hnki) (from left to right).
Use reflexivity.
∎