txcls

Description: Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015)

		Ref	Expression
	Assertion	txcls	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R \times_{t} S) (A \times B) = cls (R) (A) \times cls (S) (B)$

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ R \in TopOn (X) \to R \in Top$
2	1	ad2antrr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to R \in Top$
3		simprl	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to A \subseteq X$
4		toponuni	$⊢ R \in TopOn (X) \to X = ⋃ R$
5	4	ad2antrr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to X = ⋃ R$
6	3 5	sseqtrd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to A \subseteq ⋃ R$
7		eqid	$⊢ ⋃ R = ⋃ R$
8	7	clscld	$⊢ (R \in Top \land A \subseteq ⋃ R) \to cls (R) (A) \in Clsd (R)$
9	2 6 8	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R) (A) \in Clsd (R)$
10		topontop	$⊢ S \in TopOn (Y) \to S \in Top$
11	10	ad2antlr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to S \in Top$
12		simprr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to B \subseteq Y$
13		toponuni	$⊢ S \in TopOn (Y) \to Y = ⋃ S$
14	13	ad2antlr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to Y = ⋃ S$
15	12 14	sseqtrd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to B \subseteq ⋃ S$
16		eqid	$⊢ ⋃ S = ⋃ S$
17	16	clscld	$⊢ (S \in Top \land B \subseteq ⋃ S) \to cls (S) (B) \in Clsd (S)$
18	11 15 17	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (S) (B) \in Clsd (S)$
19		txcld	$⊢ (cls (R) (A) \in Clsd (R) \land cls (S) (B) \in Clsd (S)) \to cls (R) (A) \times cls (S) (B) \in Clsd (R \times_{t} S)$
20	9 18 19	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R) (A) \times cls (S) (B) \in Clsd (R \times_{t} S)$
21	7	sscls	$⊢ (R \in Top \land A \subseteq ⋃ R) \to A \subseteq cls (R) (A)$
22	2 6 21	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to A \subseteq cls (R) (A)$
23	16	sscls	$⊢ (S \in Top \land B \subseteq ⋃ S) \to B \subseteq cls (S) (B)$
24	11 15 23	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to B \subseteq cls (S) (B)$
25		xpss12	$⊢ (A \subseteq cls (R) (A) \land B \subseteq cls (S) (B)) \to A \times B \subseteq cls (R) (A) \times cls (S) (B)$
26	22 24 25	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to A \times B \subseteq cls (R) (A) \times cls (S) (B)$
27		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
28	27	clsss2	$⊢ (cls (R) (A) \times cls (S) (B) \in Clsd (R \times_{t} S) \land A \times B \subseteq cls (R) (A) \times cls (S) (B)) \to cls (R \times_{t} S) (A \times B) \subseteq cls (R) (A) \times cls (S) (B)$
29	20 26 28	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R \times_{t} S) (A \times B) \subseteq cls (R) (A) \times cls (S) (B)$
30		relxp	$⊢ Rel (cls (R) (A) \times cls (S) (B))$
31	30	a1i	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to Rel (cls (R) (A) \times cls (S) (B))$
32		opelxp	$⊢ ⟨x, y⟩ \in (cls (R) (A) \times cls (S) (B)) \leftrightarrow (x \in cls (R) (A) \land y \in cls (S) (B))$
33		eltx	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (u \in (R \times_{t} S) \leftrightarrow \forall z \in u \exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u))$
34	33	ad2antrr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to (u \in (R \times_{t} S) \leftrightarrow \forall z \in u \exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u))$
35		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in (r \times s) \leftrightarrow ⟨x, y⟩ \in (r \times s))$
36	35	anbi1d	$⊢ z = ⟨x, y⟩ \to ((z \in (r \times s) \land r \times s \subseteq u) \leftrightarrow (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))$
37	36	2rexbidv	$⊢ z = ⟨x, y⟩ \to (\exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u) \leftrightarrow \exists r \in R \exists s \in S (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))$
38	37	rspccva	$⊢ (\forall z \in u \exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u) \land ⟨x, y⟩ \in u) \to \exists r \in R \exists s \in S (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u)$
39	2	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to R \in Top$
40	6	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to A \subseteq ⋃ R$
41		simplrl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to x \in cls (R) (A)$
42		simprll	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to r \in R$
43		simprrl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to ⟨x, y⟩ \in (r \times s)$
44		opelxp	$⊢ ⟨x, y⟩ \in (r \times s) \leftrightarrow (x \in r \land y \in s)$
45	43 44	sylib	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to (x \in r \land y \in s)$
46	45	simpld	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to x \in r$
47	7	clsndisj	$⊢ ((R \in Top \land A \subseteq ⋃ R \land x \in cls (R) (A)) \land (r \in R \land x \in r)) \to r \cap A \neq \emptyset$
48	39 40 41 42 46 47	syl32anc	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to r \cap A \neq \emptyset$
49		n0	$⊢ r \cap A \neq \emptyset \leftrightarrow \exists z z \in (r \cap A)$
50	48 49	sylib	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to \exists z z \in (r \cap A)$
51	11	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to S \in Top$
52	15	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to B \subseteq ⋃ S$
53		simplrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to y \in cls (S) (B)$
54		simprlr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to s \in S$
55	45	simprd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to y \in s$
56	16	clsndisj	$⊢ ((S \in Top \land B \subseteq ⋃ S \land y \in cls (S) (B)) \land (s \in S \land y \in s)) \to s \cap B \neq \emptyset$
57	51 52 53 54 55 56	syl32anc	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to s \cap B \neq \emptyset$
58		n0	$⊢ s \cap B \neq \emptyset \leftrightarrow \exists w w \in (s \cap B)$
59	57 58	sylib	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to \exists w w \in (s \cap B)$
60		exdistrv	$⊢ \exists z \exists w (z \in (r \cap A) \land w \in (s \cap B)) \leftrightarrow (\exists z z \in (r \cap A) \land \exists w w \in (s \cap B))$
61		opelxpi	$⊢ (z \in (r \cap A) \land w \in (s \cap B)) \to ⟨z, w⟩ \in ((r \cap A) \times (s \cap B))$
62		inxp	$⊢ (r \times s) \cap (A \times B) = (r \cap A) \times (s \cap B)$
63	61 62	eleqtrrdi	$⊢ (z \in (r \cap A) \land w \in (s \cap B)) \to ⟨z, w⟩ \in ((r \times s) \cap (A \times B))$
64	63	elin1d	$⊢ (z \in (r \cap A) \land w \in (s \cap B)) \to ⟨z, w⟩ \in (r \times s)$
65		simprrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to r \times s \subseteq u$
66	65	sselda	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \land ⟨z, w⟩ \in (r \times s)) \to ⟨z, w⟩ \in u$
67	64 66	sylan2	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \land (z \in (r \cap A) \land w \in (s \cap B))) \to ⟨z, w⟩ \in u$
68	63	elin2d	$⊢ (z \in (r \cap A) \land w \in (s \cap B)) \to ⟨z, w⟩ \in (A \times B)$
69	68	adantl	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \land (z \in (r \cap A) \land w \in (s \cap B))) \to ⟨z, w⟩ \in (A \times B)$
70		inelcm	$⊢ (⟨z, w⟩ \in u \land ⟨z, w⟩ \in (A \times B)) \to u \cap (A \times B) \neq \emptyset$
71	67 69 70	syl2anc	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \land (z \in (r \cap A) \land w \in (s \cap B))) \to u \cap (A \times B) \neq \emptyset$
72	71	ex	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to ((z \in (r \cap A) \land w \in (s \cap B)) \to u \cap (A \times B) \neq \emptyset)$
73	72	exlimdvv	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to (\exists z \exists w (z \in (r \cap A) \land w \in (s \cap B)) \to u \cap (A \times B) \neq \emptyset)$
74	60 73	syl5bir	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to ((\exists z z \in (r \cap A) \land \exists w w \in (s \cap B)) \to u \cap (A \times B) \neq \emptyset)$
75	50 59 74	mp2and	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land ((r \in R \land s \in S) \land (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u))) \to u \cap (A \times B) \neq \emptyset$
76	75	expr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \land (r \in R \land s \in S)) \to ((⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u) \to u \cap (A \times B) \neq \emptyset)$
77	76	rexlimdvva	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to (\exists r \in R \exists s \in S (⟨x, y⟩ \in (r \times s) \land r \times s \subseteq u) \to u \cap (A \times B) \neq \emptyset)$
78	38 77	syl5	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to ((\forall z \in u \exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u) \land ⟨x, y⟩ \in u) \to u \cap (A \times B) \neq \emptyset)$
79	78	expd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to (\forall z \in u \exists r \in R \exists s \in S (z \in (r \times s) \land r \times s \subseteq u) \to (⟨x, y⟩ \in u \to u \cap (A \times B) \neq \emptyset))$
80	34 79	sylbid	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to (u \in (R \times_{t} S) \to (⟨x, y⟩ \in u \to u \cap (A \times B) \neq \emptyset))$
81	80	ralrimiv	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to \forall u \in (R \times_{t} S) (⟨x, y⟩ \in u \to u \cap (A \times B) \neq \emptyset)$
82		txtopon	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \times_{t} S \in TopOn (X \times Y)$
83	82	ad2antrr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to R \times_{t} S \in TopOn (X \times Y)$
84		topontop	$⊢ R \times_{t} S \in TopOn (X \times Y) \to R \times_{t} S \in Top$
85	83 84	syl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to R \times_{t} S \in Top$
86		xpss12	$⊢ (A \subseteq X \land B \subseteq Y) \to A \times B \subseteq X \times Y$
87	86	ad2antlr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to A \times B \subseteq X \times Y$
88		toponuni	$⊢ R \times_{t} S \in TopOn (X \times Y) \to X \times Y = ⋃ (R \times_{t} S)$
89	83 88	syl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to X \times Y = ⋃ (R \times_{t} S)$
90	87 89	sseqtrd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to A \times B \subseteq ⋃ (R \times_{t} S)$
91	7	clsss3	$⊢ (R \in Top \land A \subseteq ⋃ R) \to cls (R) (A) \subseteq ⋃ R$
92	2 6 91	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R) (A) \subseteq ⋃ R$
93	92 5	sseqtrrd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R) (A) \subseteq X$
94	93	sselda	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land x \in cls (R) (A)) \to x \in X$
95	94	adantrr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to x \in X$
96	16	clsss3	$⊢ (S \in Top \land B \subseteq ⋃ S) \to cls (S) (B) \subseteq ⋃ S$
97	11 15 96	syl2anc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (S) (B) \subseteq ⋃ S$
98	97 14	sseqtrrd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (S) (B) \subseteq Y$
99	98	sselda	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land y \in cls (S) (B)) \to y \in Y$
100	99	adantrl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to y \in Y$
101	95 100	opelxpd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to ⟨x, y⟩ \in (X \times Y)$
102	101 89	eleqtrd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to ⟨x, y⟩ \in ⋃ (R \times_{t} S)$
103	27	elcls	$⊢ (R \times_{t} S \in Top \land A \times B \subseteq ⋃ (R \times_{t} S) \land ⟨x, y⟩ \in ⋃ (R \times_{t} S)) \to (⟨x, y⟩ \in cls (R \times_{t} S) (A \times B) \leftrightarrow \forall u \in (R \times_{t} S) (⟨x, y⟩ \in u \to u \cap (A \times B) \neq \emptyset))$
104	85 90 102 103	syl3anc	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to (⟨x, y⟩ \in cls (R \times_{t} S) (A \times B) \leftrightarrow \forall u \in (R \times_{t} S) (⟨x, y⟩ \in u \to u \cap (A \times B) \neq \emptyset))$
105	81 104	mpbird	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \land (x \in cls (R) (A) \land y \in cls (S) (B))) \to ⟨x, y⟩ \in cls (R \times_{t} S) (A \times B)$
106	105	ex	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to ((x \in cls (R) (A) \land y \in cls (S) (B)) \to ⟨x, y⟩ \in cls (R \times_{t} S) (A \times B))$
107	32 106	syl5bi	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to (⟨x, y⟩ \in (cls (R) (A) \times cls (S) (B)) \to ⟨x, y⟩ \in cls (R \times_{t} S) (A \times B))$
108	31 107	relssdv	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R) (A) \times cls (S) (B) \subseteq cls (R \times_{t} S) (A \times B)$
109	29 108	eqssd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (A \subseteq X \land B \subseteq Y)) \to cls (R \times_{t} S) (A \times B) = cls (R) (A) \times cls (S) (B)$

Metamath Proof Explorer

Theorem txcls

Proof