Let x0, Tx and Ty be given.
Assume HTx: topology_on R Tx.
Assume HTy: topology_on R Ty.
Assume Hx0R: x0 ∈ R.
Set X to be the term EuclidPlane.
Set A to be the term setprod {x0} R.
Set Tprod to be the term product_topology R Tx R Ty.
Set Ta to be the term subspace_topology X Tprod A.
We prove the intermediate claim HTprod: topology_on X Tprod.
An exact proof term for the current goal is (product_topology_is_topology R Tx R Ty HTx HTy).
We prove the intermediate claim HAsub: A ⊆ X.
Let p be given.
Assume HpA: p ∈ A.
We will prove p ∈ X.
We prove the intermediate claim HSingSub: {x0} ⊆ R.
An exact proof term for the current goal is (singleton_subset x0 R Hx0R).
An exact proof term for the current goal is (setprod_Subq {x0} R R R HSingSub (Subq_ref R) p HpA).
We prove the intermediate claim HTa: topology_on A Ta.
An exact proof term for the current goal is (subspace_topology_is_topology X Tprod A HTprod HAsub).
We will prove continuous_map A Ta R Ty (projection2 R R).
We will prove topology_on A Ta ∧ topology_on R Ty ∧ function_on (projection2 R R) A R ∧ ∀V : set, V ∈ Ty → preimage_of A (projection2 R R) V ∈ Ta.
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 p be given.
Assume HpA: p ∈ A.
We will prove apply_fun (projection2 R R) p ∈ R.
We prove the intermediate claim HpRR: p ∈ setprod R R.
We prove the intermediate claim HSingSub: {x0} ⊆ R.
An exact proof term for the current goal is (singleton_subset x0 R Hx0R).
An exact proof term for the current goal is (setprod_Subq {x0} R R R HSingSub (Subq_ref R) p HpA).
We prove the intermediate claim Happ: apply_fun (projection2 R R) p = p 1.
An exact proof term for the current goal is (projection2_apply R R p HpRR).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ R) p HpA).
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of A (projection2 R R) V ∈ Ta.
Set U to be the term preimage_of X (projection2 R R) V.
We prove the intermediate claim HcontFull: continuous_map X Tprod R Ty (projection2 R R).
An exact proof term for the current goal is (projection2_continuous_in_product R Tx R Ty HTx HTy).
We prove the intermediate claim HUopen: U ∈ Tprod.
An exact proof term for the current goal is (continuous_map_preimage X Tprod R Ty (projection2 R R) HcontFull V HV).
We prove the intermediate claim HeqPre: preimage_of A (projection2 R R) V = U ∩ A.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ preimage_of A (projection2 R R) V.
We will prove p ∈ U ∩ A.
We prove the intermediate claim HpA: p ∈ A.
An exact proof term for the current goal is (SepE1 A (λq : set ⇒ apply_fun (projection2 R R) q ∈ V) p Hp).
We prove the intermediate claim HpRR: p ∈ setprod R R.
We prove the intermediate claim HSingSub: {x0} ⊆ R.
An exact proof term for the current goal is (singleton_subset x0 R Hx0R).
An exact proof term for the current goal is (setprod_Subq {x0} R R R HSingSub (Subq_ref R) p HpA).
We prove the intermediate claim HprojV: apply_fun (projection2 R R) p ∈ V.
An exact proof term for the current goal is (SepE2 A (λq : set ⇒ apply_fun (projection2 R R) q ∈ V) p Hp).
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is HpRR.
We prove the intermediate claim HpU: p ∈ U.
An exact proof term for the current goal is (SepI X (λq : set ⇒ apply_fun (projection2 R R) q ∈ V) p HpX HprojV).
An exact proof term for the current goal is (binintersectI U A p HpU HpA).
Let p be given.
Assume Hp: p ∈ U ∩ A.
We will prove p ∈ preimage_of A (projection2 R R) V.
We prove the intermediate claim HpU: p ∈ U.
An exact proof term for the current goal is (binintersectE1 U A p Hp).
We prove the intermediate claim HpA: p ∈ A.
An exact proof term for the current goal is (binintersectE2 U A p Hp).
We prove the intermediate claim HprojV: apply_fun (projection2 R R) p ∈ V.
An exact proof term for the current goal is (SepE2 X (λq : set ⇒ apply_fun (projection2 R R) q ∈ V) p HpU).
An exact proof term for the current goal is (SepI A (λq : set ⇒ apply_fun (projection2 R R) q ∈ V) p HpA HprojV).
rewrite the current goal using HeqPre (from left to right).
We prove the intermediate claim Hpow: (U ∩ A) ∈ 𝒫 A.
Apply PowerI to the current goal.
Let p be given.
Assume Hp: p ∈ U ∩ A.
An exact proof term for the current goal is (binintersectE2 U A p Hp).
We prove the intermediate claim HexW: ∃W ∈ Tprod, U ∩ A = W ∩ A.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tprod, U0 = W ∩ A) (U ∩ A) Hpow HexW).
∎