Let X, Tx, Y, Ty, Bx and By be given.
Assume HBx: basis_on X Bx ∧ generated_topology X Bx = Tx.
Assume HBy: basis_on Y By ∧ generated_topology Y By = Ty.
We will prove ∃B : set, basis_on (setprod X Y) B ∧ (∀U ∈ Bx, ∀V ∈ By, setprod U V ∈ B) ∧ generated_topology (setprod X Y) B = product_topology X Tx Y Ty.
We use (product_basis_from Bx By) to witness the existential quantifier.
We will prove basis_on (setprod X Y) (product_basis_from Bx By) ∧ (∀U ∈ Bx, ∀V ∈ By, setprod U V ∈ product_basis_from Bx By) ∧ generated_topology (setprod X Y) (product_basis_from Bx By) = product_topology X Tx Y Ty.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HBx_basis: basis_on X Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx) (generated_topology X Bx = Tx) HBx).
We prove the intermediate claim HBy_basis: basis_on Y By.
An exact proof term for the current goal is (andEL (basis_on Y By) (generated_topology Y By = Ty) HBy).
We will prove product_basis_from Bx By ⊆ 𝒫 (setprod X Y) ∧ (∀p ∈ setprod X Y, ∃b ∈ product_basis_from Bx By, p ∈ b) ∧ (∀b1 ∈ product_basis_from Bx By, ∀b2 ∈ product_basis_from Bx By, ∀p : set, p ∈ b1 → p ∈ b2 → ∃b3 ∈ product_basis_from Bx By, p ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply andI to the current goal.
Apply andI to the current goal.
Let b be given.
Assume Hb: b ∈ product_basis_from Bx By.
We will prove b ∈ 𝒫 (setprod X Y).
We prove the intermediate claim Hexists: ∃U ∈ Bx, b ∈ {setprod U V'|V' ∈ By}.
An exact proof term for the current goal is (famunionE Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) b Hb).
Apply Hexists to the current goal.
Let U be given.
Assume HU_conj: U ∈ Bx ∧ b ∈ {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) (b ∈ {setprod U V'|V' ∈ By}) HU_conj).
We prove the intermediate claim HbRepl: b ∈ {setprod U V'|V' ∈ By}.
An exact proof term for the current goal is (andER (U ∈ Bx) (b ∈ {setprod U V'|V' ∈ By}) HU_conj).
We prove the intermediate claim Hexists2: ∃V ∈ By, b = setprod U V.
An exact proof term for the current goal is (ReplE By (λV' ⇒ setprod U V') b HbRepl).
Apply Hexists2 to the current goal.
Let V be given.
Assume HV_conj: V ∈ By ∧ b = setprod U V.
We prove the intermediate claim HV: V ∈ By.
An exact proof term for the current goal is (andEL (V ∈ By) (b = setprod U V) HV_conj).
We prove the intermediate claim Hbeq: b = setprod U V.
An exact proof term for the current goal is (andER (V ∈ By) (b = setprod U V) HV_conj).
We prove the intermediate claim HBx_sub: Bx ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (Bx ⊆ 𝒫 X) (∀x ∈ X, ∃b ∈ Bx, x ∈ b) (andEL (Bx ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ Bx, x ∈ b)) (∀b1 ∈ Bx, ∀b2 ∈ Bx, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ Bx, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBx_basis)).
We prove the intermediate claim HBy_sub: By ⊆ 𝒫 Y.
An exact proof term for the current goal is (andEL (By ⊆ 𝒫 Y) (∀y ∈ Y, ∃b ∈ By, y ∈ b) (andEL (By ⊆ 𝒫 Y ∧ (∀y ∈ Y, ∃b ∈ By, y ∈ b)) (∀b1 ∈ By, ∀b2 ∈ By, ∀y : set, y ∈ b1 → y ∈ b2 → ∃b3 ∈ By, y ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBy_basis)).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U (HBx_sub U HU)).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (PowerE Y V (HBy_sub V HV)).
We prove the intermediate claim HUVsub: setprod U V ⊆ setprod X Y.
An exact proof term for the current goal is (setprod_Subq U V X Y HUsubX HVsubY).
We prove the intermediate claim Hbsub: b ⊆ setprod X Y.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HUVsub.
An exact proof term for the current goal is (PowerI (setprod X Y) b Hbsub).
Let p be given.
Assume Hp: p ∈ setprod X Y.
We will prove ∃b ∈ product_basis_from Bx By, p ∈ b.
We prove the intermediate claim Hcoords: ∃x ∈ X, ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose X Y p Hp).
Apply Hcoords to the current goal.
Let x be given.
Assume Hx_conj: x ∈ X ∧ ∃y ∈ Y, p ∈ setprod {x} {y}.
We prove the intermediate claim Hx: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hx_conj).
We prove the intermediate claim Hy_exists: ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hx_conj).
Apply Hy_exists to the current goal.
Let y be given.
Assume Hy_conj: y ∈ Y ∧ p ∈ setprod {x} {y}.
We prove the intermediate claim Hy: y ∈ Y.
An exact proof term for the current goal is (andEL (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim Hp_sing: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim HBx_cover: ∀x' ∈ X, ∃U ∈ Bx, x' ∈ U.
An exact proof term for the current goal is (andER (Bx ⊆ 𝒫 X) (∀x' ∈ X, ∃U ∈ Bx, x' ∈ U) (andEL (Bx ⊆ 𝒫 X ∧ (∀x' ∈ X, ∃U ∈ Bx, x' ∈ U)) (∀b1 ∈ Bx, ∀b2 ∈ Bx, ∀x' : set, x' ∈ b1 → x' ∈ b2 → ∃b3 ∈ Bx, x' ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBx_basis)).
We prove the intermediate claim HU_exists: ∃U ∈ Bx, x ∈ U.
An exact proof term for the current goal is (HBx_cover x Hx).
Apply HU_exists to the current goal.
Let U be given.
Assume HU_conj: U ∈ Bx ∧ x ∈ U.
We prove the intermediate claim HU: U ∈ Bx.
An exact proof term for the current goal is (andEL (U ∈ Bx) (x ∈ U) HU_conj).
We prove the intermediate claim Hx_in_U: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Bx) (x ∈ U) HU_conj).
We prove the intermediate claim HBy_cover: ∀y' ∈ Y, ∃V ∈ By, y' ∈ V.
An exact proof term for the current goal is (andER (By ⊆ 𝒫 Y) (∀y' ∈ Y, ∃V ∈ By, y' ∈ V) (andEL (By ⊆ 𝒫 Y ∧ (∀y' ∈ Y, ∃V ∈ By, y' ∈ V)) (∀b1 ∈ By, ∀b2 ∈ By, ∀y' : set, y' ∈ b1 → y' ∈ b2 → ∃b3 ∈ By, y' ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBy_basis)).
We prove the intermediate claim HV_exists: ∃V ∈ By, y ∈ V.
An exact proof term for the current goal is (HBy_cover y Hy).
Apply HV_exists to the current goal.
Let V be given.
Assume HV_conj: V ∈ By ∧ y ∈ V.
We prove the intermediate claim HV: V ∈ By.
An exact proof term for the current goal is (andEL (V ∈ By) (y ∈ V) HV_conj).
We prove the intermediate claim Hy_in_V: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ By) (y ∈ V) HV_conj).
We prove the intermediate claim Hx_sing_sub: {x} ⊆ U.
An exact proof term for the current goal is (singleton_subset x U Hx_in_U).
We prove the intermediate claim Hy_sing_sub: {y} ⊆ V.
An exact proof term for the current goal is (singleton_subset y V Hy_in_V).
We prove the intermediate claim HUV_sub: setprod {x} {y} ⊆ setprod U V.
An exact proof term for the current goal is (setprod_Subq {x} {y} U V Hx_sing_sub Hy_sing_sub).
We prove the intermediate claim Hp_in_UV: p ∈ setprod U V.
An exact proof term for the current goal is (HUV_sub p Hp_sing).
We use (setprod U V) to witness the existential quantifier.
We will prove setprod U V ∈ product_basis_from Bx By ∧ p ∈ setprod U V.
Apply andI to the current goal.
We prove the intermediate claim HUVinRepl: setprod U V ∈ {setprod U V'|V' ∈ By}.
An exact proof term for the current goal is (ReplI By (λV' ⇒ setprod U V') V HV).
An exact proof term for the current goal is (famunionI Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) U (setprod U V) HU HUVinRepl).
An exact proof term for the current goal is Hp_in_UV.
Let b1 be given.
Assume Hb1: b1 ∈ product_basis_from Bx By.
Let b2 be given.
Assume Hb2: b2 ∈ product_basis_from Bx By.
Let p be given.
Assume Hpb1: p ∈ b1.
Assume Hpb2: p ∈ b2.
We will prove ∃b3 ∈ product_basis_from Bx By, p ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hexists1: ∃U1 ∈ Bx, b1 ∈ {setprod U1 V'|V' ∈ By}.
An exact proof term for the current goal is (famunionE Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) b1 Hb1).
Apply Hexists1 to the current goal.
Let U1 be given.
Assume HU1_conj: U1 ∈ Bx ∧ b1 ∈ {setprod U1 V'|V' ∈ By}.
We prove the intermediate claim HU1: U1 ∈ Bx.
An exact proof term for the current goal is (andEL (U1 ∈ Bx) (b1 ∈ {setprod U1 V'|V' ∈ By}) HU1_conj).
We prove the intermediate claim Hb1Repl: b1 ∈ {setprod U1 V'|V' ∈ By}.
An exact proof term for the current goal is (andER (U1 ∈ Bx) (b1 ∈ {setprod U1 V'|V' ∈ By}) HU1_conj).
We prove the intermediate claim Hexists1b: ∃V1 ∈ By, b1 = setprod U1 V1.
An exact proof term for the current goal is (ReplE By (λV' ⇒ setprod U1 V') b1 Hb1Repl).
Apply Hexists1b to the current goal.
Let V1 be given.
Assume HV1_conj: V1 ∈ By ∧ b1 = setprod U1 V1.
We prove the intermediate claim HV1: V1 ∈ By.
An exact proof term for the current goal is (andEL (V1 ∈ By) (b1 = setprod U1 V1) HV1_conj).
We prove the intermediate claim Hb1eq: b1 = setprod U1 V1.
An exact proof term for the current goal is (andER (V1 ∈ By) (b1 = setprod U1 V1) HV1_conj).
We prove the intermediate claim Hexists2: ∃U2 ∈ Bx, b2 ∈ {setprod U2 V'|V' ∈ By}.
An exact proof term for the current goal is (famunionE Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) b2 Hb2).
Apply Hexists2 to the current goal.
Let U2 be given.
Assume HU2_conj: U2 ∈ Bx ∧ b2 ∈ {setprod U2 V'|V' ∈ By}.
We prove the intermediate claim HU2: U2 ∈ Bx.
An exact proof term for the current goal is (andEL (U2 ∈ Bx) (b2 ∈ {setprod U2 V'|V' ∈ By}) HU2_conj).
We prove the intermediate claim Hb2Repl: b2 ∈ {setprod U2 V'|V' ∈ By}.
An exact proof term for the current goal is (andER (U2 ∈ Bx) (b2 ∈ {setprod U2 V'|V' ∈ By}) HU2_conj).
We prove the intermediate claim Hexists2b: ∃V2 ∈ By, b2 = setprod U2 V2.
An exact proof term for the current goal is (ReplE By (λV' ⇒ setprod U2 V') b2 Hb2Repl).
Apply Hexists2b to the current goal.
Let V2 be given.
Assume HV2_conj: V2 ∈ By ∧ b2 = setprod U2 V2.
We prove the intermediate claim HV2: V2 ∈ By.
An exact proof term for the current goal is (andEL (V2 ∈ By) (b2 = setprod U2 V2) HV2_conj).
We prove the intermediate claim Hb2eq: b2 = setprod U2 V2.
An exact proof term for the current goal is (andER (V2 ∈ By) (b2 = setprod U2 V2) HV2_conj).
We prove the intermediate claim Hb1sub: b1 ⊆ setprod X Y.
We prove the intermediate claim Hb1Power: b1 ∈ 𝒫 (setprod X Y).
We prove the intermediate claim HBx_sub: Bx ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (Bx ⊆ 𝒫 X) (∀x ∈ X, ∃b ∈ Bx, x ∈ b) (andEL (Bx ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ Bx, x ∈ b)) (∀b1 ∈ Bx, ∀b2 ∈ Bx, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ Bx, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBx_basis)).
We prove the intermediate claim HBy_sub: By ⊆ 𝒫 Y.
An exact proof term for the current goal is (andEL (By ⊆ 𝒫 Y) (∀y ∈ Y, ∃b ∈ By, y ∈ b) (andEL (By ⊆ 𝒫 Y ∧ (∀y ∈ Y, ∃b ∈ By, y ∈ b)) (∀b1 ∈ By, ∀b2 ∈ By, ∀y : set, y ∈ b1 → y ∈ b2 → ∃b3 ∈ By, y ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBy_basis)).
We prove the intermediate claim HU1subX: U1 ⊆ X.
An exact proof term for the current goal is (PowerE X U1 (HBx_sub U1 HU1)).
We prove the intermediate claim HV1subY: V1 ⊆ Y.
An exact proof term for the current goal is (PowerE Y V1 (HBy_sub V1 HV1)).
We prove the intermediate claim HU1V1sub: setprod U1 V1 ⊆ setprod X Y.
An exact proof term for the current goal is (setprod_Subq U1 V1 X Y HU1subX HV1subY).
We prove the intermediate claim Hb1sub_inner: b1 ⊆ setprod X Y.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HU1V1sub.
An exact proof term for the current goal is (PowerI (setprod X Y) b1 Hb1sub_inner).
An exact proof term for the current goal is (PowerE (setprod X Y) b1 Hb1Power).
We prove the intermediate claim Hp_XY: p ∈ setprod X Y.
An exact proof term for the current goal is (Hb1sub p Hpb1).
We prove the intermediate claim Hcoords: ∃x ∈ X, ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose X Y p Hp_XY).
Apply Hcoords to the current goal.
Let x be given.
Assume Hx_conj: x ∈ X ∧ ∃y ∈ Y, p ∈ setprod {x} {y}.
We prove the intermediate claim Hx: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hx_conj).
We prove the intermediate claim Hy_exists: ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (x ∈ X) (∃y ∈ Y, p ∈ setprod {x} {y}) Hx_conj).
Apply Hy_exists to the current goal.
Let y be given.
Assume Hy_conj: y ∈ Y ∧ p ∈ setprod {x} {y}.
We prove the intermediate claim Hy: y ∈ Y.
An exact proof term for the current goal is (andEL (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim Hp_sing: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim Hp_b1: p ∈ setprod U1 V1.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hpb1.
We prove the intermediate claim Hp_b2: p ∈ setprod U2 V2.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hpb2.
We prove the intermediate claim Hxy_U1V1: x ∈ U1 ∧ y ∈ V1.
An exact proof term for the current goal is (setprod_coords_in x y U1 V1 p Hp_sing Hp_b1).
We prove the intermediate claim Hxy_U2V2: x ∈ U2 ∧ y ∈ V2.
An exact proof term for the current goal is (setprod_coords_in x y U2 V2 p Hp_sing Hp_b2).
We prove the intermediate claim Hx_U1: x ∈ U1.
An exact proof term for the current goal is (andEL (x ∈ U1) (y ∈ V1) Hxy_U1V1).
We prove the intermediate claim Hy_V1: y ∈ V1.
An exact proof term for the current goal is (andER (x ∈ U1) (y ∈ V1) Hxy_U1V1).
We prove the intermediate claim Hx_U2: x ∈ U2.
An exact proof term for the current goal is (andEL (x ∈ U2) (y ∈ V2) Hxy_U2V2).
We prove the intermediate claim Hy_V2: y ∈ V2.
An exact proof term for the current goal is (andER (x ∈ U2) (y ∈ V2) Hxy_U2V2).
We prove the intermediate claim HBx_intersect: ∀b1' ∈ Bx, ∀b2' ∈ Bx, ∀x' : set, x' ∈ b1' → x' ∈ b2' → ∃b3' ∈ Bx, x' ∈ b3' ∧ b3' ⊆ b1' ∩ b2'.
An exact proof term for the current goal is (andER (Bx ⊆ 𝒫 X ∧ (∀x' ∈ X, ∃b ∈ Bx, x' ∈ b)) (∀b1' ∈ Bx, ∀b2' ∈ Bx, ∀x' : set, x' ∈ b1' → x' ∈ b2' → ∃b3' ∈ Bx, x' ∈ b3' ∧ b3' ⊆ b1' ∩ b2') HBx_basis).
We prove the intermediate claim HU3_exists: ∃U3 ∈ Bx, x ∈ U3 ∧ U3 ⊆ U1 ∩ U2.
An exact proof term for the current goal is (HBx_intersect U1 HU1 U2 HU2 x Hx_U1 Hx_U2).
Apply HU3_exists to the current goal.
Let U3 be given.
Assume HU3_conj: U3 ∈ Bx ∧ (x ∈ U3 ∧ U3 ⊆ U1 ∩ U2).
We prove the intermediate claim HU3: U3 ∈ Bx.
An exact proof term for the current goal is (andEL (U3 ∈ Bx) (x ∈ U3 ∧ U3 ⊆ U1 ∩ U2) HU3_conj).
We prove the intermediate claim Hx_U3_and_sub: x ∈ U3 ∧ U3 ⊆ U1 ∩ U2.
An exact proof term for the current goal is (andER (U3 ∈ Bx) (x ∈ U3 ∧ U3 ⊆ U1 ∩ U2) HU3_conj).
We prove the intermediate claim Hx_U3: x ∈ U3.
An exact proof term for the current goal is (andEL (x ∈ U3) (U3 ⊆ U1 ∩ U2) Hx_U3_and_sub).
We prove the intermediate claim HU3_sub: U3 ⊆ U1 ∩ U2.
An exact proof term for the current goal is (andER (x ∈ U3) (U3 ⊆ U1 ∩ U2) Hx_U3_and_sub).
We prove the intermediate claim HBy_intersect: ∀b1' ∈ By, ∀b2' ∈ By, ∀y' : set, y' ∈ b1' → y' ∈ b2' → ∃b3' ∈ By, y' ∈ b3' ∧ b3' ⊆ b1' ∩ b2'.
An exact proof term for the current goal is (andER (By ⊆ 𝒫 Y ∧ (∀y' ∈ Y, ∃b ∈ By, y' ∈ b)) (∀b1' ∈ By, ∀b2' ∈ By, ∀y' : set, y' ∈ b1' → y' ∈ b2' → ∃b3' ∈ By, y' ∈ b3' ∧ b3' ⊆ b1' ∩ b2') HBy_basis).
We prove the intermediate claim HV3_exists: ∃V3 ∈ By, y ∈ V3 ∧ V3 ⊆ V1 ∩ V2.
An exact proof term for the current goal is (HBy_intersect V1 HV1 V2 HV2 y Hy_V1 Hy_V2).
Apply HV3_exists to the current goal.
Let V3 be given.
Assume HV3_conj: V3 ∈ By ∧ (y ∈ V3 ∧ V3 ⊆ V1 ∩ V2).
We prove the intermediate claim HV3: V3 ∈ By.
An exact proof term for the current goal is (andEL (V3 ∈ By) (y ∈ V3 ∧ V3 ⊆ V1 ∩ V2) HV3_conj).
We prove the intermediate claim Hy_V3_and_sub: y ∈ V3 ∧ V3 ⊆ V1 ∩ V2.
An exact proof term for the current goal is (andER (V3 ∈ By) (y ∈ V3 ∧ V3 ⊆ V1 ∩ V2) HV3_conj).
We prove the intermediate claim Hy_V3: y ∈ V3.
An exact proof term for the current goal is (andEL (y ∈ V3) (V3 ⊆ V1 ∩ V2) Hy_V3_and_sub).
We prove the intermediate claim HV3_sub: V3 ⊆ V1 ∩ V2.
An exact proof term for the current goal is (andER (y ∈ V3) (V3 ⊆ V1 ∩ V2) Hy_V3_and_sub).
We prove the intermediate claim Hx_sing_sub: {x} ⊆ U3.
An exact proof term for the current goal is (singleton_subset x U3 Hx_U3).
We prove the intermediate claim Hy_sing_sub: {y} ⊆ V3.
An exact proof term for the current goal is (singleton_subset y V3 Hy_V3).
We prove the intermediate claim HU3V3_super: setprod {x} {y} ⊆ setprod U3 V3.
An exact proof term for the current goal is (setprod_Subq {x} {y} U3 V3 Hx_sing_sub Hy_sing_sub).
We prove the intermediate claim Hp_U3V3: p ∈ setprod U3 V3.
An exact proof term for the current goal is (HU3V3_super p Hp_sing).
We prove the intermediate claim Hb1b2_int: b1 ∩ b2 = setprod U1 V1 ∩ setprod U2 V2.
rewrite the current goal using Hb1eq (from left to right).
rewrite the current goal using Hb2eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hprod_int: setprod U1 V1 ∩ setprod U2 V2 = setprod (U1 ∩ U2) (V1 ∩ V2).
An exact proof term for the current goal is (setprod_intersection U1 V1 U2 V2).
We prove the intermediate claim HU3V3_sub: setprod U3 V3 ⊆ setprod (U1 ∩ U2) (V1 ∩ V2).
An exact proof term for the current goal is (setprod_Subq U3 V3 (U1 ∩ U2) (V1 ∩ V2) HU3_sub HV3_sub).
We prove the intermediate claim HU3V3_sub_b1b2: setprod U3 V3 ⊆ b1 ∩ b2.
rewrite the current goal using Hb1b2_int (from left to right).
rewrite the current goal using Hprod_int (from left to right).
An exact proof term for the current goal is HU3V3_sub.
We use (setprod U3 V3) to witness the existential quantifier.
We will prove setprod U3 V3 ∈ product_basis_from Bx By ∧ (p ∈ setprod U3 V3 ∧ setprod U3 V3 ⊆ b1 ∩ b2).
Apply andI to the current goal.
We prove the intermediate claim HU3V3inRepl: setprod U3 V3 ∈ {setprod U3 V'|V' ∈ By}.
An exact proof term for the current goal is (ReplI By (λV' ⇒ setprod U3 V') V3 HV3).
An exact proof term for the current goal is (famunionI Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) U3 (setprod U3 V3) HU3 HU3V3inRepl).
Apply andI to the current goal.
An exact proof term for the current goal is Hp_U3V3.
An exact proof term for the current goal is HU3V3_sub_b1b2.
Let U be given.
Assume HU: U ∈ Bx.
Let V be given.
Assume HV: V ∈ By.
We will prove setprod U V ∈ product_basis_from Bx By.
We prove the intermediate claim HUVinRepl: setprod U V ∈ {setprod U V'|V' ∈ By}.
An exact proof term for the current goal is (ReplI By (λV' ⇒ setprod U V') V HV).
An exact proof term for the current goal is (famunionI Bx (λU' ⇒ {setprod U' V'|V' ∈ By}) U (setprod U V) HU HUVinRepl).
We prove the intermediate claim HBx_basis: basis_on X Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx) (generated_topology X Bx = Tx) HBx).
We prove the intermediate claim HBy_basis: basis_on Y By.
An exact proof term for the current goal is (andEL (basis_on Y By) (generated_topology Y By = Ty) HBy).
We prove the intermediate claim HTx_eq: generated_topology X Bx = Tx.
An exact proof term for the current goal is (andER (basis_on X Bx) (generated_topology X Bx = Tx) HBx).
We prove the intermediate claim HTy_eq: generated_topology Y By = Ty.
An exact proof term for the current goal is (andER (basis_on Y By) (generated_topology Y By = Ty) HBy).
An exact proof term for the current goal is (product_basis_generates_product_topology X Y Bx By Tx Ty HBx_basis HTx_eq HBy_basis HTy_eq).
∎