Apply andI to the current goal.

An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).

An exact proof term for the current goal is HTx.

Let p be given.

Assume Hp: p ∈ setprod X Y.

We will prove apply_fun (projection1 X Y) p ∈ X.

We prove the intermediate claim Happ: apply_fun (projection1 X Y) p = p 0.

An exact proof term for the current goal is (projection1_apply X Y p Hp).

rewrite the current goal using Happ (from left to right).

An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p Hp).

Let U be given.

Assume HU: U ∈ Tx.

We prove the intermediate claim HUsub: U ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).

We prove the intermediate claim HpreEq: preimage_of (setprod X Y) (projection1 X Y) U = rectangle_set U Y.

An exact proof term for the current goal is (preimage_projection1_rectangle X Y U HUsub).

rewrite the current goal using HpreEq (from left to right).

We prove the intermediate claim HBasis: 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 HYTy: Y ∈ Ty.

An exact proof term for the current goal is (topology_has_X Y Ty HTy).

We prove the intermediate claim HRsub: rectangle_set U Y ∈ product_subbasis X Tx Y Ty.

We prove the intermediate claim HRfam: rectangle_set U Y ∈ {rectangle_set U V0|V0 ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set U V0) Y HYTy).

An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) U (rectangle_set U Y) HU HRfam).

An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis (rectangle_set U Y) HRsub).