Let X, Tx, Y, Ty, f and Z0 be given.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume HZ0sub: Z0 ⊆ Y.
Assume Himg: ∀x : set, x ∈ X → apply_fun f x ∈ Z0.
Set Tz0 to be the term subspace_topology Y Ty Z0.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f Hcont).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (continuous_map_topology_cod X Tx Y Ty f Hcont).
We prove the intermediate claim HTz0: topology_on Z0 Tz0.
An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Z0 HTy HZ0sub).
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 continuous_map X Tx Z0 Tz0 f.
We will prove topology_on X Tx ∧ topology_on Z0 Tz0 ∧ function_on f X Z0 ∧ ∀B : set, B ∈ Tz0 → 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 ∈ Tz0.
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 (Himg 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 (continuous_map_preimage X Tx Y Ty f Hcont V HV).
∎