Metamath Proof Explorer

Theorem txcls

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

Ref Expression
Assertion 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

Step Hyp Ref Expression
1 topontop 
 |-  ( R e. ( TopOn ` X ) -> R e. Top )
2 1 ad2antrr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> R e. Top )
3 simprl 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ X )
4 toponuni 
 |-  ( R e. ( TopOn ` X ) -> X = U. R )
5 4 ad2antrr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> X = U. R )
6 3 5 sseqtrd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ U. R )
7 eqid 
 |-  U. R = U. R
8 7 clscld 
 |-  ( ( R e. Top /\ A C_ U. R ) -> ( ( cls ` R ) ` A ) e. ( Clsd ` R ) )
9 2 6 8 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) e. ( Clsd ` R ) )
10 topontop 
 |-  ( S e. ( TopOn ` Y ) -> S e. Top )
11 10 ad2antlr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> S e. Top )
12 simprr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ Y )
13 toponuni 
 |-  ( S e. ( TopOn ` Y ) -> Y = U. S )
14 13 ad2antlr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> Y = U. S )
15 12 14 sseqtrd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ U. S )
16 eqid 
 |-  U. S = U. S
17 16 clscld 
 |-  ( ( S e. Top /\ B C_ U. S ) -> ( ( cls ` S ) ` B ) e. ( Clsd ` S ) )
18 11 15 17 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) e. ( Clsd ` S ) )
19 txcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( R e. Top /\ A C_ U. R ) -> A C_ ( ( cls ` R ) ` A ) )
22 2 6 21 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> A C_ ( ( cls ` R ) ` A ) )
23 16 sscls 
 |-  ( ( S e. Top /\ B C_ U. S ) -> B C_ ( ( cls ` S ) ` B ) )
24 11 15 23 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> B C_ ( ( cls ` S ) ` B ) )
25 xpss12 
 |-  ( ( 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 
 |-  ( ( ( 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 
 |-  U. ( R tX S ) = U. ( R tX S )
28 27 clsss2 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  Rel ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) )
31 30 a1i 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> Rel ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
32 opelxp 
 |-  ( <. x , y >. e. ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) <-> ( x e. ( ( cls ` R ) ` A ) /\ y e. ( ( cls ` S ) ` B ) ) )
33 eltx 
 |-  ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( z = <. x , y >. -> ( z e. ( r X. s ) <-> <. x , y >. e. ( r X. s ) ) )
36 35 anbi1d 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( <. x , y >. e. ( r X. s ) <-> ( x e. r /\ y e. s ) )
45 43 44 sylib 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( r i^i A ) =/= (/) <-> E. z z e. ( r i^i A ) )
50 48 49 sylib 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( s i^i B ) =/= (/) <-> E. w w e. ( s i^i B ) )
59 57 58 sylib 
 |-  ( ( ( ( ( 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 exdistrv 
 |-  ( 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 opelxpi 
 |-  ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( ( r i^i A ) X. ( s i^i B ) ) )
62 inxp 
 |-  ( ( r X. s ) i^i ( A X. B ) ) = ( ( r i^i A ) X. ( s i^i B ) )
63 61 62 eleqtrrdi 
 |-  ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( ( r X. s ) i^i ( A X. B ) ) )
64 63 elin1d 
 |-  ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( r X. s ) )
65 simprrr 
 |-  ( ( ( ( ( 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 )
66 65 sselda 
 |-  ( ( ( ( ( ( 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 )
67 64 66 sylan2 
 |-  ( ( ( ( ( ( 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 )
68 63 elin2d 
 |-  ( ( z e. ( r i^i A ) /\ w e. ( s i^i B ) ) -> <. z , w >. e. ( A X. B ) )
69 68 adantl 
 |-  ( ( ( ( ( ( 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 ) )
70 inelcm 
 |-  ( ( <. z , w >. e. u /\ <. z , w >. e. ( A X. B ) ) -> ( u i^i ( A X. B ) ) =/= (/) )
71 67 69 70 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) =/= (/) )
72 71 ex 
 |-  ( ( ( ( ( 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 ) ) =/= (/) ) )
73 72 exlimdvv 
 |-  ( ( ( ( ( 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 ) ) =/= (/) ) )
74 60 73 syl5bir 
 |-  ( ( ( ( ( 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 ) ) =/= (/) ) )
75 50 59 74 mp2and 
 |-  ( ( ( ( ( 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 ) ) =/= (/) )
76 75 expr 
 |-  ( ( ( ( ( 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 ) ) =/= (/) ) )
77 76 rexlimdvva 
 |-  ( ( ( ( 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 ) ) =/= (/) ) )
78 38 77 syl5 
 |-  ( ( ( ( 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 ) ) =/= (/) ) )
79 78 expd 
 |-  ( ( ( ( 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 ) ) =/= (/) ) ) )
80 34 79 sylbid 
 |-  ( ( ( ( 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 ) ) =/= (/) ) ) )
81 80 ralrimiv 
 |-  ( ( ( ( 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 ) ) =/= (/) ) )
82 txtopon 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )
83 82 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
84 topontop 
 |-  ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) -> ( R tX S ) e. Top )
85 83 84 syl 
 |-  ( ( ( ( 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 )
86 xpss12 
 |-  ( ( A C_ X /\ B C_ Y ) -> ( A X. B ) C_ ( X X. Y ) )
87 86 ad2antlr 
 |-  ( ( ( ( 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 ) )
88 toponuni 
 |-  ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) -> ( X X. Y ) = U. ( R tX S ) )
89 83 88 syl 
 |-  ( ( ( ( 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 ) )
90 87 89 sseqtrd 
 |-  ( ( ( ( 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 ) )
91 7 clsss3 
 |-  ( ( R e. Top /\ A C_ U. R ) -> ( ( cls ` R ) ` A ) C_ U. R )
92 2 6 91 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) C_ U. R )
93 92 5 sseqtrrd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` R ) ` A ) C_ X )
94 93 sselda 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ x e. ( ( cls ` R ) ` A ) ) -> x e. X )
95 94 adantrr 
 |-  ( ( ( ( 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 )
96 16 clsss3 
 |-  ( ( S e. Top /\ B C_ U. S ) -> ( ( cls ` S ) ` B ) C_ U. S )
97 11 15 96 syl2anc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) C_ U. S )
98 97 14 sseqtrrd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` S ) ` B ) C_ Y )
99 98 sselda 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) /\ y e. ( ( cls ` S ) ` B ) ) -> y e. Y )
100 99 adantrl 
 |-  ( ( ( ( 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 )
101 95 100 opelxpd 
 |-  ( ( ( ( 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 ) )
102 101 89 eleqtrd 
 |-  ( ( ( ( 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 ) )
103 27 elcls 
 |-  ( ( ( 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 ) ) =/= (/) ) ) )
104 85 90 102 103 syl3anc 
 |-  ( ( ( ( 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 ) ) =/= (/) ) ) )
105 81 104 mpbird 
 |-  ( ( ( ( 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 ) ) )
106 105 ex 
 |-  ( ( ( 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 ) ) ) )
107 32 106 syl5bi 
 |-  ( ( ( 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 ) ) ) )
108 31 107 relssdv 
 |-  ( ( ( 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 ) ) )
109 29 108 eqssd 
 |-  ( ( ( 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 ) ) )