Metamath Proof Explorer

Theorem tx1stc

Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion tx1stc 
|- ( ( R e. 1stc /\ S e. 1stc ) -> ( R tX S ) e. 1stc )

Proof

Step Hyp Ref Expression
1 1stctop 
 |-  ( R e. 1stc -> R e. Top )
2 1stctop 
 |-  ( S e. 1stc -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> ( R tX S ) e. Top )
5 eqid 
 |-  U. R = U. R
6 5 1stcclb 
 |-  ( ( R e. 1stc /\ u e. U. R ) -> E. a e. ~P R ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) )
7 6 ad2ant2r 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> E. a e. ~P R ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) )
8 eqid 
 |-  U. S = U. S
9 8 1stcclb 
 |-  ( ( S e. 1stc /\ v e. U. S ) -> E. b e. ~P S ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) )
10 9 ad2ant2l 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> E. b e. ~P S ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) )
11 reeanv 
 |-  ( E. a e. ~P R E. b e. ~P S ( ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) <-> ( E. a e. ~P R ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ E. b e. ~P S ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) )
12 an4 
 |-  ( ( ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) <-> ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) )
13 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( m e. R /\ n e. S ) ) -> ( m X. n ) e. ( R tX S ) )
14 13 ralrimivva 
 |-  ( ( R e. Top /\ S e. Top ) -> A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) )
15 1 2 14 syl2an 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) )
16 15 adantr 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) )
17 elpwi 
 |-  ( a e. ~P R -> a C_ R )
18 ssralv 
 |-  ( a C_ R -> ( A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) -> A. m e. a A. n e. S ( m X. n ) e. ( R tX S ) ) )
19 17 18 syl 
 |-  ( a e. ~P R -> ( A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) -> A. m e. a A. n e. S ( m X. n ) e. ( R tX S ) ) )
20 elpwi 
 |-  ( b e. ~P S -> b C_ S )
21 ssralv 
 |-  ( b C_ S -> ( A. n e. S ( m X. n ) e. ( R tX S ) -> A. n e. b ( m X. n ) e. ( R tX S ) ) )
22 20 21 syl 
 |-  ( b e. ~P S -> ( A. n e. S ( m X. n ) e. ( R tX S ) -> A. n e. b ( m X. n ) e. ( R tX S ) ) )
23 22 ralimdv 
 |-  ( b e. ~P S -> ( A. m e. a A. n e. S ( m X. n ) e. ( R tX S ) -> A. m e. a A. n e. b ( m X. n ) e. ( R tX S ) ) )
24 19 23 sylan9 
 |-  ( ( a e. ~P R /\ b e. ~P S ) -> ( A. m e. R A. n e. S ( m X. n ) e. ( R tX S ) -> A. m e. a A. n e. b ( m X. n ) e. ( R tX S ) ) )
25 16 24 mpan9 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> A. m e. a A. n e. b ( m X. n ) e. ( R tX S ) )
26 eqid 
 |-  ( m e. a , n e. b |-> ( m X. n ) ) = ( m e. a , n e. b |-> ( m X. n ) )
27 26 fmpo 
 |-  ( A. m e. a A. n e. b ( m X. n ) e. ( R tX S ) <-> ( m e. a , n e. b |-> ( m X. n ) ) : ( a X. b ) --> ( R tX S ) )
28 25 27 sylib 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> ( m e. a , n e. b |-> ( m X. n ) ) : ( a X. b ) --> ( R tX S ) )
29 28 frnd 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) C_ ( R tX S ) )
30 ovex 
 |-  ( R tX S ) e. _V
31 30 elpw2 
 |-  ( ran ( m e. a , n e. b |-> ( m X. n ) ) e. ~P ( R tX S ) <-> ran ( m e. a , n e. b |-> ( m X. n ) ) C_ ( R tX S ) )
32 29 31 sylibr 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) e. ~P ( R tX S ) )
33 32 adantr 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) e. ~P ( R tX S ) )
34 omelon 
 |-  _om e. On
35 xpct 
 |-  ( ( a ~<_ _om /\ b ~<_ _om ) -> ( a X. b ) ~<_ _om )
36 ondomen 
 |-  ( ( _om e. On /\ ( a X. b ) ~<_ _om ) -> ( a X. b ) e. dom card )
37 34 35 36 sylancr 
 |-  ( ( a ~<_ _om /\ b ~<_ _om ) -> ( a X. b ) e. dom card )
38 vex 
 |-  m e. _V
39 vex 
 |-  n e. _V
40 38 39 xpex 
 |-  ( m X. n ) e. _V
41 26 40 fnmpoi 
 |-  ( m e. a , n e. b |-> ( m X. n ) ) Fn ( a X. b )
42 dffn4 
 |-  ( ( m e. a , n e. b |-> ( m X. n ) ) Fn ( a X. b ) <-> ( m e. a , n e. b |-> ( m X. n ) ) : ( a X. b ) -onto-> ran ( m e. a , n e. b |-> ( m X. n ) ) )
43 41 42 mpbi 
 |-  ( m e. a , n e. b |-> ( m X. n ) ) : ( a X. b ) -onto-> ran ( m e. a , n e. b |-> ( m X. n ) )
44 fodomnum 
 |-  ( ( a X. b ) e. dom card -> ( ( m e. a , n e. b |-> ( m X. n ) ) : ( a X. b ) -onto-> ran ( m e. a , n e. b |-> ( m X. n ) ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ ( a X. b ) ) )
45 37 43 44 mpisyl 
 |-  ( ( a ~<_ _om /\ b ~<_ _om ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ ( a X. b ) )
46 domtr 
 |-  ( ( ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ ( a X. b ) /\ ( a X. b ) ~<_ _om ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om )
47 45 35 46 syl2anc 
 |-  ( ( a ~<_ _om /\ b ~<_ _om ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om )
48 47 ad2antrl 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om )
49 1 2 anim12i 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> ( R e. Top /\ S e. Top ) )
50 49 ad3antrrr 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ( R e. Top /\ S e. Top ) )
51 eltx 
 |-  ( ( R e. Top /\ S e. Top ) -> ( z e. ( R tX S ) <-> A. w e. z E. r e. R E. s e. S ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
52 50 51 syl 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ( z e. ( R tX S ) <-> A. w e. z E. r e. R E. s e. S ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
53 eleq1 
 |-  ( w = <. u , v >. -> ( w e. ( r X. s ) <-> <. u , v >. e. ( r X. s ) ) )
54 53 anbi1d 
 |-  ( w = <. u , v >. -> ( ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) <-> ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
55 54 2rexbidv 
 |-  ( w = <. u , v >. -> ( E. r e. R E. s e. S ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) <-> E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
56 55 rspccv 
 |-  ( A. w e. z E. r e. R E. s e. S ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) -> ( <. u , v >. e. z -> E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
57 r19.27v 
 |-  ( ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) -> A. r e. R ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) )
58 r19.29 
 |-  ( ( A. r e. R ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. r e. R ( ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
59 r19.29 
 |-  ( ( A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) /\ E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. s e. S ( ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) /\ ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) )
60 opelxp 
 |-  ( <. u , v >. e. ( r X. s ) <-> ( u e. r /\ v e. s ) )
61 pm3.35 
 |-  ( ( u e. r /\ ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) -> E. p e. a ( u e. p /\ p C_ r ) )
62 pm3.35 
 |-  ( ( v e. s /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) -> E. q e. b ( v e. q /\ q C_ s ) )
63 61 62 anim12i 
 |-  ( ( ( u e. r /\ ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ ( v e. s /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) )
64 63 an4s 
 |-  ( ( ( u e. r /\ v e. s ) /\ ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) )
65 60 64 sylanb 
 |-  ( ( <. u , v >. e. ( r X. s ) /\ ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) )
66 65 anim1i 
 |-  ( ( ( <. u , v >. e. ( r X. s ) /\ ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) /\ ( r X. s ) C_ z ) -> ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
67 66 anasss 
 |-  ( ( <. u , v >. e. ( r X. s ) /\ ( ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ ( r X. s ) C_ z ) ) -> ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
68 67 an12s 
 |-  ( ( ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
69 68 expl 
 |-  ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) -> ( ( ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) /\ ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) )
70 69 reximdv 
 |-  ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) -> ( E. s e. S ( ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) /\ ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) )
71 59 70 syl5 
 |-  ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) -> ( ( A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) /\ E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) )
72 71 impl 
 |-  ( ( ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
73 72 reximi 
 |-  ( E. r e. R ( ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. r e. R E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
74 58 73 syl 
 |-  ( ( A. r e. R ( ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. r e. R E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
75 57 74 sylan 
 |-  ( ( ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. r e. R E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) )
76 reeanv 
 |-  ( E. p e. a E. q e. b ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) <-> ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) )
77 simpr1l 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> p e. a )
78 simpr1r 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> q e. b )
79 eqidd 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( p X. q ) = ( p X. q ) )
80 xpeq1 
 |-  ( m = p -> ( m X. n ) = ( p X. n ) )
81 80 eqeq2d 
 |-  ( m = p -> ( ( p X. q ) = ( m X. n ) <-> ( p X. q ) = ( p X. n ) ) )
82 xpeq2 
 |-  ( n = q -> ( p X. n ) = ( p X. q ) )
83 82 eqeq2d 
 |-  ( n = q -> ( ( p X. q ) = ( p X. n ) <-> ( p X. q ) = ( p X. q ) ) )
84 81 83 rspc2ev 
 |-  ( ( p e. a /\ q e. b /\ ( p X. q ) = ( p X. q ) ) -> E. m e. a E. n e. b ( p X. q ) = ( m X. n ) )
85 77 78 79 84 syl3anc 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> E. m e. a E. n e. b ( p X. q ) = ( m X. n ) )
86 vex 
 |-  p e. _V
87 vex 
 |-  q e. _V
88 86 87 xpex 
 |-  ( p X. q ) e. _V
89 eqeq1 
 |-  ( x = ( p X. q ) -> ( x = ( m X. n ) <-> ( p X. q ) = ( m X. n ) ) )
90 89 2rexbidv 
 |-  ( x = ( p X. q ) -> ( E. m e. a E. n e. b x = ( m X. n ) <-> E. m e. a E. n e. b ( p X. q ) = ( m X. n ) ) )
91 88 90 elab 
 |-  ( ( p X. q ) e. { x | E. m e. a E. n e. b x = ( m X. n ) } <-> E. m e. a E. n e. b ( p X. q ) = ( m X. n ) )
92 85 91 sylibr 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( p X. q ) e. { x | E. m e. a E. n e. b x = ( m X. n ) } )
93 26 rnmpo 
 |-  ran ( m e. a , n e. b |-> ( m X. n ) ) = { x | E. m e. a E. n e. b x = ( m X. n ) }
94 92 93 eleqtrrdi 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( p X. q ) e. ran ( m e. a , n e. b |-> ( m X. n ) ) )
95 simpr2 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) )
96 opelxpi 
 |-  ( ( u e. p /\ v e. q ) -> <. u , v >. e. ( p X. q ) )
97 96 ad2ant2r 
 |-  ( ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) -> <. u , v >. e. ( p X. q ) )
98 95 97 syl 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> <. u , v >. e. ( p X. q ) )
99 xpss12 
 |-  ( ( p C_ r /\ q C_ s ) -> ( p X. q ) C_ ( r X. s ) )
100 99 ad2ant2l 
 |-  ( ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) -> ( p X. q ) C_ ( r X. s ) )
101 95 100 syl 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( p X. q ) C_ ( r X. s ) )
102 simpr3 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( r X. s ) C_ z )
103 101 102 sstrd 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> ( p X. q ) C_ z )
104 eleq2 
 |-  ( w = ( p X. q ) -> ( <. u , v >. e. w <-> <. u , v >. e. ( p X. q ) ) )
105 sseq1 
 |-  ( w = ( p X. q ) -> ( w C_ z <-> ( p X. q ) C_ z ) )
106 104 105 anbi12d 
 |-  ( w = ( p X. q ) -> ( ( <. u , v >. e. w /\ w C_ z ) <-> ( <. u , v >. e. ( p X. q ) /\ ( p X. q ) C_ z ) ) )
107 106 rspcev 
 |-  ( ( ( p X. q ) e. ran ( m e. a , n e. b |-> ( m X. n ) ) /\ ( <. u , v >. e. ( p X. q ) /\ ( p X. q ) C_ z ) ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) )
108 94 98 103 107 syl12anc 
 |-  ( ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) /\ ( ( p e. a /\ q e. b ) /\ ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) )
109 108 3exp2 
 |-  ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( p e. a /\ q e. b ) -> ( ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) -> ( ( r X. s ) C_ z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
110 109 rexlimdvv 
 |-  ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) -> ( E. p e. a E. q e. b ( ( u e. p /\ p C_ r ) /\ ( v e. q /\ q C_ s ) ) -> ( ( r X. s ) C_ z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
111 76 110 syl5bir 
 |-  ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) -> ( ( r X. s ) C_ z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
112 111 impd 
 |-  ( ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
113 112 rexlimdvva 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) -> ( E. r e. R E. s e. S ( ( E. p e. a ( u e. p /\ p C_ r ) /\ E. q e. b ( v e. q /\ q C_ s ) ) /\ ( r X. s ) C_ z ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
114 75 113 syl5 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) -> ( ( ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) /\ E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
115 114 expd 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( a ~<_ _om /\ b ~<_ _om ) ) -> ( ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) -> ( E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
116 115 impr 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ( E. r e. R E. s e. S ( <. u , v >. e. ( r X. s ) /\ ( r X. s ) C_ z ) -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
117 56 116 syl9r 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ( A. w e. z E. r e. R E. s e. S ( w e. ( r X. s ) /\ ( r X. s ) C_ z ) -> ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
118 52 117 sylbid 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> ( z e. ( R tX S ) -> ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
119 118 ralrimiv 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
120 breq1 
 |-  ( y = ran ( m e. a , n e. b |-> ( m X. n ) ) -> ( y ~<_ _om <-> ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om ) )
121 rexeq 
 |-  ( y = ran ( m e. a , n e. b |-> ( m X. n ) ) -> ( E. w e. y ( <. u , v >. e. w /\ w C_ z ) <-> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) )
122 121 imbi2d 
 |-  ( y = ran ( m e. a , n e. b |-> ( m X. n ) ) -> ( ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) <-> ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
123 122 ralbidv 
 |-  ( y = ran ( m e. a , n e. b |-> ( m X. n ) ) -> ( A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) <-> A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) )
124 120 123 anbi12d 
 |-  ( y = ran ( m e. a , n e. b |-> ( m X. n ) ) -> ( ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) <-> ( ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
125 124 rspcev 
 |-  ( ( ran ( m e. a , n e. b |-> ( m X. n ) ) e. ~P ( R tX S ) /\ ( ran ( m e. a , n e. b |-> ( m X. n ) ) ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. ran ( m e. a , n e. b |-> ( m X. n ) ) ( <. u , v >. e. w /\ w C_ z ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
126 33 48 119 125 syl12anc 
 |-  ( ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) /\ ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
127 126 ex 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> ( ( ( a ~<_ _om /\ b ~<_ _om ) /\ ( A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
128 12 127 syl5bi 
 |-  ( ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) /\ ( a e. ~P R /\ b e. ~P S ) ) -> ( ( ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
129 128 rexlimdvva 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> ( E. a e. ~P R E. b e. ~P S ( ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
130 11 129 syl5bir 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> ( ( E. a e. ~P R ( a ~<_ _om /\ A. r e. R ( u e. r -> E. p e. a ( u e. p /\ p C_ r ) ) ) /\ E. b e. ~P S ( b ~<_ _om /\ A. s e. S ( v e. s -> E. q e. b ( v e. q /\ q C_ s ) ) ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
131 7 10 130 mp2and 
 |-  ( ( ( R e. 1stc /\ S e. 1stc ) /\ ( u e. U. R /\ v e. U. S ) ) -> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
132 131 ralrimivva 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> A. u e. U. R A. v e. U. S E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
133 eleq1 
 |-  ( x = <. u , v >. -> ( x e. z <-> <. u , v >. e. z ) )
134 eleq1 
 |-  ( x = <. u , v >. -> ( x e. w <-> <. u , v >. e. w ) )
135 134 anbi1d 
 |-  ( x = <. u , v >. -> ( ( x e. w /\ w C_ z ) <-> ( <. u , v >. e. w /\ w C_ z ) ) )
136 135 rexbidv 
 |-  ( x = <. u , v >. -> ( E. w e. y ( x e. w /\ w C_ z ) <-> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) )
137 133 136 imbi12d 
 |-  ( x = <. u , v >. -> ( ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
138 137 ralbidv 
 |-  ( x = <. u , v >. -> ( A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
139 138 anbi2d 
 |-  ( x = <. u , v >. -> ( ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
140 139 rexbidv 
 |-  ( x = <. u , v >. -> ( E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) ) )
141 140 ralxp 
 |-  ( A. x e. ( U. R X. U. S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> A. u e. U. R A. v e. U. S E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( <. u , v >. e. z -> E. w e. y ( <. u , v >. e. w /\ w C_ z ) ) ) )
142 132 141 sylibr 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> A. x e. ( U. R X. U. S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
143 5 8 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
144 1 2 143 syl2an 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> ( U. R X. U. S ) = U. ( R tX S ) )
145 144 raleqdv 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> ( A. x e. ( U. R X. U. S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> A. x e. U. ( R tX S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
146 142 145 mpbid 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> A. x e. U. ( R tX S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
147 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
148 147 is1stc2 
 |-  ( ( R tX S ) e. 1stc <-> ( ( R tX S ) e. Top /\ A. x e. U. ( R tX S ) E. y e. ~P ( R tX S ) ( y ~<_ _om /\ A. z e. ( R tX S ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
149 4 146 148 sylanbrc 
 |-  ( ( R e. 1stc /\ S e. 1stc ) -> ( R tX S ) e. 1stc )