Metamath Proof Explorer

Theorem txnlly

Description: If the property A is preserved under topological products, then so is the property of being n-locally A . (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis txlly.1 
|- ( ( j e. A /\ k e. A ) -> ( j tX k ) e. A )
Assertion txnlly 
|- ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( R tX S ) e. N-Locally A )

Proof

Step Hyp Ref Expression
1 txlly.1 
 |-  ( ( j e. A /\ k e. A ) -> ( j tX k ) e. A )
2 nllytop 
 |-  ( R e. N-Locally A -> R e. Top )
3 nllytop 
 |-  ( S e. N-Locally A -> S e. Top )
4 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
5 2 3 4 syl2an 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( R tX S ) e. Top )
6 eltx 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( x e. ( R tX S ) <-> A. y e. x E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) )
7 simpll 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> R e. N-Locally A )
8 simprll 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> u e. R )
9 simprrl 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> y e. ( u X. v ) )
10 xp1st 
 |-  ( y e. ( u X. v ) -> ( 1st ` y ) e. u )
11 9 10 syl 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( 1st ` y ) e. u )
12 nlly2i 
 |-  ( ( R e. N-Locally A /\ u e. R /\ ( 1st ` y ) e. u ) -> E. a e. ~P u E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) )
13 7 8 11 12 syl3anc 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. a e. ~P u E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) )
14 simplr 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> S e. N-Locally A )
15 simprlr 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> v e. S )
16 xp2nd 
 |-  ( y e. ( u X. v ) -> ( 2nd ` y ) e. v )
17 9 16 syl 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( 2nd ` y ) e. v )
18 nlly2i 
 |-  ( ( S e. N-Locally A /\ v e. S /\ ( 2nd ` y ) e. v ) -> E. b e. ~P v E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) )
19 14 15 17 18 syl3anc 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. b e. ~P v E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) )
20 reeanv 
 |-  ( E. a e. ~P u E. b e. ~P v ( E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) <-> ( E. a e. ~P u E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. b e. ~P v E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) )
21 reeanv 
 |-  ( E. r e. R E. s e. S ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) <-> ( E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) )
22 5 ad3antrrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( R tX S ) e. Top )
23 2 ad2antrr 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> R e. Top )
24 23 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> R e. Top )
25 14 3 syl 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> S e. Top )
26 25 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> S e. Top )
27 simprrl 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) -> r e. R )
28 27 adantr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> r e. R )
29 simprrr 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) -> s e. S )
30 29 adantr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> s e. S )
31 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( r e. R /\ s e. S ) ) -> ( r X. s ) e. ( R tX S ) )
32 24 26 28 30 31 syl22anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( r X. s ) e. ( R tX S ) )
33 9 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> y e. ( u X. v ) )
34 1st2nd2 
 |-  ( y e. ( u X. v ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
35 33 34 syl 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
36 simprl1 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( 1st ` y ) e. r )
37 simprr1 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( 2nd ` y ) e. s )
38 36 37 opelxpd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( r X. s ) )
39 35 38 eqeltrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> y e. ( r X. s ) )
40 opnneip 
 |-  ( ( ( R tX S ) e. Top /\ ( r X. s ) e. ( R tX S ) /\ y e. ( r X. s ) ) -> ( r X. s ) e. ( ( nei ` ( R tX S ) ) ` { y } ) )
41 22 32 39 40 syl3anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( r X. s ) e. ( ( nei ` ( R tX S ) ) ` { y } ) )
42 simprl2 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> r C_ a )
43 simprr2 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> s C_ b )
44 xpss12 
 |-  ( ( r C_ a /\ s C_ b ) -> ( r X. s ) C_ ( a X. b ) )
45 42 43 44 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( r X. s ) C_ ( a X. b ) )
46 simprll 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) -> a e. ~P u )
47 46 adantr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> a e. ~P u )
48 47 elpwid 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> a C_ u )
49 8 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> u e. R )
50 elssuni 
 |-  ( u e. R -> u C_ U. R )
51 49 50 syl 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> u C_ U. R )
52 48 51 sstrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> a C_ U. R )
53 simprlr 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) -> b e. ~P v )
54 53 adantr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> b e. ~P v )
55 54 elpwid 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> b C_ v )
56 15 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> v e. S )
57 elssuni 
 |-  ( v e. S -> v C_ U. S )
58 56 57 syl 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> v C_ U. S )
59 55 58 sstrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> b C_ U. S )
60 xpss12 
 |-  ( ( a C_ U. R /\ b C_ U. S ) -> ( a X. b ) C_ ( U. R X. U. S ) )
61 52 59 60 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) C_ ( U. R X. U. S ) )
62 eqid 
 |-  U. R = U. R
63 eqid 
 |-  U. S = U. S
64 62 63 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
65 24 26 64 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( U. R X. U. S ) = U. ( R tX S ) )
66 61 65 sseqtrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) C_ U. ( R tX S ) )
67 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
68 67 ssnei2 
 |-  ( ( ( ( R tX S ) e. Top /\ ( r X. s ) e. ( ( nei ` ( R tX S ) ) ` { y } ) ) /\ ( ( r X. s ) C_ ( a X. b ) /\ ( a X. b ) C_ U. ( R tX S ) ) ) -> ( a X. b ) e. ( ( nei ` ( R tX S ) ) ` { y } ) )
69 22 41 45 66 68 syl22anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) e. ( ( nei ` ( R tX S ) ) ` { y } ) )
70 xpss12 
 |-  ( ( a C_ u /\ b C_ v ) -> ( a X. b ) C_ ( u X. v ) )
71 48 55 70 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) C_ ( u X. v ) )
72 simprrr 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( u X. v ) C_ x )
73 72 ad2antrr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( u X. v ) C_ x )
74 71 73 sstrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) C_ x )
75 vex 
 |-  x e. _V
76 75 elpw2 
 |-  ( ( a X. b ) e. ~P x <-> ( a X. b ) C_ x )
77 74 76 sylibr 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) e. ~P x )
78 69 77 elind 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( a X. b ) e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) )
79 txrest 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( a e. ~P u /\ b e. ~P v ) ) -> ( ( R tX S ) |`t ( a X. b ) ) = ( ( R |`t a ) tX ( S |`t b ) ) )
80 24 26 47 54 79 syl22anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( ( R tX S ) |`t ( a X. b ) ) = ( ( R |`t a ) tX ( S |`t b ) ) )
81 simprl3 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( R |`t a ) e. A )
82 simprr3 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( S |`t b ) e. A )
83 1 caovcl 
 |-  ( ( ( R |`t a ) e. A /\ ( S |`t b ) e. A ) -> ( ( R |`t a ) tX ( S |`t b ) ) e. A )
84 81 82 83 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( ( R |`t a ) tX ( S |`t b ) ) e. A )
85 80 84 eqeltrd 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> ( ( R tX S ) |`t ( a X. b ) ) e. A )
86 oveq2 
 |-  ( z = ( a X. b ) -> ( ( R tX S ) |`t z ) = ( ( R tX S ) |`t ( a X. b ) ) )
87 86 eleq1d 
 |-  ( z = ( a X. b ) -> ( ( ( R tX S ) |`t z ) e. A <-> ( ( R tX S ) |`t ( a X. b ) ) e. A ) )
88 87 rspcev 
 |-  ( ( ( a X. b ) e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) /\ ( ( R tX S ) |`t ( a X. b ) ) e. A ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A )
89 78 85 88 syl2anc 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) /\ ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A )
90 89 ex 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( a e. ~P u /\ b e. ~P v ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
91 90 anassrs 
 |-  ( ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( a e. ~P u /\ b e. ~P v ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
92 91 rexlimdvva 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( a e. ~P u /\ b e. ~P v ) ) -> ( E. r e. R E. s e. S ( ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
93 21 92 syl5bir 
 |-  ( ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( a e. ~P u /\ b e. ~P v ) ) -> ( ( E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
94 93 rexlimdvva 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( E. a e. ~P u E. b e. ~P v ( E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
95 20 94 syl5bir 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( ( E. a e. ~P u E. r e. R ( ( 1st ` y ) e. r /\ r C_ a /\ ( R |`t a ) e. A ) /\ E. b e. ~P v E. s e. S ( ( 2nd ` y ) e. s /\ s C_ b /\ ( S |`t b ) e. A ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
96 13 19 95 mp2and 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A )
97 96 expr 
 |-  ( ( ( R e. N-Locally A /\ S e. N-Locally A ) /\ ( u e. R /\ v e. S ) ) -> ( ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
98 97 rexlimdvva 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) -> E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
99 98 ralimdv 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( A. y e. x E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) -> A. y e. x E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
100 6 99 sylbid 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( x e. ( R tX S ) -> A. y e. x E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
101 100 ralrimiv 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> A. x e. ( R tX S ) A. y e. x E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A )
102 isnlly 
 |-  ( ( R tX S ) e. N-Locally A <-> ( ( R tX S ) e. Top /\ A. x e. ( R tX S ) A. y e. x E. z e. ( ( ( nei ` ( R tX S ) ) ` { y } ) i^i ~P x ) ( ( R tX S ) |`t z ) e. A ) )
103 5 101 102 sylanbrc 
 |-  ( ( R e. N-Locally A /\ S e. N-Locally A ) -> ( R tX S ) e. N-Locally A )