We will prove continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y).

We will prove topology_on (setprod X Y) (product_topology X Tx Y Ty) ∧ topology_on X Tx ∧ function_on (projection_map1 X Y) (setprod X Y) X ∧ ∀V : set, V ∈ Tx → preimage_of (setprod X Y) (projection_map1 X Y) V ∈ product_topology X Tx Y Ty.

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 (projection_map1 X Y) p ∈ X.

We prove the intermediate claim Happ: apply_fun (projection_map1 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 V be given.

Assume HV: V ∈ Tx.

We will prove preimage_of (setprod X Y) (projection_map1 X Y) V ∈ product_topology X Tx Y Ty.

We prove the intermediate claim HVsub: V ⊆ X.

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

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

An exact proof term for the current goal is (preimage_projection1_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 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 V Y ∈ product_subbasis X Tx Y Ty.

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

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

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

We will prove continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y).

We will prove topology_on (setprod X Y) (product_topology X Tx Y Ty) ∧ topology_on Y Ty ∧ function_on (projection_map2 X Y) (setprod X Y) Y ∧ ∀V : set, V ∈ Ty → preimage_of (setprod X Y) (projection_map2 X Y) V ∈ product_topology X Tx Y Ty.

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 (projection_map2 X Y) p ∈ Y.

We prove the intermediate claim Happ: apply_fun (projection_map2 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 will prove preimage_of (setprod X Y) (projection_map2 X Y) V ∈ product_topology X Tx Y 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) (projection_map2 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).