Let X, Tx, Y, Ty, A and B be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HA: A ⊆ X.
Assume HB: B ⊆ Y.
We will prove product_topology A (subspace_topology X Tx A) B (subspace_topology Y Ty B) = subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B).
Set Bx to be the term {U ∩ A|U ∈ Tx}.
Set By to be the term {V ∩ B|V ∈ Ty}.
Set C to be the term product_basis_from Bx By.
We prove the intermediate claim HgenTx: basis_on X Tx ∧ generated_topology X Tx = Tx.
We will prove basis_on X Tx ∧ generated_topology X Tx = Tx.
Apply (basis_refines_topology X Tx Tx HTx) to the current goal.
Let c be given.
Assume Hc: c ∈ Tx.
An exact proof term for the current goal is Hc.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume Hx: x ∈ U.
We will prove ∃Cx ∈ Tx, x ∈ Cx ∧ Cx ⊆ U.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (Subq_ref U).
We prove the intermediate claim HgenTy: basis_on Y Ty ∧ generated_topology Y Ty = Ty.
We will prove basis_on Y Ty ∧ generated_topology Y Ty = Ty.
Apply (basis_refines_topology Y Ty Ty HTy) to the current goal.
Let c be given.
Assume Hc: c ∈ Ty.
An exact proof term for the current goal is Hc.
Let U be given.
Assume HU: U ∈ Ty.
Let x be given.
Assume Hx: x ∈ U.
We will prove ∃Cx ∈ Ty, x ∈ Cx ∧ Cx ⊆ U.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (Subq_ref U).
We prove the intermediate claim HBx: basis_on A Bx ∧ generated_topology A Bx = subspace_topology X Tx A.
An exact proof term for the current goal is (subspace_basis X Tx A Tx HTx HA HgenTx).
We prove the intermediate claim HBy: basis_on B By ∧ generated_topology B By = subspace_topology Y Ty B.
An exact proof term for the current goal is (subspace_basis Y Ty B Ty HTy HB HgenTy).
We prove the intermediate claim HBx_basis: basis_on A Bx.
An exact proof term for the current goal is (andEL (basis_on A Bx) (generated_topology A Bx = subspace_topology X Tx A) HBx).
We prove the intermediate claim HBy_basis: basis_on B By.
An exact proof term for the current goal is (andEL (basis_on B By) (generated_topology B By = subspace_topology Y Ty B) HBy).
We prove the intermediate claim HBx_eq: generated_topology A Bx = subspace_topology X Tx A.
An exact proof term for the current goal is (andER (basis_on A Bx) (generated_topology A Bx = subspace_topology X Tx A) HBx).
We prove the intermediate claim HBy_eq: generated_topology B By = subspace_topology Y Ty B.
An exact proof term for the current goal is (andER (basis_on B By) (generated_topology B By = subspace_topology Y Ty B) HBy).
We prove the intermediate claim Hprod_gen: generated_topology (setprod A B) C = product_topology A (subspace_topology X Tx A) B (subspace_topology Y Ty B).
An exact proof term for the current goal is (product_basis_generates_product_topology A B Bx By (subspace_topology X Tx A) (subspace_topology Y Ty B) HBx_basis HBx_eq HBy_basis HBy_eq).
We prove the intermediate claim HABsub: setprod A B ⊆ setprod X Y.
An exact proof term for the current goal is (setprod_Subq A B X Y HA HB).
We prove the intermediate claim HtopProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HtopSubProd: topology_on (setprod A B) (subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B)).
An exact proof term for the current goal is (subspace_topology_is_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B) HtopProd HABsub).
We prove the intermediate claim HCsub: ∀c ∈ C, c ∈ subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B).
Let c be given.
Assume HcC.
We prove the intermediate claim HexU: ∃U ∈ Bx, c ∈ {setprod U V|V ∈ By}.
An exact proof term for the current goal is (famunionE Bx (λU0 : set ⇒ {setprod U0 V|V ∈ By}) c HcC).
Apply HexU to the current goal.
Let U be given.
Assume HUconj.
We prove the intermediate claim HUbx: U ∈ Bx.
An exact proof term for the current goal is (andEL (U ∈ Bx) (c ∈ {setprod U V|V ∈ By}) HUconj).
We prove the intermediate claim HcRepl: c ∈ {setprod U V|V ∈ By}.
An exact proof term for the current goal is (andER (U ∈ Bx) (c ∈ {setprod U V|V ∈ By}) HUconj).
We prove the intermediate claim HexV: ∃V ∈ By, c = setprod U V.
An exact proof term for the current goal is (ReplE By (λV0 : set ⇒ setprod U V0) c HcRepl).
Apply HexV to the current goal.
Let V be given.
Assume HVconj.
We prove the intermediate claim HVby: V ∈ By.
An exact proof term for the current goal is (andEL (V ∈ By) (c = setprod U V) HVconj).
We prove the intermediate claim HcEqUV: c = setprod U V.
An exact proof term for the current goal is (andER (V ∈ By) (c = setprod U V) HVconj).
We prove the intermediate claim HexUx: ∃U0 ∈ Tx, U = U0 ∩ A.
An exact proof term for the current goal is (ReplE Tx (λU0 : set ⇒ U0 ∩ A) U HUbx).
We prove the intermediate claim HexVy: ∃V0 ∈ Ty, V = V0 ∩ B.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ V0 ∩ B) V HVby).
Apply HexUx to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (U = U0 ∩ A) HU0conj).
We prove the intermediate claim HUeq: U = U0 ∩ A.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (U = U0 ∩ A) HU0conj).
Apply HexVy to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (andEL (V0 ∈ Ty) (V = V0 ∩ B) HV0conj).
We prove the intermediate claim HVeq: V = V0 ∩ B.
An exact proof term for the current goal is (andER (V0 ∈ Ty) (V = V0 ∩ B) HV0conj).
Set W to be the term setprod U0 V0.
We prove the intermediate claim HWsub: W ∈ product_subbasis X Tx Y Ty.
We will prove W ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HWV: rectangle_set U0 V0 ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV1 : set ⇒ rectangle_set U0 V1) V0 HV0Ty).
An exact proof term for the current goal is (famunionI Tx (λU1 : set ⇒ {rectangle_set U1 V|V ∈ Ty}) U0 (rectangle_set U0 V0) HU0Tx HWV).
We prove the intermediate claim HBsubbasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HWopen: W ∈ product_topology X Tx Y Ty.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBsubbasis W HWsub).
We prove the intermediate claim HcPow: c ∈ 𝒫 (setprod A B).
Apply PowerI (setprod A B) c to the current goal.
Let p be given.
Assume Hp: p ∈ c.
We will prove p ∈ setprod A B.
We prove the intermediate claim HpUV: p ∈ setprod U V.
We will prove p ∈ setprod U V.
rewrite the current goal using HcEqUV (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim HsubU: U ⊆ A.
We will prove U ⊆ A.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersect_Subq_2 U0 A).
We prove the intermediate claim HsubV: V ⊆ B.
We will prove V ⊆ B.
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is (binintersect_Subq_2 V0 B).
We prove the intermediate claim HsubUV: setprod U V ⊆ setprod A B.
An exact proof term for the current goal is (setprod_Subq U V A B HsubU HsubV).
An exact proof term for the current goal is (HsubUV p HpUV).
We prove the intermediate claim HcEqSub: c = W ∩ setprod A B.
We will prove c = W ∩ setprod A B.
rewrite the current goal using HcEqUV (from left to right).
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using HVeq (from left to right).
rewrite the current goal using (setprod_intersection U0 V0 A B) (from right to left).
Use reflexivity.
We prove the intermediate claim HexW: ∃V1 ∈ product_topology X Tx Y Ty, c = V1 ∩ setprod A B.
We use W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HWopen.
An exact proof term for the current goal is HcEqSub.
An exact proof term for the current goal is (SepI (𝒫 (setprod A B)) (λU1 : set ⇒ ∃V1 ∈ product_topology X Tx Y Ty, U1 = V1 ∩ setprod A B) c HcPow HexW).
We prove the intermediate claim Href: ∀U1 ∈ subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B), ∀p ∈ U1, ∃Cx ∈ C, p ∈ Cx ∧ Cx ⊆ U1.
Let U1 be given.
Assume HU1: U1 ∈ subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B).
Let p be given.
Assume HpU1: p ∈ U1.
We prove the intermediate claim HU1sub: U1 ⊆ setprod A B.
An exact proof term for the current goal is (PowerE (setprod A B) U1 (SepE1 (𝒫 (setprod A B)) (λU0 : set ⇒ ∃V0 ∈ product_topology X Tx Y Ty, U0 = V0 ∩ setprod A B) U1 HU1)).
We prove the intermediate claim HpAB: p ∈ setprod A B.
An exact proof term for the current goal is (HU1sub p HpU1).
We prove the intermediate claim HU1prop: ∃W ∈ product_topology X Tx Y Ty, U1 = W ∩ setprod A B.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod A B)) (λU0 : set ⇒ ∃V0 ∈ product_topology X Tx Y Ty, U0 = V0 ∩ setprod A B) U1 HU1).
Apply HU1prop to the current goal.
Let W be given.
Assume HWconj.
We prove the intermediate claim HWopen: W ∈ product_topology X Tx Y Ty.
An exact proof term for the current goal is (andEL (W ∈ product_topology X Tx Y Ty) (U1 = W ∩ setprod A B) HWconj).
We prove the intermediate claim HU1eq: U1 = W ∩ setprod A B.
An exact proof term for the current goal is (andER (W ∈ product_topology X Tx Y Ty) (U1 = W ∩ setprod A B) HWconj).
We prove the intermediate claim HpWAB: p ∈ W ∩ setprod A B.
rewrite the current goal using HU1eq (from right to left).
An exact proof term for the current goal is HpU1.
We prove the intermediate claim HpW: p ∈ W.
An exact proof term for the current goal is (binintersectE1 W (setprod A B) p HpWAB).
We prove the intermediate claim HWgen: W ∈ generated_topology (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is HWopen.
We prove the intermediate claim HWref: ∀z ∈ W, ∃b ∈ product_subbasis X Tx Y Ty, z ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀z0 ∈ U0, ∃b0 ∈ product_subbasis X Tx Y Ty, z0 ∈ b0 ∧ b0 ⊆ U0) W HWgen).
We prove the intermediate claim Hexb: ∃b ∈ product_subbasis X Tx Y Ty, p ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (HWref p HpW).
Apply Hexb to the current goal.
Let b be given.
Assume Hbconj.
We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (andEL (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ W) Hbconj).
We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ W.
An exact proof term for the current goal is (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ W) Hbconj).
We prove the intermediate claim Hpb: p ∈ b.
An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ W) Hbprop).
We prove the intermediate claim HbsubW: b ⊆ W.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ W) Hbprop).
We prove the intermediate claim HexU: ∃U0 ∈ Tx, b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbSub).
Apply HexU to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HexV: ∃V0 ∈ Ty, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).
Apply HexV to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
Set Cx to be the term setprod (U0 ∩ A) (V0 ∩ B).
We use Cx to witness the existential quantifier.
Apply andI to the current goal.
We will prove Cx ∈ C.
We prove the intermediate claim HU0Bx: U0 ∩ A ∈ Bx.
An exact proof term for the current goal is (ReplI Tx (λU1 : set ⇒ U1 ∩ A) U0 HU0Tx).
We prove the intermediate claim HV0By: V0 ∩ B ∈ By.
An exact proof term for the current goal is (ReplI Ty (λV1 : set ⇒ V1 ∩ B) V0 HV0Ty).
We prove the intermediate claim HcxRepl: setprod (U0 ∩ A) (V0 ∩ B) ∈ {setprod (U0 ∩ A) V|V ∈ By}.
An exact proof term for the current goal is (ReplI By (λV1 : set ⇒ setprod (U0 ∩ A) V1) (V0 ∩ B) HV0By).
An exact proof term for the current goal is (famunionI Bx (λU1 : set ⇒ {setprod U1 V|V ∈ By}) (U0 ∩ A) (setprod (U0 ∩ A) (V0 ∩ B)) HU0Bx HcxRepl).
Apply andI to the current goal.
We will prove p ∈ Cx.
We prove the intermediate claim HpInInter: p ∈ (rectangle_set U0 V0) ∩ setprod A B.
We will prove p ∈ (rectangle_set U0 V0) ∩ setprod A B.
Apply binintersectI to the current goal.
We will prove p ∈ rectangle_set U0 V0.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hpb.
An exact proof term for the current goal is HpAB.
rewrite the current goal using (setprod_intersection U0 V0 A B) (from right to left).
An exact proof term for the current goal is HpInInter.
We will prove Cx ⊆ U1.
We prove the intermediate claim HCx_sub_b: Cx ⊆ rectangle_set U0 V0.
An exact proof term for the current goal is (setprod_Subq (U0 ∩ A) (V0 ∩ B) U0 V0 (binintersect_Subq_1 U0 A) (binintersect_Subq_1 V0 B)).
We prove the intermediate claim HCx_sub_W: Cx ⊆ W.
We prove the intermediate claim HrectSubb: rectangle_set U0 V0 ⊆ b.
We will prove rectangle_set U0 V0 ⊆ b.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is (Subq_ref b).
An exact proof term for the current goal is (Subq_tra Cx (rectangle_set U0 V0) W HCx_sub_b (Subq_tra (rectangle_set U0 V0) b W HrectSubb HbsubW)).
We prove the intermediate claim HCx_sub_AB: Cx ⊆ setprod A B.
An exact proof term for the current goal is (setprod_Subq (U0 ∩ A) (V0 ∩ B) A B (binintersect_Subq_2 U0 A) (binintersect_Subq_2 V0 B)).
We prove the intermediate claim HCx_sub_WAB: Cx ⊆ W ∩ setprod A B.
An exact proof term for the current goal is (binintersect_Subq_max W (setprod A B) Cx HCx_sub_W HCx_sub_AB).
rewrite the current goal using HU1eq (from left to right).
An exact proof term for the current goal is HCx_sub_WAB.
We prove the intermediate claim HsubEq: generated_topology (setprod A B) C = subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B).
An exact proof term for the current goal is (andER (basis_on (setprod A B) C) (generated_topology (setprod A B) C = subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B)) (basis_refines_topology (setprod A B) (subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod A B)) C HtopSubProd HCsub Href)).
rewrite the current goal using Hprod_gen (from right to left).
rewrite the current goal using HsubEq (from left to right).
Use reflexivity.
∎