Let Xi and Ti be given.
Assume Hchain: coherent_chain Xi Ti.
Assume Hnorms: ∀i : set, i ∈ ω → normal_space (apply_fun Xi i) (apply_fun Ti i).
Set X to be the term coherent_union Xi.
Set Tx to be the term coherent_topology Xi Ti.
We prove the intermediate claim HchainAB: (∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i)) ∧ (∀i : set, i ∈ ω → apply_fun Xi i ⊆ apply_fun Xi (ordsucc i)).
We prove the intermediate claim Habc: ((∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i)) ∧ (∀i : set, i ∈ ω → apply_fun Xi i ⊆ apply_fun Xi (ordsucc i))) ∧ (∀i : set, i ∈ ω → subspace_topology (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) (apply_fun Xi i) = apply_fun Ti i).
An exact proof term for the current goal is (andEL (((∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i)) ∧ (∀i : set, i ∈ ω → apply_fun Xi i ⊆ apply_fun Xi (ordsucc i))) ∧ (∀i : set, i ∈ ω → subspace_topology (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) (apply_fun Xi i) = apply_fun Ti i)) (∀i : set, i ∈ ω → closed_in (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) (apply_fun Xi i)) Hchain).
An exact proof term for the current goal is (andEL ((∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i)) ∧ (∀i : set, i ∈ ω → apply_fun Xi i ⊆ apply_fun Xi (ordsucc i))) (∀i : set, i ∈ ω → subspace_topology (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) (apply_fun Xi i) = apply_fun Ti i) Habc).
We prove the intermediate claim Htops: ∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i).
An exact proof term for the current goal is (andEL (∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i)) (∀i : set, i ∈ ω → apply_fun Xi i ⊆ apply_fun Xi (ordsucc i)) HchainAB).
We prove the intermediate claim HtopX: topology_on X Tx.
An exact proof term for the current goal is (ex35_9a_coherent_topology_is_topology Xi Ti Htops).
We will prove normal_space X Tx.
We will prove one_point_sets_closed X Tx ∧ ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove one_point_sets_closed X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HtopX.
Let x be given.
Assume HxX: x ∈ X.
We will prove closed_in X Tx {x}.
We prove the intermediate claim HsingSub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
Set U to be the term X ∖ {x}.
We prove the intermediate claim HUinTx: U ∈ Tx.
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (setminus_Subq X {x}).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsub).
We prove the intermediate claim HUall: ∀i ∈ ω, (U ∩ apply_fun Xi i) ∈ apply_fun Ti i.
Let i be given.
Assume HiO: i ∈ ω.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
We prove the intermediate claim HTi: topology_on Xi_i Ti_i.
An exact proof term for the current goal is (Htops i HiO).
We prove the intermediate claim HXiSubX: Xi_i ⊆ X.
An exact proof term for the current goal is (coherent_union_component_subset Xi i HiO).
We prove the intermediate claim HcapEq: U ∩ Xi_i = Xi_i ∖ {x}.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ Xi_i.
Apply binintersectE U Xi_i y Hy to the current goal.
Assume HyU HyXi.
We prove the intermediate claim Hynot: y ∉ {x}.
An exact proof term for the current goal is (setminusE2 X {x} y HyU).
An exact proof term for the current goal is (setminusI Xi_i {x} y HyXi Hynot).
Let y be given.
Assume Hy: y ∈ Xi_i ∖ {x}.
We prove the intermediate claim HyXi: y ∈ Xi_i.
An exact proof term for the current goal is (setminusE1 Xi_i {x} y Hy).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HXiSubX y HyXi).
We prove the intermediate claim Hynot: y ∉ {x}.
An exact proof term for the current goal is (setminusE2 Xi_i {x} y Hy).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (setminusI X {x} y HyX Hynot).
An exact proof term for the current goal is (binintersectI U Xi_i y HyU HyXi).
rewrite the current goal using HcapEq (from left to right).
Apply xm (x ∈ Xi_i) to the current goal.
Assume HxXi: x ∈ Xi_i.
We prove the intermediate claim Hnormi: normal_space Xi_i Ti_i.
An exact proof term for the current goal is (Hnorms i HiO).
We prove the intermediate claim Hone: one_point_sets_closed Xi_i Ti_i.
An exact proof term for the current goal is (andEL (one_point_sets_closed Xi_i Ti_i) (∀A B : set, closed_in Xi_i Ti_i A → closed_in Xi_i Ti_i B → A ∩ B = Empty → ∃U0 V0 : set, U0 ∈ Ti_i ∧ V0 ∈ Ti_i ∧ A ⊆ U0 ∧ B ⊆ V0 ∧ U0 ∩ V0 = Empty) Hnormi).
We prove the intermediate claim HsingClosed: closed_in Xi_i Ti_i {x}.
An exact proof term for the current goal is ((andER (topology_on Xi_i Ti_i) (∀y : set, y ∈ Xi_i → closed_in Xi_i Ti_i {y}) Hone) x HxXi).
We prove the intermediate claim Hop: open_in Xi_i Ti_i (Xi_i ∖ {x}).
An exact proof term for the current goal is (open_of_closed_complement Xi_i Ti_i {x} HsingClosed).
An exact proof term for the current goal is (open_in_elem Xi_i Ti_i (Xi_i ∖ {x}) Hop).
Assume HxNotXi: x ∉ Xi_i.
We prove the intermediate claim Heq: Xi_i ∖ {x} = Xi_i.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Xi_i ∖ {x}.
An exact proof term for the current goal is (setminusE1 Xi_i {x} y Hy).
Let y be given.
Assume HyXi: y ∈ Xi_i.
We will prove y ∈ Xi_i ∖ {x}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HyXi.
Assume HySing: y ∈ {x}.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y HySing).
Apply HxNotXi to the current goal.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is HyXi.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X Xi_i Ti_i HTi).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) U HUpow HUall).
We prove the intermediate claim HclosedComp: closed_in X Tx (X ∖ U).
An exact proof term for the current goal is (closed_of_open_complement X Tx U HtopX HUinTx).
We prove the intermediate claim Heq: X ∖ U = {x}.
We prove the intermediate claim HUdef: U = X ∖ {x}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq X {x} HsingSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HclosedComp.
Let A and B be given.
Assume HA: closed_in X Tx A.
Assume HB: closed_in X Tx B.
Assume Hab: A ∩ B = Empty.
We prove the intermediate claim HAi: ∀i : set, i ∈ ω → closed_in (apply_fun Xi i) (apply_fun Ti i) (A ∩ apply_fun Xi i).
Let i be given.
Assume HiO: i ∈ ω.
An exact proof term for the current goal is (closed_in_coherent_component Xi Ti A i Htops HA HiO).
We prove the intermediate claim HBi: ∀i : set, i ∈ ω → closed_in (apply_fun Xi i) (apply_fun Ti i) (B ∩ apply_fun Xi i).
Let i be given.
Assume HiO: i ∈ ω.
An exact proof term for the current goal is (closed_in_coherent_component Xi Ti B i Htops HB HiO).
We prove the intermediate claim Hdisji: ∀i : set, i ∈ ω → (A ∩ apply_fun Xi i) ∩ (B ∩ apply_fun Xi i) = Empty.
Let i be given.
Assume HiO: i ∈ ω.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (A ∩ apply_fun Xi i) ∩ (B ∩ apply_fun Xi i).
We will prove x ∈ Empty.
Apply binintersectE (A ∩ apply_fun Xi i) (B ∩ apply_fun Xi i) x Hx to the current goal.
Assume HxAi HxBi.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (apply_fun Xi i) x HxAi).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (binintersectE1 B (apply_fun Xi i) x HxBi).
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hab (from right to left).
An exact proof term for the current goal is HxAB.
An exact proof term for the current goal is HxE.
Let x be given.
Assume HxE: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim Hsep_i: ∀i : set, i ∈ ω → ∃U V : set, U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty.
Let i be given.
Assume HiO: i ∈ ω.
We prove the intermediate claim Hnormi: normal_space (apply_fun Xi i) (apply_fun Ti i).
An exact proof term for the current goal is (Hnorms i HiO).
We prove the intermediate claim Hsep: ∀A0 B0 : set, closed_in (apply_fun Xi i) (apply_fun Ti i) A0 → closed_in (apply_fun Xi i) (apply_fun Ti i) B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed (apply_fun Xi i) (apply_fun Ti i)) (∀A0 B0 : set, closed_in (apply_fun Xi i) (apply_fun Ti i) A0 → closed_in (apply_fun Xi i) (apply_fun Ti i) B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnormi).
An exact proof term for the current goal is (Hsep (A ∩ apply_fun Xi i) (B ∩ apply_fun Xi i) (HAi i HiO) (HBi i HiO) (Hdisji i HiO)).
We prove the intermediate claim Hab01: Rle 0 1.
An exact proof term for the current goal is (RleI 0 1 real_0 real_1 (not_Rlt_sym 0 1 Rlt_0_1)).
Set I01 to be the term closed_interval 0 1.
Set TI01 to be the term closed_interval_topology 0 1.
We prove the intermediate claim HexUrysohn_i: ∀i : set, i ∈ ω → ∃fi : set, continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 fi ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi i) → apply_fun fi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi i) → apply_fun fi x = 1).
Let i be given.
Assume HiO: i ∈ ω.
We prove the intermediate claim Hnormi: normal_space (apply_fun Xi i) (apply_fun Ti i).
An exact proof term for the current goal is (Hnorms i HiO).
An exact proof term for the current goal is (Urysohn_lemma (apply_fun Xi i) (apply_fun Ti i) (A ∩ apply_fun Xi i) (B ∩ apply_fun Xi i) 0 1 Hab01 Hnormi (HAi i HiO) (HBi i HiO) (Hdisji i HiO)).
We prove the intermediate claim Hextend_succ: ∀i fi : set, i ∈ ω → continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 fi → ∃gi : set, continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 gi ∧ (∀x : set, x ∈ apply_fun Xi i → apply_fun gi x = apply_fun fi x).
Let i and fi be given.
Assume HiO: i ∈ ω.
Assume Hfi: continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 fi.
We prove the intermediate claim HsuccO: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HnormS: normal_space (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)).
An exact proof term for the current goal is (Hnorms (ordsucc i) HsuccO).
An exact proof term for the current goal is (coherent_chain_Tietze_extend_interval_succ Xi Ti i 0 1 fi Hchain HiO Hab01 HnormS Hfi).
Set UV to be the term (λi : set ⇒ Eps_i (λp : set ⇒ ∃U V : set, p = (U,V) ∧ (U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty))).
We prove the intermediate claim HUVpair: ∀i : set, i ∈ ω → ∃U V : set, UV i = (U,V) ∧ (U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty).
Let i be given.
Assume HiO: i ∈ ω.
Set P to be the term (λp : set ⇒ ∃U V : set, p = (U,V) ∧ (U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty)).
We prove the intermediate claim Hex: ∃p : set, P p.
We prove the intermediate claim HexSep: ∃U V : set, U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep_i i HiO).
Apply HexSep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty.
Apply HexV to the current goal.
Let V be given.
Assume HUV: U ∈ apply_fun Ti i ∧ V ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U ∧ (B ∩ apply_fun Xi i) ⊆ V ∧ U ∩ V = Empty.
We use (U,V) to witness the existential quantifier.
We will prove ∃U0 V0 : set, (U,V) = (U0,V0) ∧ (U0 ∈ apply_fun Ti i ∧ V0 ∈ apply_fun Ti i ∧ (A ∩ apply_fun Xi i) ⊆ U0 ∧ (B ∩ apply_fun Xi i) ⊆ V0 ∧ U0 ∩ V0 = Empty).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HUV.
We prove the intermediate claim HP: P (UV i).
An exact proof term for the current goal is (Eps_i_ex P Hex).
An exact proof term for the current goal is HP.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Set f0 to be the term Eps_i (λfi : set ⇒ continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 fi ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun fi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun fi x = 1)).
We prove the intermediate claim Hf0pack: continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0 ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun f0 x = 1).
An exact proof term for the current goal is (Eps_i_ex (λfi : set ⇒ continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 fi ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun fi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun fi x = 1)) (HexUrysohn_i 0 H0O)).
Set step to be the term (λi fi : set ⇒ Eps_i (λgi : set ⇒ continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 gi ∧ (∀x : set, x ∈ apply_fun Xi i → apply_fun gi x = apply_fun fi x) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x = 1))).
Set Fi to be the term (λn : set ⇒ nat_primrec f0 step n).
We prove the intermediate claim HFi_def: ∀n : set, Fi n = nat_primrec f0 step n.
Let n be given.
Use reflexivity.
Set PFi to be the term (λn : set ⇒ continuous_map (apply_fun Xi n) (apply_fun Ti n) I01 TI01 (Fi n) ∧ ((∀x : set, x ∈ (A ∩ apply_fun Xi n) → apply_fun (Fi n) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi n) → apply_fun (Fi n) x = 1))).
We prove the intermediate claim HPFi_def: ∀n : set, PFi n = (continuous_map (apply_fun Xi n) (apply_fun Ti n) I01 TI01 (Fi n) ∧ ((∀x : set, x ∈ (A ∩ apply_fun Xi n) → apply_fun (Fi n) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi n) → apply_fun (Fi n) x = 1))).
Let n be given.
Use reflexivity.
We prove the intermediate claim HFi_all: ∀n : set, n ∈ ω → PFi n.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
Set p to be the term (λt : set ⇒ PFi t).
We prove the intermediate claim Hbase: p 0.
We prove the intermediate claim Hbase0: continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 (Fi 0) ∧ ((∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun (Fi 0) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun (Fi 0) x = 1)).
We prove the intermediate claim HFi0: Fi 0 = f0.
rewrite the current goal using (HFi_def 0) (from left to right).
rewrite the current goal using (nat_primrec_0 f0 step) (from left to right).
Use reflexivity.
Apply andI to the current goal.
rewrite the current goal using HFi0 (from left to right).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0) (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0) (andEL (continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0 ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0)) (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun f0 x = 1) Hf0pack)).
Apply andI to the current goal.
rewrite the current goal using HFi0 (from left to right).
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0) (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0) (andEL (continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0 ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0)) (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun f0 x = 1) Hf0pack)).
rewrite the current goal using HFi0 (from left to right).
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi 0) (apply_fun Ti 0) I01 TI01 f0 ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi 0) → apply_fun f0 x = 0)) (∀x : set, x ∈ (B ∩ apply_fun Xi 0) → apply_fun f0 x = 1) Hf0pack).
An exact proof term for the current goal is Hbase0.
We prove the intermediate claim Hstep: ∀t : set, nat_p t → p t → p (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume HtIH: PFi t.
We prove the intermediate claim HtIHpack: continuous_map (apply_fun Xi t) (apply_fun Ti t) I01 TI01 (Fi t) ∧ ((∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1)).
An exact proof term for the current goal is HtIH.
We will prove PFi (ordsucc t).
We prove the intermediate claim HtO: t ∈ ω.
An exact proof term for the current goal is (nat_p_omega t HtNat).
We prove the intermediate claim Hcont_t: continuous_map (apply_fun Xi t) (apply_fun Ti t) I01 TI01 (Fi t).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi t) (apply_fun Ti t) I01 TI01 (Fi t)) ((∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1)) HtIHpack).
We prove the intermediate claim HAt: ∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0.
An exact proof term for the current goal is (andEL (∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1) (andER (continuous_map (apply_fun Xi t) (apply_fun Ti t) I01 TI01 (Fi t)) ((∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1)) HtIHpack)).
We prove the intermediate claim HBt: ∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1.
An exact proof term for the current goal is (andER (∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1) (andER (continuous_map (apply_fun Xi t) (apply_fun Ti t) I01 TI01 (Fi t)) ((∀x : set, x ∈ (A ∩ apply_fun Xi t) → apply_fun (Fi t) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi t) → apply_fun (Fi t) x = 1)) HtIHpack)).
We prove the intermediate claim Hex: ∃gi : set, continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 gi ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun gi x = apply_fun (Fi t) x) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun gi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun gi x = 1).
An exact proof term for the current goal is (coherent_chain_extend_interval_succ_with_boundary Xi Ti A B t (Fi t) Hchain Hnorms HtO HA HB Hab Hcont_t HAt HBt).
We prove the intermediate claim HstepP: continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 1).
An exact proof term for the current goal is (Eps_i_ex (λgi : set ⇒ continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 gi ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun gi x = apply_fun (Fi t) x) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun gi x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun gi x = 1)) Hex).
We prove the intermediate claim HFi_succ_eq: Fi (ordsucc t) = step t (Fi t).
rewrite the current goal using (HFi_def (ordsucc t)) (from left to right).
rewrite the current goal using (nat_primrec_S f0 step t HtNat) (from left to right).
rewrite the current goal using (HFi_def t) (from right to left).
Use reflexivity.
We prove the intermediate claim Hleft: (continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x)) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0).
An exact proof term for the current goal is (andEL ((continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x)) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0)) (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 1) HstepP).
We prove the intermediate claim Hc: continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t))) (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x) (andEL (continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x)) (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0) Hleft)).
We prove the intermediate claim HA_s: ∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0.
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x)) (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0) Hleft).
We prove the intermediate claim HB_s: ∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 1.
An exact proof term for the current goal is (andER ((continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (step t (Fi t)) ∧ (∀x : set, x ∈ apply_fun Xi t → apply_fun (step t (Fi t)) x = apply_fun (Fi t) x)) ∧ (∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 0)) (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (step t (Fi t)) x = 1) HstepP).
We prove the intermediate claim Hstepgoal: continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (Fi (ordsucc t)) ∧ ((∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (Fi (ordsucc t)) x = 0) ∧ (∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (Fi (ordsucc t)) x = 1)).
Apply andI to the current goal.
We will prove continuous_map (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) I01 TI01 (Fi (ordsucc t)).
rewrite the current goal using HFi_succ_eq (from left to right).
An exact proof term for the current goal is Hc.
Apply andI to the current goal.
We will prove ∀x : set, x ∈ (A ∩ apply_fun Xi (ordsucc t)) → apply_fun (Fi (ordsucc t)) x = 0.
rewrite the current goal using HFi_succ_eq (from left to right).
An exact proof term for the current goal is HA_s.
We will prove ∀x : set, x ∈ (B ∩ apply_fun Xi (ordsucc t)) → apply_fun (Fi (ordsucc t)) x = 1.
rewrite the current goal using HFi_succ_eq (from left to right).
An exact proof term for the current goal is HB_s.
An exact proof term for the current goal is Hstepgoal.
An exact proof term for the current goal is (nat_ind p Hbase Hstep n HnNat).
We prove the intermediate claim HFi_succ_ext: ∀i : set, i ∈ ω → ∀x : set, x ∈ apply_fun Xi i → apply_fun (Fi (ordsucc i)) x = apply_fun (Fi i) x.
Let i be given.
Assume HiO: i ∈ ω.
Let x be given.
Assume HxXi: x ∈ apply_fun Xi i.
We prove the intermediate claim HiNat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i HiO).
We prove the intermediate claim HiPack: PFi i.
An exact proof term for the current goal is (HFi_all i HiO).
We prove the intermediate claim HiPackP: continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 (Fi i) ∧ ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1)).
An exact proof term for the current goal is HiPack.
We prove the intermediate claim Hcont_i: continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 (Fi i).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 (Fi i)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1)) HiPackP).
We prove the intermediate claim HA_i: ∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0.
An exact proof term for the current goal is (andEL (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1) (andER (continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 (Fi i)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1)) HiPackP)).
We prove the intermediate claim HB_i: ∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1.
An exact proof term for the current goal is (andER (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1) (andER (continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 (Fi i)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi i) → apply_fun (Fi i) x0 = 1)) HiPackP)).
We prove the intermediate claim Hex: ∃gi : set, continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 gi ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun gi x0 = apply_fun (Fi i) x0) ∧ (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x0 = 1).
An exact proof term for the current goal is (coherent_chain_extend_interval_succ_with_boundary Xi Ti A B i (Fi i) Hchain Hnorms HiO HA HB Hab Hcont_i HA_i HB_i).
We prove the intermediate claim HstepP: continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i)) ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0) ∧ (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 1).
An exact proof term for the current goal is (Eps_i_ex (λgi : set ⇒ continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 gi ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun gi x0 = apply_fun (Fi i) x0) ∧ (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi (ordsucc i)) → apply_fun gi x0 = 1)) Hex).
rewrite the current goal using (HFi_def (ordsucc i)) (from left to right).
rewrite the current goal using (nat_primrec_S f0 step i HiNat) (from left to right).
rewrite the current goal using (HFi_def i) (from right to left).
We prove the intermediate claim HleftP: (continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i)) ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0)) ∧ (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 0).
An exact proof term for the current goal is (andEL ((continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i)) ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0)) ∧ (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 0)) (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 1) HstepP).
We prove the intermediate claim Hcont_extP: continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i)) ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i)) ∧ (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0)) (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi (ordsucc i)) → apply_fun (step i (Fi i)) x0 = 0) HleftP).
We prove the intermediate claim Hext: ∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0.
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)) I01 TI01 (step i (Fi i))) (∀x0 : set, x0 ∈ apply_fun Xi i → apply_fun (step i (Fi i)) x0 = apply_fun (Fi i) x0) Hcont_extP).
An exact proof term for the current goal is (Hext x HxXi).
We prove the intermediate claim HFi_ext_mem: ∀j : set, j ∈ ω → ∀i : set, i ∈ j → ∀x : set, x ∈ apply_fun Xi i → apply_fun (Fi j) x = apply_fun (Fi i) x.
Let j be given.
Assume HjO: j ∈ ω.
We prove the intermediate claim HjNat: nat_p j.
An exact proof term for the current goal is (omega_nat_p j HjO).
Set q to be the term (λt : set ⇒ ∀i0 : set, i0 ∈ t → ∀x : set, x ∈ apply_fun Xi i0 → apply_fun (Fi t) x = apply_fun (Fi i0) x).
We prove the intermediate claim Hq0: q 0.
Let i0 be given.
Assume Hi0: i0 ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE i0 Hi0).
We prove the intermediate claim HqS: ∀t : set, nat_p t → q t → q (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume HtIH: q t.
Let i0 be given.
Assume Hi0s: i0 ∈ ordsucc t.
Let x be given.
Assume HxXi0: x ∈ apply_fun Xi i0.
Apply (ordsuccE t i0 Hi0s (apply_fun (Fi (ordsucc t)) x = apply_fun (Fi i0) x)) to the current goal.
Assume Hi0t: i0 ∈ t.
We prove the intermediate claim Hsub: apply_fun Xi i0 ⊆ apply_fun Xi t.
An exact proof term for the current goal is (coherent_chain_mono_mem Xi Ti t Hchain (nat_p_omega t HtNat) i0 Hi0t).
We prove the intermediate claim HxXt: x ∈ apply_fun Xi t.
An exact proof term for the current goal is (Hsub x HxXi0).
We prove the intermediate claim Hst: apply_fun (Fi (ordsucc t)) x = apply_fun (Fi t) x.
An exact proof term for the current goal is (HFi_succ_ext t (nat_p_omega t HtNat) x HxXt).
rewrite the current goal using Hst (from left to right).
An exact proof term for the current goal is (HtIH i0 Hi0t x HxXi0).
Assume Hi0eq: i0 = t.
rewrite the current goal using Hi0eq (from left to right).
We prove the intermediate claim HxXt: x ∈ apply_fun Xi t.
rewrite the current goal using Hi0eq (from right to left).
An exact proof term for the current goal is HxXi0.
An exact proof term for the current goal is (HFi_succ_ext t (nat_p_omega t HtNat) x HxXt).
We prove the intermediate claim Hqj: q j.
An exact proof term for the current goal is (nat_ind q Hq0 HqS j HjNat).
An exact proof term for the current goal is (Hqj).
Set idx to be the term (λx : set ⇒ Eps_i (λi : set ⇒ i ∈ ω ∧ x ∈ apply_fun Xi i)).
We prove the intermediate claim Hidx: ∀x : set, x ∈ X → idx x ∈ ω ∧ x ∈ apply_fun Xi (idx x).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexi: ∃i : set, i ∈ ω ∧ x ∈ apply_fun Xi i.
An exact proof term for the current goal is (coherent_unionE Xi x HxX).
An exact proof term for the current goal is (Eps_i_ex (λi : set ⇒ i ∈ ω ∧ x ∈ apply_fun Xi i) Hexi).
Set g to be the term (λx : set ⇒ apply_fun (Fi (idx x)) x).
Set f to be the term graph X g.
We prove the intermediate claim Hf_agree: ∀i x : set, i ∈ ω → x ∈ apply_fun Xi i → apply_fun f x = apply_fun (Fi i) x.
Let i and x be given.
Assume HiO: i ∈ ω.
Assume HxXi: x ∈ apply_fun Xi i.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (coherent_union_component_subset Xi i HiO x HxXi).
We prove the intermediate claim HidxPack: idx x ∈ ω ∧ x ∈ apply_fun Xi (idx x).
An exact proof term for the current goal is (Hidx x HxX).
Set k to be the term idx x.
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) (x ∈ apply_fun Xi k) HidxPack).
We prove the intermediate claim HxXk: x ∈ apply_fun Xi k.
An exact proof term for the current goal is (andER (k ∈ ω) (x ∈ apply_fun Xi k) HidxPack).
We prove the intermediate claim Hfx: apply_fun f x = g x.
An exact proof term for the current goal is (apply_fun_graph X g x HxX).
rewrite the current goal using Hfx (from left to right).
We prove the intermediate claim Hordi: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i HiO).
We prove the intermediate claim Hordk: ordinal k.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal k HkO).
Apply (ordinal_trichotomy_or_impred i k Hordi Hordk (apply_fun (Fi k) x = apply_fun (Fi i) x)) to the current goal.
Assume Hik: i ∈ k.
An exact proof term for the current goal is (HFi_ext_mem k HkO i Hik x HxXi).
Assume HikEq: i = k.
rewrite the current goal using HikEq (from left to right).
Use reflexivity.
Assume Hki: k ∈ i.
We prove the intermediate claim Heq: apply_fun (Fi i) x = apply_fun (Fi k) x.
An exact proof term for the current goal is (HFi_ext_mem i HiO k Hki x HxXk).
rewrite the current goal using Heq (from right to left).
Use reflexivity.
We prove the intermediate claim HI01top: topology_on I01 TI01.
An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology I01 R_standard_topology_is_topology (closed_interval_sub_R 0 1)).
We prove the intermediate claim Hf_on_components: ∀i : set, i ∈ ω → continuous_map (apply_fun Xi i) (apply_fun Ti i) I01 TI01 f.
Let i be given.
Assume HiO: i ∈ ω.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
We prove the intermediate claim HTi: topology_on Xi_i Ti_i.
An exact proof term for the current goal is (Htops i HiO).
We will prove continuous_map Xi_i Ti_i I01 TI01 f.
We will prove topology_on Xi_i Ti_i ∧ topology_on I01 TI01 ∧ function_on f Xi_i I01 ∧ ∀V : set, V ∈ TI01 → preimage_of Xi_i f V ∈ Ti_i.
Apply andI to the current goal.
We will prove (topology_on Xi_i Ti_i ∧ topology_on I01 TI01) ∧ function_on f Xi_i I01.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTi.
An exact proof term for the current goal is HI01top.
Let x be given.
Assume HxXi: x ∈ Xi_i.
We prove the intermediate claim HFiPack: PFi i.
An exact proof term for the current goal is (HFi_all i HiO).
We prove the intermediate claim HFiCont: continuous_map Xi_i Ti_i I01 TI01 (Fi i).
An exact proof term for the current goal is (andEL (continuous_map Xi_i Ti_i I01 TI01 (Fi i)) ((∀x0 : set, x0 ∈ (A ∩ Xi_i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ Xi_i) → apply_fun (Fi i) x0 = 1)) HFiPack).
We prove the intermediate claim HFiFun: function_on (Fi i) Xi_i I01.
An exact proof term for the current goal is (continuous_map_function_on Xi_i Ti_i I01 TI01 (Fi i) HFiCont).
rewrite the current goal using (Hf_agree i x HiO HxXi) (from left to right) at position 1.
An exact proof term for the current goal is (HFiFun x HxXi).
Let V be given.
Assume HV: V ∈ TI01.
We prove the intermediate claim HpreEq: preimage_of Xi_i f V = preimage_of Xi_i (Fi i) V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of Xi_i f V.
We prove the intermediate claim HxXi: x ∈ Xi_i.
An exact proof term for the current goal is (SepE1 Xi_i (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 Xi_i (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun (Fi i) x.
An exact proof term for the current goal is (Hf_agree i x HiO HxXi).
We prove the intermediate claim HfxV': apply_fun (Fi i) x ∈ V.
rewrite the current goal using Hfx (from right to left) at position 1.
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI Xi_i (λx0 : set ⇒ apply_fun (Fi i) x0 ∈ V) x HxXi HfxV').
Let x be given.
Assume Hx: x ∈ preimage_of Xi_i (Fi i) V.
We prove the intermediate claim HxXi: x ∈ Xi_i.
An exact proof term for the current goal is (SepE1 Xi_i (λx0 : set ⇒ apply_fun (Fi i) x0 ∈ V) x Hx).
We prove the intermediate claim HfxV: apply_fun (Fi i) x ∈ V.
An exact proof term for the current goal is (SepE2 Xi_i (λx0 : set ⇒ apply_fun (Fi i) x0 ∈ V) x Hx).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun (Fi i) x.
An exact proof term for the current goal is (Hf_agree i x HiO HxXi).
We prove the intermediate claim HfxV': apply_fun f x ∈ V.
rewrite the current goal using Hfx (from left to right) at position 1.
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI Xi_i (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxXi HfxV').
rewrite the current goal using HpreEq (from left to right).
We prove the intermediate claim HFiCont2: continuous_map Xi_i Ti_i I01 TI01 (Fi i).
An exact proof term for the current goal is (andEL (continuous_map Xi_i Ti_i I01 TI01 (Fi i)) ((∀x0 : set, x0 ∈ (A ∩ Xi_i) → apply_fun (Fi i) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ Xi_i) → apply_fun (Fi i) x0 = 1)) (HFi_all i HiO)).
An exact proof term for the current goal is (continuous_map_preimage Xi_i Ti_i I01 TI01 (Fi i) HFiCont2 V HV).
We prove the intermediate claim Hf_fun: function_on f X I01.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hkpack: idx x ∈ ω ∧ x ∈ apply_fun Xi (idx x).
An exact proof term for the current goal is (Hidx x HxX).
Set k to be the term idx x.
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim HxXk: x ∈ apply_fun Xi k.
An exact proof term for the current goal is (andER (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim Hfx: apply_fun f x = g x.
An exact proof term for the current goal is (apply_fun_graph X g x HxX).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right) at position 1.
We prove the intermediate claim HFiCont: continuous_map (apply_fun Xi k) (apply_fun Ti k) I01 TI01 (Fi k).
An exact proof term for the current goal is (andEL (continuous_map (apply_fun Xi k) (apply_fun Ti k) I01 TI01 (Fi k)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1)) (HFi_all k HkO)).
We prove the intermediate claim HFiFun: function_on (Fi k) (apply_fun Xi k) I01.
An exact proof term for the current goal is (continuous_map_function_on (apply_fun Xi k) (apply_fun Ti k) I01 TI01 (Fi k) HFiCont).
An exact proof term for the current goal is (HFiFun x HxXk).
We prove the intermediate claim Hf_cont: continuous_map X Tx I01 TI01 f.
An exact proof term for the current goal is (ex35_9b_continuous_if_restrictions_continuous Xi Ti I01 TI01 f Htops HI01top Hf_fun Hf_on_components).
We prove the intermediate claim HH01: Hausdorff_space I01 TI01.
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff R R_standard_topology I01 R_standard_topology_Hausdorff (closed_interval_sub_R 0 1)).
We prove the intermediate claim HHsep: ∀y1 y2 : set, y1 ∈ I01 → y2 ∈ I01 → y1 ≠ y2 → ∃U0 V0 : set, U0 ∈ TI01 ∧ V0 ∈ TI01 ∧ y1 ∈ U0 ∧ y2 ∈ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER (topology_on I01 TI01) (∀y1 y2 : set, y1 ∈ I01 → y2 ∈ I01 → y1 ≠ y2 → ∃U0 V0 : set, U0 ∈ TI01 ∧ V0 ∈ TI01 ∧ y1 ∈ U0 ∧ y2 ∈ V0 ∧ U0 ∩ V0 = Empty) HH01).
We prove the intermediate claim H0I01: 0 ∈ I01.
An exact proof term for the current goal is (left_endpoint_in_closed_interval 0 1 Hab01).
We prove the intermediate claim H1I01: 1 ∈ I01.
An exact proof term for the current goal is (right_endpoint_in_closed_interval 0 1 Hab01).
We prove the intermediate claim HexUV01: ∃O0 O1 : set, O0 ∈ TI01 ∧ O1 ∈ TI01 ∧ 0 ∈ O0 ∧ 1 ∈ O1 ∧ O0 ∩ O1 = Empty.
An exact proof term for the current goal is (HHsep 0 1 H0I01 H1I01 neq_0_1).
Apply HexUV01 to the current goal.
Let O0 be given.
Assume HexO1.
Apply HexO1 to the current goal.
Let O1 be given.
Assume HOpack.
We prove the intermediate claim Hleft: ((O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0) ∧ 1 ∈ O1.
An exact proof term for the current goal is (andEL (((O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0) ∧ 1 ∈ O1) (O0 ∩ O1 = Empty) HOpack).
We prove the intermediate claim Hdisj01: O0 ∩ O1 = Empty.
An exact proof term for the current goal is (andER (((O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0) ∧ 1 ∈ O1) (O0 ∩ O1 = Empty) HOpack).
We prove the intermediate claim Habc: (O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0.
An exact proof term for the current goal is (andEL ((O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0) (1 ∈ O1) Hleft).
We prove the intermediate claim H1O1: 1 ∈ O1.
An exact proof term for the current goal is (andER ((O0 ∈ TI01 ∧ O1 ∈ TI01) ∧ 0 ∈ O0) (1 ∈ O1) Hleft).
We prove the intermediate claim Hab: O0 ∈ TI01 ∧ O1 ∈ TI01.
An exact proof term for the current goal is (andEL (O0 ∈ TI01 ∧ O1 ∈ TI01) (0 ∈ O0) Habc).
We prove the intermediate claim H0O0: 0 ∈ O0.
An exact proof term for the current goal is (andER (O0 ∈ TI01 ∧ O1 ∈ TI01) (0 ∈ O0) Habc).
We prove the intermediate claim HO0: O0 ∈ TI01.
An exact proof term for the current goal is (andEL (O0 ∈ TI01) (O1 ∈ TI01) Hab).
We prove the intermediate claim HO1: O1 ∈ TI01.
An exact proof term for the current goal is (andER (O0 ∈ TI01) (O1 ∈ TI01) Hab).
Set U to be the term preimage_of X f O0.
Set V to be the term preimage_of X f O1.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (continuous_map_preimage X Tx I01 TI01 f Hf_cont O0 HO0).
An exact proof term for the current goal is (continuous_map_preimage X Tx I01 TI01 f Hf_cont O1 HO1).
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HAsub: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U0 ∈ Tx, A = X ∖ U0) (closed_in_package X Tx A HA)).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsub x HxA).
We will prove x ∈ U.
We prove the intermediate claim Hfx: apply_fun f x = g x.
An exact proof term for the current goal is (apply_fun_graph X g x HxX).
We prove the intermediate claim Hkpack: idx x ∈ ω ∧ x ∈ apply_fun Xi (idx x).
An exact proof term for the current goal is (Hidx x HxX).
Set k to be the term idx x.
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim HxXk: x ∈ apply_fun Xi k.
An exact proof term for the current goal is (andER (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim HFiPack: PFi k.
An exact proof term for the current goal is (HFi_all k HkO).
We prove the intermediate claim HA_pack: (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1).
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi k) (apply_fun Ti k) I01 TI01 (Fi k)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1)) HFiPack).
We prove the intermediate claim HA_k: ∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0.
An exact proof term for the current goal is (andEL (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1) HA_pack).
We prove the intermediate claim HxAk: x ∈ (A ∩ apply_fun Xi k).
An exact proof term for the current goal is (binintersectI A (apply_fun Xi k) x HxA HxXk).
We prove the intermediate claim Hval0: apply_fun (Fi k) x = 0.
An exact proof term for the current goal is (HA_k x HxAk).
We prove the intermediate claim Hg0: g x = 0.
An exact proof term for the current goal is Hval0.
We prove the intermediate claim Hfx0: apply_fun f x = 0.
rewrite the current goal using Hfx (from left to right) at position 1.
An exact proof term for the current goal is Hg0.
We prove the intermediate claim HfxO0: apply_fun f x ∈ O0.
rewrite the current goal using Hfx0 (from left to right) at position 1.
An exact proof term for the current goal is H0O0.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ O0) x HxX HfxO0).
Let x be given.
Assume HxB: x ∈ B.
We prove the intermediate claim HBsub: B ⊆ X.
An exact proof term for the current goal is (andEL (B ⊆ X) (∃U0 ∈ Tx, B = X ∖ U0) (closed_in_package X Tx B HB)).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HBsub x HxB).
We will prove x ∈ V.
We prove the intermediate claim Hfx: apply_fun f x = g x.
An exact proof term for the current goal is (apply_fun_graph X g x HxX).
We prove the intermediate claim Hkpack: idx x ∈ ω ∧ x ∈ apply_fun Xi (idx x).
An exact proof term for the current goal is (Hidx x HxX).
Set k to be the term idx x.
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim HxXk: x ∈ apply_fun Xi k.
An exact proof term for the current goal is (andER (k ∈ ω) (x ∈ apply_fun Xi k) Hkpack).
We prove the intermediate claim HFiPack: PFi k.
An exact proof term for the current goal is (HFi_all k HkO).
We prove the intermediate claim HB_pack: (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1).
An exact proof term for the current goal is (andER (continuous_map (apply_fun Xi k) (apply_fun Ti k) I01 TI01 (Fi k)) ((∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) ∧ (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1)) HFiPack).
We prove the intermediate claim HB_k: ∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1.
An exact proof term for the current goal is (andER (∀x0 : set, x0 ∈ (A ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 0) (∀x0 : set, x0 ∈ (B ∩ apply_fun Xi k) → apply_fun (Fi k) x0 = 1) HB_pack).
We prove the intermediate claim HxBk: x ∈ (B ∩ apply_fun Xi k).
An exact proof term for the current goal is (binintersectI B (apply_fun Xi k) x HxB HxXk).
We prove the intermediate claim Hval1: apply_fun (Fi k) x = 1.
An exact proof term for the current goal is (HB_k x HxBk).
We prove the intermediate claim Hg1: g x = 1.
An exact proof term for the current goal is Hval1.
We prove the intermediate claim Hfx1: apply_fun f x = 1.
rewrite the current goal using Hfx (from left to right) at position 1.
An exact proof term for the current goal is Hg1.
We prove the intermediate claim HfxO1: apply_fun f x ∈ O1.
rewrite the current goal using Hfx1 (from left to right) at position 1.
An exact proof term for the current goal is H1O1.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ O1) x HxX HfxO1).
Apply set_ext to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∩ V.
We will prove x ∈ Empty.
Apply binintersectE U V x HxUV to the current goal.
Assume HxU HxV.
We prove the intermediate claim Hfx0: apply_fun f x ∈ O0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ O0) x HxU).
We prove the intermediate claim Hfx1: apply_fun f x ∈ O1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ O1) x HxV).
We prove the intermediate claim HfxIn: apply_fun f x ∈ O0 ∩ O1.
An exact proof term for the current goal is (binintersectI O0 O1 (apply_fun f x) Hfx0 Hfx1).
We prove the intermediate claim HfxE: apply_fun f x ∈ Empty.
We prove the intermediate claim Himpl: apply_fun f x ∈ Empty → apply_fun f x ∈ O0 ∩ O1.
Assume HfxE0: apply_fun f x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE (apply_fun f x) HfxE0).
We prove the intermediate claim Htrans: apply_fun f x ∈ O0 ∩ O1 → apply_fun f x ∈ Empty.
An exact proof term for the current goal is (Hdisj01 (λS T : set ⇒ apply_fun f x ∈ T → apply_fun f x ∈ S) Himpl).
An exact proof term for the current goal is (Htrans HfxIn).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE (apply_fun f x) HfxE).
Let x be given.
Assume HxE: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
∎