Metamath Proof Explorer

Theorem txlly

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

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

Proof

Step Hyp Ref Expression
1 txlly.1 
 |-  ( ( j e. A /\ k e. A ) -> ( j tX k ) e. A )
2 llytop 
 |-  ( R e. Locally A -> R e. Top )
3 llytop 
 |-  ( S e. 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. Locally A /\ S e. Locally A ) -> ( R tX S ) e. Top )
6 eltx 
 |-  ( ( R e. Locally A /\ S e. 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. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> R e. Locally A )
8 simprll 
 |-  ( ( ( R e. Locally A /\ S e. 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. Locally A /\ S e. 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. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( 1st ` y ) e. u )
12 llyi 
 |-  ( ( R e. Locally A /\ u e. R /\ ( 1st ` y ) e. u ) -> E. r e. R ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) )
13 7 8 11 12 syl3anc 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. r e. R ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) )
14 simplr 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> S e. Locally A )
15 simprlr 
 |-  ( ( ( R e. Locally A /\ S e. 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. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( 2nd ` y ) e. v )
18 llyi 
 |-  ( ( S e. Locally A /\ v e. S /\ ( 2nd ` y ) e. v ) -> E. s e. S ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) )
19 14 15 17 18 syl3anc 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. s e. S ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) )
20 reeanv 
 |-  ( E. r e. R E. s e. S ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) <-> ( E. r e. R ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ E. s e. S ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) )
21 2 ad3antrrr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> R e. Top )
22 3 ad3antlr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> S e. Top )
23 simprll 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> r e. R )
24 simprlr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> s e. S )
25 txopn 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( r e. R /\ s e. S ) ) -> ( r X. s ) e. ( R tX S ) )
26 21 22 23 24 25 syl22anc 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( r X. s ) e. ( R tX S ) )
27 simprl1 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> r C_ u )
28 simprr1 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> s C_ v )
29 xpss12 
 |-  ( ( r C_ u /\ s C_ v ) -> ( r X. s ) C_ ( u X. v ) )
30 27 28 29 syl2anc 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( r X. s ) C_ ( u X. v ) )
31 simprrr 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( u X. v ) C_ x )
32 30 31 sylan9ssr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( r X. s ) C_ x )
33 vex 
 |-  x e. _V
34 33 elpw2 
 |-  ( ( r X. s ) e. ~P x <-> ( r X. s ) C_ x )
35 32 34 sylibr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( r X. s ) e. ~P x )
36 26 35 elind 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( r X. s ) e. ( ( R tX S ) i^i ~P x ) )
37 1st2nd2 
 |-  ( y e. ( u X. v ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
38 9 37 syl 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
39 38 adantr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
40 simprl2 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( 1st ` y ) e. r )
41 simprr2 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( 2nd ` y ) e. s )
42 40 41 opelxpd 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( r X. s ) )
43 42 adantl 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( r X. s ) )
44 39 43 eqeltrd 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> y e. ( r X. s ) )
45 txrest 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( r e. R /\ s e. S ) ) -> ( ( R tX S ) |`t ( r X. s ) ) = ( ( R |`t r ) tX ( S |`t s ) ) )
46 21 22 23 24 45 syl22anc 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( ( R tX S ) |`t ( r X. s ) ) = ( ( R |`t r ) tX ( S |`t s ) ) )
47 simprl3 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( R |`t r ) e. A )
48 simprr3 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( S |`t s ) e. A )
49 1 caovcl 
 |-  ( ( ( R |`t r ) e. A /\ ( S |`t s ) e. A ) -> ( ( R |`t r ) tX ( S |`t s ) ) e. A )
50 47 48 49 syl2anc 
 |-  ( ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) -> ( ( R |`t r ) tX ( S |`t s ) ) e. A )
51 50 adantl 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( ( R |`t r ) tX ( S |`t s ) ) e. A )
52 46 51 eqeltrd 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> ( ( R tX S ) |`t ( r X. s ) ) e. A )
53 eleq2 
 |-  ( z = ( r X. s ) -> ( y e. z <-> y e. ( r X. s ) ) )
54 oveq2 
 |-  ( z = ( r X. s ) -> ( ( R tX S ) |`t z ) = ( ( R tX S ) |`t ( r X. s ) ) )
55 54 eleq1d 
 |-  ( z = ( r X. s ) -> ( ( ( R tX S ) |`t z ) e. A <-> ( ( R tX S ) |`t ( r X. s ) ) e. A ) )
56 53 55 anbi12d 
 |-  ( z = ( r X. s ) -> ( ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) <-> ( y e. ( r X. s ) /\ ( ( R tX S ) |`t ( r X. s ) ) e. A ) ) )
57 56 rspcev 
 |-  ( ( ( r X. s ) e. ( ( R tX S ) i^i ~P x ) /\ ( y e. ( r X. s ) /\ ( ( R tX S ) |`t ( r X. s ) ) e. A ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) )
58 36 44 52 57 syl12anc 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) )
59 58 expr 
 |-  ( ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
60 59 rexlimdvva 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( E. r e. R E. s e. S ( ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
61 20 60 syl5bir 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> ( ( E. r e. R ( r C_ u /\ ( 1st ` y ) e. r /\ ( R |`t r ) e. A ) /\ E. s e. S ( s C_ v /\ ( 2nd ` y ) e. s /\ ( S |`t s ) e. A ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
62 13 19 61 mp2and 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( ( u e. R /\ v e. S ) /\ ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) ) ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) )
63 62 expr 
 |-  ( ( ( R e. Locally A /\ S e. Locally A ) /\ ( u e. R /\ v e. S ) ) -> ( ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
64 63 rexlimdvva 
 |-  ( ( R e. Locally A /\ S e. Locally A ) -> ( E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ x ) -> E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
65 64 ralimdv 
 |-  ( ( R e. Locally A /\ S e. 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. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
66 6 65 sylbid 
 |-  ( ( R e. Locally A /\ S e. Locally A ) -> ( x e. ( R tX S ) -> A. y e. x E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
67 66 ralrimiv 
 |-  ( ( R e. Locally A /\ S e. Locally A ) -> A. x e. ( R tX S ) A. y e. x E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) )
68 islly 
 |-  ( ( R tX S ) e. Locally A <-> ( ( R tX S ) e. Top /\ A. x e. ( R tX S ) A. y e. x E. z e. ( ( R tX S ) i^i ~P x ) ( y e. z /\ ( ( R tX S ) |`t z ) e. A ) ) )
69 5 67 68 sylanbrc 
 |-  ( ( R e. Locally A /\ S e. Locally A ) -> ( R tX S ) e. Locally A )