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 HTy.

Let p be given.

Assume Hp: p ∈ setprod X Y.

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

We prove the intermediate claim Happ: apply_fun (projection2 X Y) p = p 1.

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

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

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

Let V be given.

Assume HV: V ∈ Ty.

We prove the intermediate claim HVsub: V ⊆ Y.

An exact proof term for the current goal is (topology_elem_subset Y Ty V HTy HV).

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

An exact proof term for the current goal is (preimage_projection2_rectangle X Y V HVsub).

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 HXTx: X ∈ Tx.

An exact proof term for the current goal is (topology_has_X X Tx HTx).

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

We prove the intermediate claim HRfam: rectangle_set X V ∈ {rectangle_set X V0|V0 ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set X V0) V HV).

An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) X (rectangle_set X V) HXTx 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 X V) HRsub).