Let X, Tx, Y, Ty, Z and Tz be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HTz: topology_on Z Tz.
We will prove (∀y0 : set, y0 ∈ Y → continuous_map X Tx Y Ty (const_fun X y0)) ∧ (∀A : set, A ⊆ X → continuous_map A (subspace_topology X Tx A) X Tx {(y,y)|y ∈ A}) ∧ (∀f g : set, continuous_map X Tx Y Ty f → continuous_map Y Ty Z Tz g → continuous_map X Tx Z Tz (compose_fun X f g)) ∧ (∀f A : set, A ⊆ X → continuous_map X Tx Y Ty f → continuous_map A (subspace_topology X Tx A) Y Ty f) ∧ ((∀f Z0 : set, continuous_map X Tx Y Ty f → Z0 ⊆ Y → (∀x : set, x ∈ X → apply_fun f x ∈ Z0) → continuous_map X Tx Z0 (subspace_topology Y Ty Z0) f) ∧ (∀f Z0 Tz0 : set, continuous_map X Tx Y Ty f → Y ⊆ Z0 → topology_on Z0 Tz0 → Ty = subspace_topology Z0 Tz0 Y → continuous_map X Tx Z0 Tz0 f)) ∧ (∀f : set, (∃UFam : set, UFam ⊆ Tx ∧ ⋃ UFam = X ∧ (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f)) → continuous_map X Tx Y Ty f).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let y0 be given.
Assume Hy0: y0 ∈ Y.
An exact proof term for the current goal is (const_fun_continuous X Tx Y Ty y0 HTx HTy Hy0).
Let A be given.
Assume HA: A ⊆ X.
Set j to be the term {(y,y)|y ∈ A}.
We will prove continuous_map A (subspace_topology X Tx A) X Tx j.
We will prove topology_on A (subspace_topology X Tx A) ∧ topology_on X Tx ∧ function_on j A X ∧ ∀V : set, V ∈ Tx → preimage_of A j V ∈ subspace_topology X Tx A.
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 (subspace_topology_is_topology X Tx A HTx HA).
An exact proof term for the current goal is HTx.
Let a be given.
Assume HaA: a ∈ A.
We will prove apply_fun j a ∈ X.
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
rewrite the current goal using Haj (from left to right).
An exact proof term for the current goal is (HA a HaA).
Let V be given.
Assume HV: V ∈ Tx.
We will prove preimage_of A j V ∈ subspace_topology X Tx A.
We prove the intermediate claim Heq: preimage_of A j V = V ∩ A.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A j V.
We will prove a ∈ V ∩ A.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λu : set ⇒ apply_fun j u ∈ V) a Ha).
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using Haj (from right to left).
An exact proof term for the current goal is (SepE2 A (λu : set ⇒ apply_fun j u ∈ V) a Ha).
An exact proof term for the current goal is (binintersectI V A a HaV HaA).
Let a be given.
Assume Ha: a ∈ V ∩ A.
We will prove a ∈ preimage_of A j V.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (binintersectE1 V A a Ha).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 V A a Ha).
We will prove a ∈ {u ∈ A|apply_fun j u ∈ V}.
Apply (SepI A (λu : set ⇒ apply_fun j u ∈ V) a HaA) to the current goal.
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
rewrite the current goal using Haj (from left to right).
An exact proof term for the current goal is HaV.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HVpow: (V ∩ A) ∈ 𝒫 A.
Apply PowerI to the current goal.
Let a be given.
Assume Ha: a ∈ V ∩ A.
An exact proof term for the current goal is (binintersectE2 V A a Ha).
We prove the intermediate claim HexW: ∃W ∈ Tx, V ∩ A = W ∩ A.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ A) (V ∩ A) HVpow HexW).
Let f be given.
Let g be given.
Assume Hf.
Assume Hg.
An exact proof term for the current goal is (composition_continuous X Tx Y Ty Z Tz f g Hf Hg).
Let f be given.
Let A be given.
Assume HA.
Assume Hf.
We will prove continuous_map A (subspace_topology X Tx A) Y Ty f.
We prove the intermediate claim HTA: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).
We prove the intermediate claim HpreX: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER (((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y)) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim Htmp: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (andEL (((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y)) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim HfunXY: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Htmp).
We will prove (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty ∧ function_on f A Y) ∧ ∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A.
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 HTA.
An exact proof term for the current goal is HTy.
Let a be given.
Assume HaA: a ∈ A.
We will prove apply_fun f a ∈ Y.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HA a HaA).
An exact proof term for the current goal is (HfunXY a HaX).
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of A f V ∈ subspace_topology X Tx A.
We prove the intermediate claim HWTx: preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (HpreX V HV).
We prove the intermediate claim Heq: preimage_of A f V = (preimage_of X f V) ∩ A.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A f V.
We will prove a ∈ (preimage_of X f V) ∩ A.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λu : set ⇒ apply_fun f u ∈ V) a Ha).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HA a HaA).
We prove the intermediate claim HafV: apply_fun f a ∈ V.
An exact proof term for the current goal is (SepE2 A (λu : set ⇒ apply_fun f u ∈ V) a Ha).
We prove the intermediate claim HaPreX: a ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) a HaX HafV).
An exact proof term for the current goal is (binintersectI (preimage_of X f V) A a HaPreX HaA).
Let a be given.
Assume Ha: a ∈ (preimage_of X f V) ∩ A.
We will prove a ∈ preimage_of A f V.
We prove the intermediate claim HaPreX: a ∈ preimage_of X f V.
An exact proof term for the current goal is (binintersectE1 (preimage_of X f V) A a Ha).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 (preimage_of X f V) A a Ha).
We prove the intermediate claim HafV: apply_fun f a ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) a HaPreX).
An exact proof term for the current goal is (SepI A (λu : set ⇒ apply_fun f u ∈ V) a HaA HafV).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hpow: ((preimage_of X f V) ∩ A) ∈ 𝒫 A.
Apply PowerI to the current goal.
Let a be given.
Assume Ha: a ∈ (preimage_of X f V) ∩ A.
An exact proof term for the current goal is (binintersectE2 (preimage_of X f V) A a Ha).
We prove the intermediate claim HexW: ∃W ∈ Tx, (preimage_of X f V) ∩ A = W ∩ A.
We use (preimage_of X f V) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HWTx.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ A) ((preimage_of X f V) ∩ A) Hpow HexW).
Apply andI to the current goal.
Let f be given.
Let Z0 be given.
Assume Hf.
Assume HZ0.
Assume Himg.
We will prove continuous_map X Tx Z0 (subspace_topology Y Ty Z0) f.
We prove the intermediate claim HpreY: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER (((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y)) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim HTz0: topology_on Z0 (subspace_topology Y Ty Z0).
An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Z0 HTy HZ0).
We prove the intermediate claim HfunXZ0: function_on f X Z0.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Himg x HxX).
We will prove (topology_on X Tx ∧ topology_on Z0 (subspace_topology Y Ty Z0) ∧ function_on f X Z0) ∧ ∀B : set, B ∈ subspace_topology Y Ty Z0 → preimage_of X f B ∈ Tx.
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 HTx.
An exact proof term for the current goal is HTz0.
An exact proof term for the current goal is HfunXZ0.
Let B be given.
Assume HB: B ∈ subspace_topology Y Ty Z0.
We prove the intermediate claim Hex: ∃V ∈ Ty, B = V ∩ Z0.
An exact proof term for the current goal is (subspace_topologyE Y Ty Z0 B HB).
Apply Hex to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HV: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (B = V ∩ Z0) HVpair).
We prove the intermediate claim HB_eq: B = V ∩ Z0.
An exact proof term for the current goal is (andER (V ∈ Ty) (B = V ∩ Z0) HVpair).
We prove the intermediate claim HeqPre: preimage_of X f B = preimage_of X f V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f B.
We will prove x ∈ preimage_of X f V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ B) x Hx).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ B) x Hx).
We prove the intermediate claim HfxVz0: apply_fun f x ∈ V ∩ Z0.
rewrite the current goal using HB_eq (from right to left).
An exact proof term for the current goal is HfxB.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Z0 (apply_fun f x) HfxVz0).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x HxX HfxV).
Let x be given.
Assume Hx: x ∈ preimage_of X f V.
We will prove x ∈ preimage_of X f B.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim HfxZ0: apply_fun f x ∈ Z0.
An exact proof term for the current goal is (HfunXZ0 x HxX).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
rewrite the current goal using HB_eq (from left to right).
An exact proof term for the current goal is (binintersectI V Z0 (apply_fun f x) HfxV HfxZ0).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ B) x HxX HfxB).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (HpreY V HV).
Let f be given.
Let Z0 be given.
Let Tz0 be given.
Assume Hf: continuous_map X Tx Y Ty f.
Assume HYZ0: Y ⊆ Z0.
Assume HTz0: topology_on Z0 Tz0.
Assume HTy_eq: Ty = subspace_topology Z0 Tz0 Y.
We will prove continuous_map X Tx Z0 Tz0 f.
We prove the intermediate claim HpreY: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER (((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y)) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim Htmp: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (andEL (((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y)) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim HfunXY: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Htmp).
We prove the intermediate claim HfunXZ0: function_on f X Z0.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (HYZ0 (apply_fun f x) (HfunXY x HxX)).
We will prove (topology_on X Tx ∧ topology_on Z0 Tz0 ∧ function_on f X Z0) ∧ ∀W : set, W ∈ Tz0 → preimage_of X f W ∈ Tx.
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 HTx.
An exact proof term for the current goal is HTz0.
An exact proof term for the current goal is HfunXZ0.
Let W be given.
Assume HW: W ∈ Tz0.
Set B to be the term W ∩ Y.
We prove the intermediate claim HB_inTy: B ∈ Ty.
rewrite the current goal using HTy_eq (from left to right).
We prove the intermediate claim HBpow: B ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 W Y y HyB).
We prove the intermediate claim Hex: ∃V ∈ Tz0, B = V ∩ Y.
We use W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HW.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tz0, U0 = V ∩ Y) B HBpow Hex).
We prove the intermediate claim HeqPre: preimage_of X f W = preimage_of X f B.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f W.
We will prove x ∈ preimage_of X f B.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ W) x Hx).
We prove the intermediate claim HfxW: apply_fun f x ∈ W.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ W) x Hx).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (HfunXY x HxX).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
An exact proof term for the current goal is (binintersectI W Y (apply_fun f x) HfxW HfxY).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ B) x HxX HfxB).
Let x be given.
Assume Hx: x ∈ preimage_of X f B.
We will prove x ∈ preimage_of X f W.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ B) x Hx).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ B) x Hx).
We prove the intermediate claim HfxW: apply_fun f x ∈ W.
An exact proof term for the current goal is (binintersectE1 W Y (apply_fun f x) HfxB).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ W) x HxX HfxW).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (HpreY B HB_inTy).
Let f be given.
Assume Hloc.
We will prove continuous_map X Tx Y Ty f.
Apply Hloc to the current goal.
Let UFam be given.
Assume HUFconj.
We prove the intermediate claim HUFpair: (UFam ⊆ Tx ∧ ⋃ UFam = X) ∧ (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f).
An exact proof term for the current goal is HUFconj.
We prove the intermediate claim HUFsub_union: UFam ⊆ Tx ∧ ⋃ UFam = X.
An exact proof term for the current goal is (andEL (UFam ⊆ Tx ∧ ⋃ UFam = X) (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f) HUFpair).
We prove the intermediate claim HcontU: ∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f.
An exact proof term for the current goal is (andER (UFam ⊆ Tx ∧ ⋃ UFam = X) (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f) HUFpair).
We prove the intermediate claim HUFsub: UFam ⊆ Tx.
An exact proof term for the current goal is (andEL (UFam ⊆ Tx) (⋃ UFam = X) HUFsub_union).
We prove the intermediate claim HUnionEq: ⋃ UFam = X.
An exact proof term for the current goal is (andER (UFam ⊆ Tx) (⋃ UFam = X) HUFsub_union).
We prove the intermediate claim HfunXY: function_on f X Y.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HxUnion: x ∈ ⋃ UFam.
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HxX.
Apply (UnionE UFam x HxUnion) to the current goal.
Let U be given.
Assume HxUconj.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ UFam) HxUconj).
We prove the intermediate claim HUUF: U ∈ UFam.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ UFam) HxUconj).
We prove the intermediate claim HcU: continuous_map U (subspace_topology X Tx U) Y Ty f.
An exact proof term for the current goal is (HcontU U HUUF).
We prove the intermediate claim Htmp: (topology_on U (subspace_topology X Tx U) ∧ topology_on Y Ty) ∧ function_on f U Y.
An exact proof term for the current goal is (andEL ((topology_on U (subspace_topology X Tx U) ∧ topology_on Y Ty) ∧ function_on f U Y) (∀V : set, V ∈ Ty → preimage_of U f V ∈ subspace_topology X Tx U) HcU).
We prove the intermediate claim HfunUY: function_on f U Y.
An exact proof term for the current goal is (andER (topology_on U (subspace_topology X Tx U) ∧ topology_on Y Ty) (function_on f U Y) Htmp).
An exact proof term for the current goal is (HfunUY x HxU).
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.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is HfunXY.
Let V be given.
Assume HV: V ∈ Ty.
Set S to be the term preimage_of X f V.
Set Fam to be the term {W ∈ 𝒫 X|W ∈ Tx ∧ W ⊆ S}.
We prove the intermediate claim HFamSubTx: Fam ⊆ Tx.
Let W be given.
Assume HW: W ∈ Fam.
We prove the intermediate claim HWpred: W ∈ Tx ∧ W ⊆ S.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λW0 : set ⇒ W0 ∈ Tx ∧ W0 ⊆ S) W HW).
An exact proof term for the current goal is (andEL (W ∈ Tx) (W ⊆ S) HWpred).
We prove the intermediate claim HUnionFamEq: ⋃ Fam = S.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ Fam.
We will prove x ∈ S.
Apply (UnionE Fam x Hx) to the current goal.
Let W be given.
Assume HxWconj.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (andEL (x ∈ W) (W ∈ Fam) HxWconj).
We prove the intermediate claim HWFam: W ∈ Fam.
An exact proof term for the current goal is (andER (x ∈ W) (W ∈ Fam) HxWconj).
We prove the intermediate claim HWpred: W ∈ Tx ∧ W ⊆ S.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λW0 : set ⇒ W0 ∈ Tx ∧ W0 ⊆ S) W HWFam).
We prove the intermediate claim HWsubS: W ⊆ S.
An exact proof term for the current goal is (andER (W ∈ Tx) (W ⊆ S) HWpred).
An exact proof term for the current goal is (HWsubS x HxW).
Let x be given.
Assume Hx: x ∈ S.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim HxUnion: x ∈ ⋃ UFam.
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HxX.
Apply (UnionE UFam x HxUnion) to the current goal.
Let U be given.
Assume HxUconj.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ UFam) HxUconj).
We prove the intermediate claim HUUF: U ∈ UFam.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ UFam) HxUconj).
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (HUFsub U HUUF).
We prove the intermediate claim HUSubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUTx).
We prove the intermediate claim HcU: continuous_map U (subspace_topology X Tx U) Y Ty f.
An exact proof term for the current goal is (HcontU U HUUF).
We prove the intermediate claim HpreU: preimage_of U f V ∈ subspace_topology X Tx U.
An exact proof term for the current goal is (andER (((topology_on U (subspace_topology X Tx U) ∧ topology_on Y Ty) ∧ function_on f U Y)) (∀V0 : set, V0 ∈ Ty → preimage_of U f V0 ∈ subspace_topology X Tx U) HcU V HV).
We prove the intermediate claim HexW0: ∃W0 ∈ Tx, preimage_of U f V = W0 ∩ U.
An exact proof term for the current goal is (SepE2 (𝒫 U) (λU0 : set ⇒ ∃W0 ∈ Tx, U0 = W0 ∩ U) (preimage_of U f V) HpreU).
Apply HexW0 to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0Tx: W0 ∈ Tx.
An exact proof term for the current goal is (andEL (W0 ∈ Tx) (preimage_of U f V = W0 ∩ U) HW0pair).
We prove the intermediate claim HeqPreU: preimage_of U f V = W0 ∩ U.
An exact proof term for the current goal is (andER (W0 ∈ Tx) (preimage_of U f V = W0 ∩ U) HW0pair).
Set W to be the term W0 ∩ U.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim HxPreU: x ∈ preimage_of U f V.
We will prove x ∈ {u ∈ U|apply_fun f u ∈ V}.
Apply (SepI U (λu : set ⇒ apply_fun f u ∈ V) x HxU) to the current goal.
An exact proof term for the current goal is HfxV.
We prove the intermediate claim HxW: x ∈ W.
rewrite the current goal using HeqPreU (from right to left).
An exact proof term for the current goal is HxPreU.
We prove the intermediate claim HWsubS: W ⊆ S.
Let z be given.
Assume Hz: z ∈ W.
We will prove z ∈ S.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE2 W0 U z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HUSubX z HzU).
We prove the intermediate claim HzPreU: z ∈ preimage_of U f V.
rewrite the current goal using HeqPreU (from left to right).
An exact proof term for the current goal is Hz.
We prove the intermediate claim HfzV: apply_fun f z ∈ V.
An exact proof term for the current goal is (SepE2 U (λu : set ⇒ apply_fun f u ∈ V) z HzPreU).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) z HzX HfzV).
We prove the intermediate claim HWpow: W ∈ 𝒫 X.
Apply PowerI to the current goal.
Let z be given.
Assume Hz: z ∈ W.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE2 W0 U z Hz).
An exact proof term for the current goal is (HUSubX z HzU).
We prove the intermediate claim HWFam: W ∈ Fam.
An exact proof term for the current goal is (SepI (𝒫 X) (λW1 : set ⇒ W1 ∈ Tx ∧ W1 ⊆ S) W HWpow (andI (W ∈ Tx) (W ⊆ S) (topology_binintersect_closed X Tx W0 U HTx HW0Tx HUTx) HWsubS)).
An exact proof term for the current goal is (UnionI Fam x W HxW HWFam).
rewrite the current goal using HUnionFamEq (from right to left).
An exact proof term for the current goal is (topology_union_closed X Tx Fam HTx HFamSubTx).
∎