Theorem txcls 21407

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

Assertion

Ref	Expression
txcls	|- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) = ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )

Proof of Theorem txcls

Dummy variables s r u w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		topontop 20718	. . . . . 6 |- ( R e. (TopOn ` X ) -> R e. Top )
2	1	ad2antrr 762	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> R e. Top )
3		simprl 794	. . . . . 6 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ X )
4		toponuni 20719	. . . . . . 7 |- ( R e. (TopOn ` X ) -> X = U. R )
5	4	ad2antrr 762	. . . . . 6 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> X = U. R )
6	3, 5	sseqtrd 3641	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ U. R )
7		eqid 2622	. . . . . 6 |- U. R = U. R
8	7	clscld 20851	. . . . 5 |- ( ( R e. Top /\ A C_ U. R ) -> ( ( cls ` R ) ` A ) e. ( Clsd ` R ) )
9	2, 6, 8	syl2anc 693	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) e. ( Clsd ` R ) )
10		topontop 20718	. . . . . 6 |- ( S e. (TopOn ` Y ) -> S e. Top )
11	10	ad2antlr 763	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> S e. Top )
12		simprr 796	. . . . . 6 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ Y )
13		toponuni 20719	. . . . . . 7 |- ( S e. (TopOn ` Y ) -> Y = U. S )
14	13	ad2antlr 763	. . . . . 6 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> Y = U. S )
15	12, 14	sseqtrd 3641	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ U. S )
16		eqid 2622	. . . . . 6 |- U. S = U. S
17	16	clscld 20851	. . . . 5 |- ( ( S e. Top /\ B C_ U. S ) -> ( ( cls ` S ) ` B ) e. ( Clsd ` S ) )
18	11, 15, 17	syl2anc 693	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) e. ( Clsd ` S ) )
19		txcld 21406	. . . 4 |- ( ( ( ( cls ` R ) ` A ) e. ( Clsd ` R ) /\ ( ( cls ` S ) ` B ) e. ( Clsd ` S ) ) -> ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) e. ( Clsd ` ( R tX S ) ) )
20	9, 18, 19	syl2anc 693	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) e. ( Clsd ` ( R tX S ) ) )
21	7	sscls 20860	. . . . 5 |- ( ( R e. Top /\ A C_ U. R ) -> A C_ ( ( cls ` R ) ` A ) )
22	2, 6, 21	syl2anc 693	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ ( ( cls ` R ) ` A ) )
23	16	sscls 20860	. . . . 5 |- ( ( S e. Top /\ B C_ U. S ) -> B C_ ( ( cls ` S ) ` B ) )
24	11, 15, 23	syl2anc 693	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ ( ( cls ` S ) ` B ) )
25		xpss12 5225	. . . 4 |- ( ( A C_ ( ( cls ` R ) ` A ) /\ B C_ ( ( cls ` S ) ` B ) ) -> ( A X. B ) C_ ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
26	22, 24, 25	syl2anc 693	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( A X. B ) C_ ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
27		eqid 2622	. . . 4 |- U. ( R tX S ) = U. ( R tX S )
28	27	clsss2 20876	. . 3 |- ( ( ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) e. ( Clsd ` ( R tX S ) ) /\ ( A X. B ) C_ ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) ) -> ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) C_ ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
29	20, 26, 28	syl2anc 693	. 2 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) C_ ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
30		relxp 5227	. . . 4 |- Rel ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) )
31	30	a1i 11	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> Rel ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
32		opelxp 5146	. . . 4 |- ( <. x , y >. e. ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) <-> ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) )
33		eltx 21371	. . . . . . . . 9 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( u e. ( R tX S ) <-> A. z e. u E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) ) )
34	33	ad2antrr 762	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( u e. ( R tX S ) <-> A. z e. u E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) ) )
35		eleq1 2689	. . . . . . . . . . . . 13 |- ( z = <. x , y >. -> ( z e. ( r X. s ) <-> <. x , y >. e. ( r X. s ) ) )
36	35	anbi1d 741	. . . . . . . . . . . 12 |- ( z = <. x , y >. -> ( ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) <-> ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) )
37	36	2rexbidv 3057	. . . . . . . . . . 11 |- ( z = <. x , y >. -> ( E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) <-> E. r e. R E. s e. S ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) )
38	37	rspccva 3308	. . . . . . . . . 10 |- ( ( A. z e. u E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) /\ <. x , y >. e. u ) -> E. r e. R E. s e. S ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) )
39	2	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> R e. Top )
40	6	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> A C_ U. R )
41		simplrl 800	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> x e. ( ( cls ` R ) ` A ) )
42		simprll 802	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> r e. R )
43		simprrl 804	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> <. x , y >. e. ( r X. s ) )
44		opelxp 5146	. . . . . . . . . . . . . . . . 17 |- ( <. x , y >. e. ( r X. s ) <-> ( x e. r /\ y e. s ) )
45	43, 44	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( x e. r /\ y e. s ) )
46	45	simpld 475	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> x e. r )
47	7	clsndisj 20879	. . . . . . . . . . . . . . 15 |- ( ( ( R e. Top /\ A C_ U. R /\ x e. ( ( cls ` R ) ` A ) ) /\ ( r e. R /\ x e. r ) ) -> ( r i^i A ) =/= (/) )
48	39, 40, 41, 42, 46, 47	syl32anc 1334	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( r i^i A ) =/= (/) )
49		n0 3931	. . . . . . . . . . . . . 14 |- ( ( r i^i A ) =/= (/) <-> E. z z e. ( r i^i A ) )
50	48, 49	sylib 208	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> E. z z e. ( r i^i A ) )
51	11	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> S e. Top )
52	15	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> B C_ U. S )
53		simplrr 801	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> y e. ( ( cls ` S ) ` B ) )
54		simprlr 803	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> s e. S )
55	45	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> y e. s )
56	16	clsndisj 20879	. . . . . . . . . . . . . . 15 |- ( ( ( S e. Top /\ B C_ U. S /\ y e. ( ( cls ` S ) ` B ) ) /\ ( s e. S /\ y e. s ) ) -> ( s i^i B ) =/= (/) )
57	51, 52, 53, 54, 55, 56	syl32anc 1334	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( s i^i B ) =/= (/) )
58		n0 3931	. . . . . . . . . . . . . 14 |- ( ( s i^i B ) =/= (/) <-> E. w w e. ( s i^i B ) )
59	57, 58	sylib 208	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> E. w w e. ( s i^i B ) )
60		eeanv 2182	. . . . . . . . . . . . . 14 |- ( E. z E. w ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) <-> ( E. z z e. ( r i^i A ) /\ E. w w e. ( s i^i B ) ) )
61		inss1 3833	. . . . . . . . . . . . . . . . . . 19 |- ( ( r X. s ) i^i ( A X. B ) ) C_ ( r X. s )
62		opelxpi 5148	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( ( r i^i A ) X. ( s i^i B ) ) )
63		inxp 5254	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r X. s ) i^i ( A X. B ) ) = ( ( r i^i A ) X. ( s i^i B ) )
64	62, 63	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( ( r X. s ) i^i ( A X. B ) ) )
65	61, 64	sseldi 3601	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( r X. s ) )
66		simprrr 805	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( r X. s ) C_ u )
67	66	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) /\ <. z , w >. e. ( r X. s ) ) -> <. z , w >. e. u )
68	65, 67	sylan2 491	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) /\ ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) ) -> <. z , w >. e. u )
69		inss2 3834	. . . . . . . . . . . . . . . . . . 19 |- ( ( r X. s ) i^i ( A X. B ) ) C_ ( A X. B )
70	69, 64	sseldi 3601	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( A X. B ) )
71	70	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) /\ ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) ) -> <. z , w >. e. ( A X. B ) )
72		inelcm 4032	. . . . . . . . . . . . . . . . 17 |- ( ( <. z , w >. e. u /\ <. z , w >. e. ( A X. B ) ) -> ( u i^i ( A X. B ) ) =/= (/) )
73	68, 71, 72	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) /\ ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) ) -> ( u i^i ( A X. B ) ) =/= (/) )
74	73	ex 450	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
75	74	exlimdvv 1862	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( E. z E. w ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
76	60, 75	syl5bir 233	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( ( E. z z e. ( r i^i A ) /\ E. w w e. ( s i^i B ) ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
77	50, 59, 76	mp2and 715	. . . . . . . . . . . 12 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) ) ) -> ( u i^i ( A X. B ) ) =/= (/) )
78	77	expr 643	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
79	78	rexlimdvva 3038	. . . . . . . . . 10 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( E. r e. R E. s e. S ( <. x , y >. e. ( r X. s ) /\ ( r X. s ) C_ u ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
80	38, 79	syl5 34	. . . . . . . . 9 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( ( A. z e. u E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) /\ <. x , y >. e. u ) -> ( u i^i ( A X. B ) ) =/= (/) ) )
81	80	expd 452	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( A. z e. u E. r e. R E. s e. S ( z e. ( r X. s ) /\ ( r X. s ) C_ u ) -> ( <. x , y >. e. u -> ( u i^i ( A X. B ) ) =/= (/) ) ) )
82	34, 81	sylbid 230	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( u e. ( R tX S ) -> ( <. x , y >. e. u -> ( u i^i ( A X. B ) ) =/= (/) ) ) )
83	82	ralrimiv 2965	. . . . . 6 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> A. u e. ( R tX S ) ( <. x , y >. e. u -> ( u i^i ( A X. B ) ) =/= (/) ) )
84		txtopon 21394	. . . . . . . . 9 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( R tX S ) e. (TopOn ` ( X X. Y ) ) )
85	84	ad2antrr 762	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( R tX S ) e. (TopOn ` ( X X. Y ) ) )
86		topontop 20718	. . . . . . . 8 |- ( ( R tX S ) e. (TopOn ` ( X X. Y ) ) -> ( R tX S ) e. Top )
87	85, 86	syl 17	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( R tX S ) e. Top )
88		xpss12 5225	. . . . . . . . 9 |- ( ( A C_ X /\ B C_ Y ) -> ( A X. B ) C_ ( X X. Y ) )
89	88	ad2antlr 763	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( A X. B ) C_ ( X X. Y ) )
90		toponuni 20719	. . . . . . . . 9 |- ( ( R tX S ) e. (TopOn ` ( X X. Y ) ) -> ( X X. Y ) = U. ( R tX S ) )
91	85, 90	syl 17	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( X X. Y ) = U. ( R tX S ) )
92	89, 91	sseqtrd 3641	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( A X. B ) C_ U. ( R tX S ) )
93	7	clsss3 20863	. . . . . . . . . . . . 13 |- ( ( R e. Top /\ A C_ U. R ) -> ( ( cls ` R ) ` A ) C_ U. R )
94	2, 6, 93	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) C_ U. R )
95	94, 5	sseqtr4d 3642	. . . . . . . . . . 11 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) C_ X )
96	95	sselda 3603	. . . . . . . . . 10 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ x e. ( ( cls ` R ) ` A ) ) -> x e. X )
97	96	adantrr 753	. . . . . . . . 9 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> x e. X )
98	16	clsss3 20863	. . . . . . . . . . . . 13 |- ( ( S e. Top /\ B C_ U. S ) -> ( ( cls ` S ) ` B ) C_ U. S )
99	11, 15, 98	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) C_ U. S )
100	99, 14	sseqtr4d 3642	. . . . . . . . . . 11 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) C_ Y )
101	100	sselda 3603	. . . . . . . . . 10 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ y e. ( ( cls ` S ) ` B ) ) -> y e. Y )
102	101	adantrl 752	. . . . . . . . 9 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> y e. Y )
103		opelxpi 5148	. . . . . . . . 9 |- ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) )
104	97, 102, 103	syl2anc 693	. . . . . . . 8 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> <. x , y >. e. ( X X. Y ) )
105	104, 91	eleqtrd 2703	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> <. x , y >. e. U. ( R tX S ) )
106	27	elcls 20877	. . . . . . 7 |- ( ( ( R tX S ) e. Top /\ ( A X. B ) C_ U. ( R tX S ) /\ <. x , y >. e. U. ( R tX S ) ) -> ( <. x , y >. e. ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) <-> A. u e. ( R tX S ) ( <. x , y >. e. u -> ( u i^i ( A X. B ) ) =/= (/) ) ) )
107	87, 92, 105, 106	syl3anc 1326	. . . . . 6 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> ( <. x , y >. e. ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) <-> A. u e. ( R tX S ) ( <. x , y >. e. u -> ( u i^i ( A X. B ) ) =/= (/) ) ) )
108	83, 107	mpbird 247	. . . . 5 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) ) -> <. x , y >. e. ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) )
109	108	ex 450	. . . 4 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) -> <. x , y >. e. ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) ) )
110	32, 109	syl5bi 232	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( <. x , y >. e. ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) -> <. x , y >. e. ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) ) )
111	31, 110	relssdv 5212	. 2 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) C_ ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) )
112	29, 111	eqssd 3620	1 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) = ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   i^i cin 3573   C_ wss 3574   (/)c0 3915   <.cop 4183   U.cuni 4436   X. cxp 5112   Rel wrel 5119   ` cfv 5888  (class class class)co 6650   Topctop 20698  TopOnctopon 20715   Clsdccld 20820   clsccl 20822   tX ctx 21363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-tx 21365

This theorem is referenced by:  clssubg  21912