Let X, T, T', Y, U and U' be given.
Assume HXne: X ≠ Empty.
Assume HYne: Y ≠ Empty.
Assume HTx: topology_on X T.
Assume HTx': topology_on X T'.
Assume HTy: topology_on Y U.
Assume HTy': topology_on Y U'.
Assume Hprod: product_topology X T Y U ⊆ product_topology X T' Y U'.
We will prove T ⊆ T' ∧ U ⊆ U'.
Apply andI to the current goal.
Let V be given.
Assume HV: V ∈ T.
We will prove V ∈ T'.
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X T V HTx HV).
We prove the intermediate claim HYsubY: Y ⊆ Y.
Let y be given.
Assume Hy: y ∈ Y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim HYU: Y ∈ U.
An exact proof term for the current goal is (topology_has_X Y U HTy).
We prove the intermediate claim HbSub: rectangle_set V Y ∈ product_subbasis X T Y U.
We will prove rectangle_set V Y ∈ product_subbasis X T Y U.
We prove the intermediate claim HbV: rectangle_set V Y ∈ {rectangle_set V W|W ∈ U}.
An exact proof term for the current goal is (ReplI U (λW1 : set ⇒ rectangle_set V W1) Y HYU).
An exact proof term for the current goal is (famunionI T (λU0 : set ⇒ {rectangle_set U0 W|W ∈ U}) V (rectangle_set V Y) HV HbV).
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X T Y U).
An exact proof term for the current goal is (product_subbasis_is_basis X T Y U HTx HTy).
We prove the intermediate claim HbOpen: rectangle_set V Y ∈ product_topology X T Y U.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X T Y U) HBasis (rectangle_set V Y) HbSub).
We prove the intermediate claim HbOpen': rectangle_set V Y ∈ product_topology X T' Y U'.
An exact proof term for the current goal is (Hprod (rectangle_set V Y) HbOpen).
We prove the intermediate claim HprojOpen: open_in X T' (projection_image1 X Y (rectangle_set V Y)).
An exact proof term for the current goal is (andEL (open_in X T' (projection_image1 X Y (rectangle_set V Y))) (open_in Y U' (projection_image2 X Y (rectangle_set V Y))) (ex16_4_projections_open X T' Y U' HTx' HTy' (rectangle_set V Y) HbOpen')).
We prove the intermediate claim HVeqProj: projection_image1 X Y (rectangle_set V Y) = V.
An exact proof term for the current goal is (projection_image1_rectangle_nonempty X Y V Y HVsubX HYsubY HYne).
We prove the intermediate claim HVinT': projection_image1 X Y (rectangle_set V Y) ∈ T'.
An exact proof term for the current goal is (andER (topology_on X T') (projection_image1 X Y (rectangle_set V Y) ∈ T') HprojOpen).
rewrite the current goal using HVeqProj (from right to left).
An exact proof term for the current goal is HVinT'.
Let W be given.
Assume HW: W ∈ U.
We will prove W ∈ U'.
We prove the intermediate claim HWsubY: W ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y U W HTy HW).
We prove the intermediate claim HXsubX: X ⊆ X.
Let x be given.
Assume Hx: x ∈ X.
An exact proof term for the current goal is Hx.
We prove the intermediate claim HX_T: X ∈ T.
An exact proof term for the current goal is (topology_has_X X T HTx).
We prove the intermediate claim HbSub: rectangle_set X W ∈ product_subbasis X T Y U.
We will prove rectangle_set X W ∈ product_subbasis X T Y U.
We prove the intermediate claim HbW: rectangle_set X W ∈ {rectangle_set X V|V ∈ U}.
An exact proof term for the current goal is (ReplI U (λV1 : set ⇒ rectangle_set X V1) W HW).
An exact proof term for the current goal is (famunionI T (λU0 : set ⇒ {rectangle_set U0 V|V ∈ U}) X (rectangle_set X W) HX_T HbW).
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X T Y U).
An exact proof term for the current goal is (product_subbasis_is_basis X T Y U HTx HTy).
We prove the intermediate claim HbOpen: rectangle_set X W ∈ product_topology X T Y U.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X T Y U) HBasis (rectangle_set X W) HbSub).
We prove the intermediate claim HbOpen': rectangle_set X W ∈ product_topology X T' Y U'.
An exact proof term for the current goal is (Hprod (rectangle_set X W) HbOpen).
We prove the intermediate claim HprojOpen: open_in Y U' (projection_image2 X Y (rectangle_set X W)).
An exact proof term for the current goal is (andER (open_in X T' (projection_image1 X Y (rectangle_set X W))) (open_in Y U' (projection_image2 X Y (rectangle_set X W))) (ex16_4_projections_open X T' Y U' HTx' HTy' (rectangle_set X W) HbOpen')).
We prove the intermediate claim HWeqProj: projection_image2 X Y (rectangle_set X W) = W.
An exact proof term for the current goal is (projection_image2_rectangle_nonempty X Y X W HXsubX HWsubY HXne).
We prove the intermediate claim HWinU': projection_image2 X Y (rectangle_set X W) ∈ U'.
An exact proof term for the current goal is (andER (topology_on Y U') (projection_image2 X Y (rectangle_set X W) ∈ U') HprojOpen).
rewrite the current goal using HWeqProj (from right to left).
An exact proof term for the current goal is HWinU'.
∎