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 ) |