Let Xi, Ti, Y, Ty and f be given.
Assume Htops: ∀i : set, i ∈ ω → topology_on (apply_fun Xi i) (apply_fun Ti i).
Assume HYtop: topology_on Y Ty.
Assume Hfun: function_on f (coherent_union Xi) Y.
Assume Hconti: ∀i : set, i ∈ ω → continuous_map (apply_fun Xi i) (apply_fun Ti i) Y Ty f.
Set X to be the term coherent_union Xi.
Set Tx to be the term coherent_topology Xi Ti.
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 continuous_map X Tx Y Ty f.
We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
Apply andI to the current goal.
We will prove (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ topology_on Y Ty.
Apply andI to the current goal.
An exact proof term for the current goal is HtopX.
An exact proof term for the current goal is HYtop.
An exact proof term for the current goal is Hfun.
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of X f V ∈ Tx.
We prove the intermediate claim HprePow: preimage_of X f V ∈ 𝒫 X.
Apply PowerI X (preimage_of X f V) to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).
We prove the intermediate claim HpreAll: ∀i ∈ ω, ((preimage_of X f V) ∩ 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 Hcont: continuous_map Xi_i Ti_i Y Ty f.
An exact proof term for the current goal is (Hconti i HiO).
We prove the intermediate claim Hprei: preimage_of Xi_i f V ∈ Ti_i.
An exact proof term for the current goal is (continuous_map_preimage Xi_i Ti_i Y Ty f Hcont V HV).
We prove the intermediate claim HXiSub: Xi_i ⊆ X.
Let x be given.
Assume Hx: x ∈ Xi_i.
We will prove x ∈ X.
Set Fam to be the term {apply_fun Xi j|j ∈ ω}.
We prove the intermediate claim HXdef: X = ⋃ Fam.
Use reflexivity.
rewrite the current goal using HXdef (from left to right).
We prove the intermediate claim HXi_i_in: Xi_i ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λj : set ⇒ apply_fun Xi j) i HiO).
An exact proof term for the current goal is (UnionI Fam x Xi_i Hx HXi_i_in).
We prove the intermediate claim HpreEq: (preimage_of X f V) ∩ Xi_i = preimage_of Xi_i f V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (preimage_of X f V) ∩ Xi_i.
Apply binintersectE (preimage_of X f V) Xi_i x Hx to the current goal.
Assume HxPre HxXi.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPre).
An exact proof term for the current goal is (SepI Xi_i (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxXi HfxV).
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 HxX: x ∈ X.
An exact proof term for the current goal is (HXiSub x HxXi).
We prove the intermediate claim HxPre: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HfxV).
An exact proof term for the current goal is (binintersectI (preimage_of X f V) Xi_i x HxPre HxXi).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is Hprei.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) (preimage_of X f V) HprePow HpreAll).
∎