Let X, Tx, Y, Ty, A and B be given.
Assume HA: closed_in X Tx A.
Assume HB: closed_in Y Ty B.
We will prove closed_in (setprod X Y) (product_topology X Tx Y Ty) (setprod A B).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (A ⊆ X ∧ ∃U ∈ Tx, A = X ∖ U) HA).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on Y Ty) (B ⊆ Y ∧ ∃V ∈ Ty, B = Y ∖ V) HB).
We prove the intermediate claim HAparts: A ⊆ X ∧ ∃U ∈ Tx, A = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (A ⊆ X ∧ ∃U ∈ Tx, A = X ∖ U) HA).
We prove the intermediate claim HBparts: B ⊆ Y ∧ ∃V ∈ Ty, B = Y ∖ V.
An exact proof term for the current goal is (andER (topology_on Y Ty) (B ⊆ Y ∧ ∃V ∈ Ty, B = Y ∖ V) HB).
We prove the intermediate claim HAsub: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) HAparts).
We prove the intermediate claim HBsub: B ⊆ Y.
An exact proof term for the current goal is (andEL (B ⊆ Y) (∃V ∈ Ty, B = Y ∖ V) HBparts).
We prove the intermediate claim HexU: ∃U ∈ Tx, A = X ∖ U.
An exact proof term for the current goal is (andER (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) HAparts).
We prove the intermediate claim HexV: ∃V ∈ Ty, B = Y ∖ V.
An exact proof term for the current goal is (andER (B ⊆ Y) (∃V ∈ Ty, B = Y ∖ V) HBparts).
We prove the intermediate claim HTProd: 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 will prove topology_on (setprod X Y) (product_topology X Tx Y Ty) ∧ (setprod A B ⊆ setprod X Y ∧ ∃W ∈ product_topology X Tx Y Ty, setprod A B = (setprod X Y) ∖ W).
Apply andI to the current goal.
An exact proof term for the current goal is HTProd.
Apply andI to the current goal.
An exact proof term for the current goal is (setprod_Subq A B X Y HAsub HBsub).
Apply HexU to the current goal.
Let U be given.
Assume HU_conj.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (A = X ∖ U) HU_conj).
We prove the intermediate claim HAeq: A = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (A = X ∖ U) HU_conj).
Apply HexV to the current goal.
Let V be given.
Assume HV_conj.
We prove the intermediate claim HVinTy: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (B = Y ∖ V) HV_conj).
We prove the intermediate claim HBeq: B = Y ∖ V.
An exact proof term for the current goal is (andER (V ∈ Ty) (B = Y ∖ V) HV_conj).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y Ty V HTy HVinTy).
We prove the intermediate claim HXminusA: X ∖ A = U.
rewrite the current goal using HAeq (from left to right) at position 1.
An exact proof term for the current goal is (setminus_setminus_eq X U HUsubX).
We prove the intermediate claim HYminusB: Y ∖ B = V.
rewrite the current goal using HBeq (from left to right) at position 1.
An exact proof term for the current goal is (setminus_setminus_eq Y V HVsubY).
Set W1 to be the term setprod (X ∖ A) Y.
Set W2 to be the term setprod X (Y ∖ B).
Set W to be the term W1 ∪ W2.
We use W to witness the existential quantifier.
Apply andI to the current goal.
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 HW1sub: W1 ∈ product_subbasis X Tx Y Ty.
We will prove W1 ∈ product_subbasis X Tx Y Ty.
rewrite the current goal using HXminusA (from left to right).
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 HW1fam: 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) HUinTx HW1fam).
We prove the intermediate claim HW2sub: W2 ∈ product_subbasis X Tx Y Ty.
We will prove W2 ∈ product_subbasis X Tx Y Ty.
rewrite the current goal using HYminusB (from left to right).
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 HW2fam: 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 HVinTy).
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 HW2fam).
We prove the intermediate claim HW1open: W1 ∈ product_topology X Tx Y Ty.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis W1 HW1sub).
We prove the intermediate claim HW2open: W2 ∈ product_topology X Tx Y Ty.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis W2 HW2sub).
An exact proof term for the current goal is (lemma_union_two_open (setprod X Y) (product_topology X Tx Y Ty) W1 W2 HTProd HW1open HW2open).
We will prove setprod A B = setprod X Y ∖ W.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ setprod A B.
We will prove p ∈ setprod X Y ∖ W.
We prove the intermediate claim HpXY: p ∈ setprod X Y.
An exact proof term for the current goal is ((setprod_Subq A B X Y HAsub HBsub) p Hp).
We prove the intermediate claim Hexab: ∃x ∈ A, ∃y ∈ B, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose A B p Hp).
We prove the intermediate claim HpNotW: p ∉ W.
Apply Hexab to the current goal.
Let x be given.
Assume Hx_conj.
We prove the intermediate claim HxA': x ∈ A.
An exact proof term for the current goal is (andEL (x ∈ A) (∃y0 ∈ B, p ∈ setprod {x} {y0}) Hx_conj).
We prove the intermediate claim Hexy: ∃y0 ∈ B, p ∈ setprod {x} {y0}.
An exact proof term for the current goal is (andER (x ∈ A) (∃y0 ∈ B, p ∈ setprod {x} {y0}) Hx_conj).
Apply Hexy to the current goal.
Let y be given.
Assume Hy_conj.
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (andEL (y ∈ B) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim Hpsing: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ B) (p ∈ setprod {x} {y}) Hy_conj).
Assume HpW: p ∈ W.
Apply (binunionE W1 W2 p HpW) to the current goal.
Assume HpW1: p ∈ W1.
We prove the intermediate claim Hxy: x ∈ (X ∖ A) ∧ y ∈ Y.
An exact proof term for the current goal is (setprod_coords_in x y (X ∖ A) Y p Hpsing HpW1).
We prove the intermediate claim HxXA: x ∈ X ∖ A.
An exact proof term for the current goal is (andEL (x ∈ X ∖ A) (y ∈ Y) Hxy).
An exact proof term for the current goal is ((setminusE2 X A x HxXA) HxA').
Assume HpW2: p ∈ W2.
We prove the intermediate claim Hxy: x ∈ X ∧ y ∈ (Y ∖ B).
An exact proof term for the current goal is (setprod_coords_in x y X (Y ∖ B) p Hpsing HpW2).
We prove the intermediate claim HyYB: y ∈ Y ∖ B.
An exact proof term for the current goal is (andER (x ∈ X) (y ∈ Y ∖ B) Hxy).
An exact proof term for the current goal is ((setminusE2 Y B y HyYB) HyB).
An exact proof term for the current goal is (setminusI (setprod X Y) W p HpXY HpNotW).
Let p be given.
Assume Hp: p ∈ setprod X Y ∖ W.
We will prove p ∈ setprod A B.
We prove the intermediate claim HpXY: p ∈ setprod X Y.
An exact proof term for the current goal is (setminusE1 (setprod X Y) W p Hp).
We prove the intermediate claim HpNotW: p ∉ W.
An exact proof term for the current goal is (setminusE2 (setprod X Y) W p Hp).
We prove the intermediate claim Hexxy: ∃x ∈ X, ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose X Y p HpXY).
Apply Hexxy to the current goal.
Let x be given.
Assume Hx_conj.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (∃y0 ∈ Y, p ∈ setprod {x} {y0}) Hx_conj).
We prove the intermediate claim Hexy: ∃y0 ∈ Y, p ∈ setprod {x} {y0}.
An exact proof term for the current goal is (andER (x ∈ X) (∃y0 ∈ Y, p ∈ setprod {x} {y0}) Hx_conj).
Apply Hexy to the current goal.
Let y be given.
Assume Hy_conj.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (andEL (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim Hpsing: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {x} {y}) Hy_conj).
We prove the intermediate claim HxA: x ∈ A.
Apply (xm (x ∈ A)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HxNotA: ¬ (x ∈ A).
We prove the intermediate claim HxXA: x ∈ X ∖ A.
An exact proof term for the current goal is (setminusI X A x HxX HxNotA).
We prove the intermediate claim HxSingSub: {x} ⊆ X ∖ A.
An exact proof term for the current goal is (singleton_subset x (X ∖ A) HxXA).
We prove the intermediate claim HySingSub: {y} ⊆ Y.
An exact proof term for the current goal is (singleton_subset y Y HyY).
We prove the intermediate claim HpW1: p ∈ W1.
We prove the intermediate claim Hsub: setprod {x} {y} ⊆ W1.
An exact proof term for the current goal is (setprod_Subq {x} {y} (X ∖ A) Y HxSingSub HySingSub).
An exact proof term for the current goal is (Hsub p Hpsing).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HpNotW (binunionI1 W1 W2 p HpW1)).
We prove the intermediate claim HyB: y ∈ B.
Apply (xm (y ∈ B)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HyNotB: ¬ (y ∈ B).
We prove the intermediate claim HyYB: y ∈ Y ∖ B.
An exact proof term for the current goal is (setminusI Y B y HyY HyNotB).
We prove the intermediate claim HySingSub: {y} ⊆ Y ∖ B.
An exact proof term for the current goal is (singleton_subset y (Y ∖ B) HyYB).
We prove the intermediate claim HxSingSub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
We prove the intermediate claim HpW2: p ∈ W2.
We prove the intermediate claim Hsub: setprod {x} {y} ⊆ W2.
An exact proof term for the current goal is (setprod_Subq {x} {y} X (Y ∖ B) HxSingSub HySingSub).
An exact proof term for the current goal is (Hsub p Hpsing).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HpNotW (binunionI2 W1 W2 p HpW2)).
We prove the intermediate claim HxSingSubA: {x} ⊆ A.
An exact proof term for the current goal is (singleton_subset x A HxA).
We prove the intermediate claim HySingSubB: {y} ⊆ B.
An exact proof term for the current goal is (singleton_subset y B HyB).
We prove the intermediate claim HpAB: p ∈ setprod A B.
We prove the intermediate claim Hsub: setprod {x} {y} ⊆ setprod A B.
An exact proof term for the current goal is (setprod_Subq {x} {y} A B HxSingSubA HySingSubB).
An exact proof term for the current goal is (Hsub p Hpsing).
An exact proof term for the current goal is HpAB.
∎