Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Let U be given.
Assume HU: U ∈ product_topology X Tx Y Ty.
We will prove open_in X Tx (projection_image1 X Y U) ∧ open_in Y Ty (projection_image2 X Y U).
Apply andI to the current goal.
We will prove open_in X Tx (projection_image1 X Y U).
We will prove topology_on X Tx ∧ projection_image1 X Y U ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We prove the intermediate claim HtopProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HUopen: open_in (setprod X Y) (product_topology X Tx Y Ty) U.
An exact proof term for the current goal is (andI (topology_on (setprod X Y) (product_topology X Tx Y Ty)) (U ∈ product_topology X Tx Y Ty) HtopProd HU).
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 HexFam: ∃Fam ∈ 𝒫 (product_subbasis X Tx Y Ty), ⋃ Fam = U.
An exact proof term for the current goal is (open_sets_as_unions_of_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis U HUopen).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (andEL (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = U) HFampair).
We prove the intermediate claim HUnionEq: ⋃ Fam = U.
An exact proof term for the current goal is (andER (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = U) HFampair).
Set P1Fam to be the term {projection_image1 X Y b|b ∈ Fam}.
We prove the intermediate claim HP1open: open_in X Tx (⋃ P1Fam).
Apply (union_open X Tx P1Fam HTx) to the current goal.
Let W be given.
Assume HW: W ∈ P1Fam.
We will prove open_in X Tx W.
We prove the intermediate claim Hexb: ∃b ∈ Fam, W = projection_image1 X Y b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ projection_image1 X Y b0) W HW).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (W = projection_image1 X Y b) Hbpair).
We prove the intermediate claim HWeq: W = projection_image1 X Y b.
An exact proof term for the current goal is (andER (b ∈ Fam) (W = projection_image1 X Y b) Hbpair).
We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (PowerE (product_subbasis X Tx Y Ty) Fam HFamPow b HbFam).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbSub).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0Tx).
We prove the intermediate claim HV0subY: V0 ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y Ty V0 HTy HV0Ty).
Apply (xm (V0 = Empty)) to the current goal.
Assume HV0E: V0 = Empty.
We prove the intermediate claim HWEmpty: W = Empty.
We will prove W = Empty.
rewrite the current goal using HWeq (from left to right).
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HV0E (from left to right).
An exact proof term for the current goal is (projection_image1_rectangle_empty X Y U0).
rewrite the current goal using HWEmpty (from left to right).
An exact proof term for the current goal is (andI (topology_on X Tx) (Empty ∈ Tx) HTx (topology_has_empty X Tx HTx)).
Assume HV0NE: ¬ (V0 = Empty).
We prove the intermediate claim HV0ne: V0 ≠ Empty.
An exact proof term for the current goal is HV0NE.
We prove the intermediate claim HWU0: W = U0.
We will prove W = U0.
rewrite the current goal using HWeq (from left to right).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (projection_image1_rectangle_nonempty X Y U0 V0 HU0subX HV0subY HV0ne).
rewrite the current goal using HWU0 (from left to right).
An exact proof term for the current goal is (andI (topology_on X Tx) (U0 ∈ Tx) HTx HU0Tx).
We prove the intermediate claim HP1inTx: ⋃ P1Fam ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (⋃ P1Fam ∈ Tx) HP1open).
We prove the intermediate claim HUnionP1: ⋃ P1Fam = projection_image1 X Y (⋃ Fam).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ P1Fam.
We prove the intermediate claim HexW: ∃W : set, x ∈ W ∧ W ∈ P1Fam.
An exact proof term for the current goal is (UnionE P1Fam x Hx).
Apply HexW to the current goal.
Let W be given.
Assume HWconj.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (andEL (x ∈ W) (W ∈ P1Fam) HWconj).
We prove the intermediate claim HWPF: W ∈ P1Fam.
An exact proof term for the current goal is (andER (x ∈ W) (W ∈ P1Fam) HWconj).
We prove the intermediate claim Hexb: ∃b ∈ Fam, W = projection_image1 X Y b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ projection_image1 X Y b0) W HWPF).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (W = projection_image1 X Y b) Hbpair).
We prove the intermediate claim HWeq: W = projection_image1 X Y b.
An exact proof term for the current goal is (andER (b ∈ Fam) (W = projection_image1 X Y b) Hbpair).
We prove the intermediate claim HxP1b: x ∈ projection_image1 X Y b.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is HxW.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ b) x HxP1b).
We prove the intermediate claim Hexy: ∃y : set, (x,y) ∈ b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ b) x HxP1b).
We prove the intermediate claim Hpred: ∃y : set, (x,y) ∈ ⋃ Fam.
Apply Hexy to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ b.
We prove the intermediate claim HbInUnion: (x,y) ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam (x,y) b Hxy HbFam).
We use y to witness the existential quantifier.
An exact proof term for the current goal is HbInUnion.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ ⋃ Fam) x HxX Hpred).
Let x be given.
Assume Hx: x ∈ projection_image1 X Y (⋃ Fam).
We will prove x ∈ ⋃ P1Fam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ ⋃ Fam) x Hx).
We prove the intermediate claim Hexy: ∃y : set, (x,y) ∈ ⋃ Fam.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ ⋃ Fam) x Hx).
Apply Hexy to the current goal.
Let y be given.
Assume HxyUnion: (x,y) ∈ ⋃ Fam.
Apply UnionE_impred Fam (x,y) HxyUnion to the current goal.
Let b be given.
Assume Hxyb HbFam.
We prove the intermediate claim HbPF: projection_image1 X Y b ∈ P1Fam.
An exact proof term for the current goal is (ReplI Fam (λb0 : set ⇒ projection_image1 X Y b0) b HbFam).
We prove the intermediate claim HxP1b: x ∈ projection_image1 X Y b.
We prove the intermediate claim Hpred: ∃y0 : set, (x,y0) ∈ b.
We use y to witness the existential quantifier.
An exact proof term for the current goal is Hxyb.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∃y0 : set, (x0,y0) ∈ b) x HxX Hpred).
An exact proof term for the current goal is (UnionI P1Fam x (projection_image1 X Y b) HxP1b HbPF).
rewrite the current goal using HUnionEq (from right to left).
rewrite the current goal using HUnionP1 (from right to left).
An exact proof term for the current goal is HP1inTx.
We will prove open_in Y Ty (projection_image2 X Y U).
We will prove topology_on Y Ty ∧ projection_image2 X Y U ∈ Ty.
Apply andI to the current goal.
An exact proof term for the current goal is HTy.
We prove the intermediate claim HtopProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HUopen: open_in (setprod X Y) (product_topology X Tx Y Ty) U.
An exact proof term for the current goal is (andI (topology_on (setprod X Y) (product_topology X Tx Y Ty)) (U ∈ product_topology X Tx Y Ty) HtopProd HU).
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 HexFam: ∃Fam ∈ 𝒫 (product_subbasis X Tx Y Ty), ⋃ Fam = U.
An exact proof term for the current goal is (open_sets_as_unions_of_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis U HUopen).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (andEL (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = U) HFampair).
We prove the intermediate claim HUnionEq: ⋃ Fam = U.
An exact proof term for the current goal is (andER (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = U) HFampair).
Set P2Fam to be the term {projection_image2 X Y b|b ∈ Fam}.
We prove the intermediate claim HP2open: open_in Y Ty (⋃ P2Fam).
Apply (union_open Y Ty P2Fam HTy) to the current goal.
Let W be given.
Assume HW: W ∈ P2Fam.
We will prove open_in Y Ty W.
We prove the intermediate claim Hexb: ∃b ∈ Fam, W = projection_image2 X Y b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ projection_image2 X Y b0) W HW).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (W = projection_image2 X Y b) Hbpair).
We prove the intermediate claim HWeq: W = projection_image2 X Y b.
An exact proof term for the current goal is (andER (b ∈ Fam) (W = projection_image2 X Y b) Hbpair).
We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (PowerE (product_subbasis X Tx Y Ty) Fam HFamPow b HbFam).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbSub).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0conj).
We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0Tx).
We prove the intermediate claim HV0subY: V0 ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y Ty V0 HTy HV0Ty).
Apply (xm (U0 = Empty)) to the current goal.
Assume HU0E: U0 = Empty.
We prove the intermediate claim HWEmpty: W = Empty.
We will prove W = Empty.
rewrite the current goal using HWeq (from left to right).
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HU0E (from left to right).
An exact proof term for the current goal is (projection_image2_rectangle_empty X Y V0).
rewrite the current goal using HWEmpty (from left to right).
An exact proof term for the current goal is (andI (topology_on Y Ty) (Empty ∈ Ty) HTy (topology_has_empty Y Ty HTy)).
Assume HU0NE: ¬ (U0 = Empty).
We prove the intermediate claim HUne: U0 ≠ Empty.
An exact proof term for the current goal is HU0NE.
We prove the intermediate claim HWV0: W = V0.
We will prove W = V0.
rewrite the current goal using HWeq (from left to right).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (projection_image2_rectangle_nonempty X Y U0 V0 HU0subX HV0subY HUne).
rewrite the current goal using HWV0 (from left to right).
An exact proof term for the current goal is (andI (topology_on Y Ty) (V0 ∈ Ty) HTy HV0Ty).
We prove the intermediate claim HP2inTy: ⋃ P2Fam ∈ Ty.
An exact proof term for the current goal is (andER (topology_on Y Ty) (⋃ P2Fam ∈ Ty) HP2open).
We prove the intermediate claim HUnionP2: ⋃ P2Fam = projection_image2 X Y (⋃ Fam).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ P2Fam.
We prove the intermediate claim HexW: ∃W : set, y ∈ W ∧ W ∈ P2Fam.
An exact proof term for the current goal is (UnionE P2Fam y Hy).
Apply HexW to the current goal.
Let W be given.
Assume HWconj.
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (andEL (y ∈ W) (W ∈ P2Fam) HWconj).
We prove the intermediate claim HWPF: W ∈ P2Fam.
An exact proof term for the current goal is (andER (y ∈ W) (W ∈ P2Fam) HWconj).
We prove the intermediate claim Hexb: ∃b ∈ Fam, W = projection_image2 X Y b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ projection_image2 X Y b0) W HWPF).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (W = projection_image2 X Y b) Hbpair).
We prove the intermediate claim HWeq: W = projection_image2 X Y b.
An exact proof term for the current goal is (andER (b ∈ Fam) (W = projection_image2 X Y b) Hbpair).
We prove the intermediate claim HyP2b: y ∈ projection_image2 X Y b.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is HyW.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ b) y HyP2b).
We prove the intermediate claim Hexx: ∃x : set, (x,y) ∈ b.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ b) y HyP2b).
We prove the intermediate claim Hpred: ∃x : set, (x,y) ∈ ⋃ Fam.
Apply Hexx to the current goal.
Let x be given.
Assume Hxy: (x,y) ∈ b.
We prove the intermediate claim HbInUnion: (x,y) ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam (x,y) b Hxy HbFam).
We use x to witness the existential quantifier.
An exact proof term for the current goal is HbInUnion.
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ ⋃ Fam) y HyY Hpred).
Let y be given.
Assume Hy: y ∈ projection_image2 X Y (⋃ Fam).
We will prove y ∈ ⋃ P2Fam.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ ⋃ Fam) y Hy).
We prove the intermediate claim Hexx: ∃x : set, (x,y) ∈ ⋃ Fam.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∃x : set, (x,y0) ∈ ⋃ Fam) y Hy).
Apply Hexx to the current goal.
Let x be given.
Assume HxyUnion: (x,y) ∈ ⋃ Fam.
Apply UnionE_impred Fam (x,y) HxyUnion to the current goal.
Let b be given.
Assume Hxyb HbFam.
We prove the intermediate claim HbPF: projection_image2 X Y b ∈ P2Fam.
An exact proof term for the current goal is (ReplI Fam (λb0 : set ⇒ projection_image2 X Y b0) b HbFam).
We prove the intermediate claim HyP2b: y ∈ projection_image2 X Y b.
We prove the intermediate claim Hpred: ∃x0 : set, (x0,y) ∈ b.
We use x to witness the existential quantifier.
An exact proof term for the current goal is Hxyb.
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ ∃x0 : set, (x0,y0) ∈ b) y HyY Hpred).
An exact proof term for the current goal is (UnionI P2Fam y (projection_image2 X Y b) HyP2b HbPF).
rewrite the current goal using HUnionEq (from right to left).
rewrite the current goal using HUnionP2 (from right to left).
An exact proof term for the current goal is HP2inTy.
∎