Apply andI to the current goal.

Let b be given.

Assume Hb: b ∈ product_subbasis X Tx Y Ty.

We will prove b ∈ 𝒫 (setprod X Y).

We prove the intermediate claim HTxSub: Tx ⊆ 𝒫 X.

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

We prove the intermediate claim HTySub: Ty ⊆ 𝒫 Y.

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

We prove the intermediate claim HexU: ∃U ∈ Tx, b ∈ {rectangle_set U V|V ∈ Ty}.

An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b Hb).

Apply HexU to the current goal.

Let U be given.

Assume HUconj: U ∈ Tx ∧ b ∈ {rectangle_set U V|V ∈ Ty}.

We prove the intermediate claim HU: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ Ty}) HUconj).

We prove the intermediate claim HbRepl: b ∈ {rectangle_set U V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ Ty}) HUconj).

We prove the intermediate claim HexV: ∃V ∈ Ty, b = rectangle_set U V.

An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U V0) b HbRepl).

Apply HexV to the current goal.

Let V be given.

Assume HVconj: V ∈ Ty ∧ b = rectangle_set U V.

We prove the intermediate claim HV: V ∈ Ty.

An exact proof term for the current goal is (andEL (V ∈ Ty) (b = rectangle_set U V) HVconj).

We prove the intermediate claim Hbeq: b = rectangle_set U V.

An exact proof term for the current goal is (andER (V ∈ Ty) (b = rectangle_set U V) HVconj).

We prove the intermediate claim HUpow: U ∈ 𝒫 X.

An exact proof term for the current goal is (HTxSub U HU).

We prove the intermediate claim HVpow: V ∈ 𝒫 Y.

An exact proof term for the current goal is (HTySub V HV).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U HUpow).

We prove the intermediate claim HVsubY: V ⊆ Y.

An exact proof term for the current goal is (PowerE Y V HVpow).

We prove the intermediate claim HrectSub: rectangle_set U V ⊆ setprod X Y.

An exact proof term for the current goal is (setprod_Subq U V X Y HUsubX HVsubY).

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

An exact proof term for the current goal is (PowerI (setprod X Y) (rectangle_set U V) HrectSub).

Let p be given.

Assume Hp: p ∈ setprod X Y.

We use (rectangle_set X Y) to witness the existential quantifier.

Apply andI to the current goal.

We will prove rectangle_set X Y ∈ product_subbasis X Tx Y Ty.

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 HYTy: Y ∈ Ty.

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

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

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

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

An exact proof term for the current goal is Hp.

Let b1 be given.

Assume Hb1: b1 ∈ product_subbasis X Tx Y Ty.

Let b2 be given.

Assume Hb2: b2 ∈ product_subbasis X Tx Y Ty.

Let p be given.

Assume Hp1: p ∈ b1.

Assume Hp2: p ∈ b2.

We prove the intermediate claim HexU1: ∃U1 ∈ Tx, b1 ∈ {rectangle_set U1 V|V ∈ Ty}.

An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b1 Hb1).

Apply HexU1 to the current goal.

Let U1 be given.

Assume HU1conj: U1 ∈ Tx ∧ b1 ∈ {rectangle_set U1 V|V ∈ Ty}.

We prove the intermediate claim HU1: U1 ∈ Tx.

An exact proof term for the current goal is (andEL (U1 ∈ Tx) (b1 ∈ {rectangle_set U1 V|V ∈ Ty}) HU1conj).

We prove the intermediate claim Hb1Repl: b1 ∈ {rectangle_set U1 V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U1 ∈ Tx) (b1 ∈ {rectangle_set U1 V|V ∈ Ty}) HU1conj).

We prove the intermediate claim HexV1: ∃V1 ∈ Ty, b1 = rectangle_set U1 V1.

An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U1 V0) b1 Hb1Repl).

Apply HexV1 to the current goal.

Let V1 be given.

Assume HV1conj: V1 ∈ Ty ∧ b1 = rectangle_set U1 V1.

We prove the intermediate claim HV1: V1 ∈ Ty.

An exact proof term for the current goal is (andEL (V1 ∈ Ty) (b1 = rectangle_set U1 V1) HV1conj).

We prove the intermediate claim Hb1eq: b1 = rectangle_set U1 V1.

An exact proof term for the current goal is (andER (V1 ∈ Ty) (b1 = rectangle_set U1 V1) HV1conj).

We prove the intermediate claim HexU2: ∃U2 ∈ Tx, b2 ∈ {rectangle_set U2 V|V ∈ Ty}.

An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b2 Hb2).

Apply HexU2 to the current goal.

Let U2 be given.

Assume HU2conj: U2 ∈ Tx ∧ b2 ∈ {rectangle_set U2 V|V ∈ Ty}.

We prove the intermediate claim HU2: U2 ∈ Tx.

An exact proof term for the current goal is (andEL (U2 ∈ Tx) (b2 ∈ {rectangle_set U2 V|V ∈ Ty}) HU2conj).

We prove the intermediate claim Hb2Repl: b2 ∈ {rectangle_set U2 V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U2 ∈ Tx) (b2 ∈ {rectangle_set U2 V|V ∈ Ty}) HU2conj).

We prove the intermediate claim HexV2: ∃V2 ∈ Ty, b2 = rectangle_set U2 V2.

An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U2 V0) b2 Hb2Repl).

Apply HexV2 to the current goal.

Let V2 be given.

Assume HV2conj: V2 ∈ Ty ∧ b2 = rectangle_set U2 V2.

We prove the intermediate claim HV2: V2 ∈ Ty.

An exact proof term for the current goal is (andEL (V2 ∈ Ty) (b2 = rectangle_set U2 V2) HV2conj).

We prove the intermediate claim Hb2eq: b2 = rectangle_set U2 V2.

An exact proof term for the current goal is (andER (V2 ∈ Ty) (b2 = rectangle_set U2 V2) HV2conj).

Set b3 to be the term rectangle_set (U1 ∩ U2) (V1 ∩ V2).

We use b3 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HU12: (U1 ∩ U2) ∈ Tx.

An exact proof term for the current goal is (topology_binintersect_closed X Tx U1 U2 HTx HU1 HU2).

We prove the intermediate claim HV12: (V1 ∩ V2) ∈ Ty.

An exact proof term for the current goal is (topology_binintersect_closed Y Ty V1 V2 HTy HV1 HV2).

We prove the intermediate claim Hb3fam: rectangle_set (U1 ∩ U2) (V1 ∩ V2) ∈ {rectangle_set (U1 ∩ U2) V|V ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set (U1 ∩ U2) V0) (V1 ∩ V2) HV12).

An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) (U1 ∩ U2) b3 HU12 Hb3fam).

Apply andI to the current goal.

We prove the intermediate claim HpU1V1: p ∈ rectangle_set U1 V1.

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

An exact proof term for the current goal is Hp1.

We prove the intermediate claim HpU2V2: p ∈ rectangle_set U2 V2.

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

An exact proof term for the current goal is Hp2.

We prove the intermediate claim HpInt: p ∈ (rectangle_set U1 V1) ∩ (rectangle_set U2 V2).

An exact proof term for the current goal is (binintersectI (rectangle_set U1 V1) (rectangle_set U2 V2) p HpU1V1 HpU2V2).

rewrite the current goal using (setprod_intersection U1 V1 U2 V2) (from right to left).

An exact proof term for the current goal is HpInt.

We prove the intermediate claim HintEq: b1 ∩ b2 = b3.

We will prove b1 ∩ b2 = b3.

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

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

An exact proof term for the current goal is (setprod_intersection U1 V1 U2 V2).

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

An exact proof term for the current goal is (Subq_ref b3).