Let X, Y, Bx, By, Tx and Ty be given.
Assume HBx_basis: basis_on X Bx.
Assume HTx_eq: generated_topology X Bx = Tx.
Assume HBy_basis: basis_on Y By.
Assume HTy_eq: generated_topology Y By = Ty.
We prove the intermediate claim HTx: topology_on X Tx.
rewrite the current goal using HTx_eq (from right to left).
An exact proof term for the current goal is (lemma_topology_from_basis X Bx HBx_basis).
We prove the intermediate claim HTy: topology_on Y Ty.
rewrite the current goal using HTy_eq (from right to left).
An exact proof term for the current goal is (lemma_topology_from_basis Y By HBy_basis).
We prove the intermediate claim HTprod: 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 HCsub: ∀c ∈ product_basis_from Bx By, c ∈ product_topology X Tx Y Ty.
Let c be given.
Assume HcC.
We prove the intermediate claim HBprod: 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 HexU: ∃U ∈ Bx, c ∈ {setprod U V|V ∈ By}.
An exact proof term for the current goal is (famunionE Bx (λU0 : set ⇒ {setprod U0 V0|V0 ∈ By}) c HcC).
Apply HexU to the current goal.
Let U be given.
Assume HUconj: U ∈ Bx ∧ c ∈ {setprod U V|V ∈ By}.
We prove the intermediate claim HU: 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: V ∈ By ∧ c = setprod U V.
We prove the intermediate claim HV: V ∈ By.
An exact proof term for the current goal is (andEL (V ∈ By) (c = setprod U V) HVconj).
We prove the intermediate claim Hceq: 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 HUTx: U ∈ Tx.
rewrite the current goal using HTx_eq (from right to left).
An exact proof term for the current goal is (generated_topology_contains_basis X Bx HBx_basis U HU).
We prove the intermediate claim HVTy: V ∈ Ty.
rewrite the current goal using HTy_eq (from right to left).
An exact proof term for the current goal is (generated_topology_contains_basis Y By HBy_basis V HV).
We prove the intermediate claim HcSub: c ∈ product_subbasis X Tx Y Ty.
rewrite the current goal using Hceq (from left to right).
We prove the intermediate claim Hrepl: rectangle_set U V ∈ {rectangle_set U W|W ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λW : set ⇒ rectangle_set U W) V HVTy).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 W|W ∈ Ty}) U (rectangle_set U V) HUTx Hrepl).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBprod c HcSub).
We prove the intermediate claim Href: ∀U ∈ product_topology X Tx Y Ty, ∀p ∈ U, ∃Cx ∈ product_basis_from Bx By, p ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ product_topology X Tx Y Ty.
Let p be given.
Assume Hp: p ∈ U.
We prove the intermediate claim HUprop: ∀q ∈ U, ∃b ∈ product_subbasis X Tx Y Ty, q ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀q0 ∈ U0, ∃b0 ∈ product_subbasis X Tx Y Ty, q0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ product_subbasis X Tx Y Ty, p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop p Hp).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
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 ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hpb: p ∈ b.
An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, b ∈ {rectangle_set U0 V0|V0 ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU1 : set ⇒ {rectangle_set U1 V1|V1 ∈ Ty}) b HbSub).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0conj: U0 ∈ Tx ∧ b ∈ {rectangle_set U0 V0|V0 ∈ Ty}.
We prove the intermediate claim HU0: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V0|V0 ∈ Ty}) HU0conj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V0|V0 ∈ Ty}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V0|V0 ∈ Ty}) HU0conj).
We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE Ty (λV1 : set ⇒ rectangle_set U0 V1) b HbRepl).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0conj: V0 ∈ Ty ∧ b = rectangle_set U0 V0.
We prove the intermediate claim HV0: 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).
We prove the intermediate claim Hpb0: p ∈ rectangle_set U0 V0.
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.
We prove the intermediate claim Hp0U0: p 0 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) p Hpb0).
We prove the intermediate claim Hp1V0: p 1 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) p Hpb0).
We prove the intermediate claim HU0gen: U0 ∈ generated_topology X Bx.
rewrite the current goal using HTx_eq (from left to right).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HV0gen: V0 ∈ generated_topology Y By.
rewrite the current goal using HTy_eq (from left to right).
An exact proof term for the current goal is HV0.
We prove the intermediate claim HU0loc: ∀x ∈ U0, ∃bx ∈ Bx, x ∈ bx ∧ bx ⊆ U0.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU1 : set ⇒ ∀x1 ∈ U1, ∃b1 ∈ Bx, x1 ∈ b1 ∧ b1 ⊆ U1) U0 HU0gen).
We prove the intermediate claim HV0loc: ∀y ∈ V0, ∃by ∈ By, y ∈ by ∧ by ⊆ V0.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV1 : set ⇒ ∀y1 ∈ V1, ∃b1 ∈ By, y1 ∈ b1 ∧ b1 ⊆ V1) V0 HV0gen).
We prove the intermediate claim Hexbx: ∃bx ∈ Bx, p 0 ∈ bx ∧ bx ⊆ U0.
An exact proof term for the current goal is (HU0loc (p 0) Hp0U0).
Apply Hexbx to the current goal.
Let bx be given.
Assume Hbxpair.
We prove the intermediate claim Hbx: bx ∈ Bx.
An exact proof term for the current goal is (andEL (bx ∈ Bx) (p 0 ∈ bx ∧ bx ⊆ U0) Hbxpair).
We prove the intermediate claim Hbxprop: p 0 ∈ bx ∧ bx ⊆ U0.
An exact proof term for the current goal is (andER (bx ∈ Bx) (p 0 ∈ bx ∧ bx ⊆ U0) Hbxpair).
We prove the intermediate claim Hp0bx: p 0 ∈ bx.
An exact proof term for the current goal is (andEL (p 0 ∈ bx) (bx ⊆ U0) Hbxprop).
We prove the intermediate claim Hbxsub: bx ⊆ U0.
An exact proof term for the current goal is (andER (p 0 ∈ bx) (bx ⊆ U0) Hbxprop).
We prove the intermediate claim Hexby: ∃by ∈ By, p 1 ∈ by ∧ by ⊆ V0.
An exact proof term for the current goal is (HV0loc (p 1) Hp1V0).
Apply Hexby to the current goal.
Let by be given.
Assume Hbypair.
We prove the intermediate claim Hby: by ∈ By.
An exact proof term for the current goal is (andEL (by ∈ By) (p 1 ∈ by ∧ by ⊆ V0) Hbypair).
We prove the intermediate claim Hbyprop: p 1 ∈ by ∧ by ⊆ V0.
An exact proof term for the current goal is (andER (by ∈ By) (p 1 ∈ by ∧ by ⊆ V0) Hbypair).
We prove the intermediate claim Hp1by: p 1 ∈ by.
An exact proof term for the current goal is (andEL (p 1 ∈ by) (by ⊆ V0) Hbyprop).
We prove the intermediate claim Hbysub: by ⊆ V0.
An exact proof term for the current goal is (andER (p 1 ∈ by) (by ⊆ V0) Hbyprop).
We use (setprod bx by) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hrepl: setprod bx by ∈ {setprod bx w|w ∈ By}.
An exact proof term for the current goal is (ReplI By (λw : set ⇒ setprod bx w) by Hby).
An exact proof term for the current goal is (famunionI Bx (λu : set ⇒ {setprod u w|w ∈ By}) bx (setprod bx by) Hbx Hrepl).
Apply andI to the current goal.
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U0 V0 p Hpb0).
rewrite the current goal using Heta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma bx by (p 0) (p 1) Hp0bx Hp1by).
We prove the intermediate claim Hsubbb: setprod bx by ⊆ setprod U0 V0.
An exact proof term for the current goal is (setprod_Subq bx by U0 V0 Hbxsub Hbysub).
We prove the intermediate claim HsubbU: setprod U0 V0 ⊆ U.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is HbsubU.
An exact proof term for the current goal is (Subq_tra (setprod bx by) (setprod U0 V0) U Hsubbb HsubbU).
Apply (andER (basis_on (setprod X Y) (product_basis_from Bx By)) (generated_topology (setprod X Y) (product_basis_from Bx By) = product_topology X Tx Y Ty) (basis_refines_topology (setprod X Y) (product_topology X Tx Y Ty) (product_basis_from Bx By) HTprod HCsub Href)) to the current goal.
∎