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 )