Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
|- F/ x A C_ RR |
2 |
|
nfre1 |
|- F/ x E. x e. ZZ A. y e. A x <_ y |
3 |
|
btwnz |
|- ( x e. RR -> ( E. z e. ZZ z < x /\ E. z e. ZZ x < z ) ) |
4 |
3
|
simpld |
|- ( x e. RR -> E. z e. ZZ z < x ) |
5 |
|
ssel2 |
|- ( ( A C_ RR /\ y e. A ) -> y e. RR ) |
6 |
|
zre |
|- ( z e. ZZ -> z e. RR ) |
7 |
|
ltleletr |
|- ( ( z e. RR /\ x e. RR /\ y e. RR ) -> ( ( z < x /\ x <_ y ) -> z <_ y ) ) |
8 |
6 7
|
syl3an1 |
|- ( ( z e. ZZ /\ x e. RR /\ y e. RR ) -> ( ( z < x /\ x <_ y ) -> z <_ y ) ) |
9 |
8
|
expd |
|- ( ( z e. ZZ /\ x e. RR /\ y e. RR ) -> ( z < x -> ( x <_ y -> z <_ y ) ) ) |
10 |
9
|
3expia |
|- ( ( z e. ZZ /\ x e. RR ) -> ( y e. RR -> ( z < x -> ( x <_ y -> z <_ y ) ) ) ) |
11 |
5 10
|
syl5 |
|- ( ( z e. ZZ /\ x e. RR ) -> ( ( A C_ RR /\ y e. A ) -> ( z < x -> ( x <_ y -> z <_ y ) ) ) ) |
12 |
11
|
expdimp |
|- ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( y e. A -> ( z < x -> ( x <_ y -> z <_ y ) ) ) ) |
13 |
12
|
com23 |
|- ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( z < x -> ( y e. A -> ( x <_ y -> z <_ y ) ) ) ) |
14 |
13
|
imp |
|- ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> ( y e. A -> ( x <_ y -> z <_ y ) ) ) |
15 |
14
|
ralrimiv |
|- ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> A. y e. A ( x <_ y -> z <_ y ) ) |
16 |
|
ralim |
|- ( A. y e. A ( x <_ y -> z <_ y ) -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) |
17 |
15 16
|
syl |
|- ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) |
18 |
17
|
ex |
|- ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) |
19 |
18
|
anasss |
|- ( ( z e. ZZ /\ ( x e. RR /\ A C_ RR ) ) -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) |
20 |
19
|
expcom |
|- ( ( x e. RR /\ A C_ RR ) -> ( z e. ZZ -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) ) |
21 |
20
|
com23 |
|- ( ( x e. RR /\ A C_ RR ) -> ( z < x -> ( z e. ZZ -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) ) |
22 |
21
|
imp |
|- ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( z e. ZZ -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) |
23 |
22
|
imdistand |
|- ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> ( z e. ZZ /\ A. y e. A z <_ y ) ) ) |
24 |
|
breq1 |
|- ( x = z -> ( x <_ y <-> z <_ y ) ) |
25 |
24
|
ralbidv |
|- ( x = z -> ( A. y e. A x <_ y <-> A. y e. A z <_ y ) ) |
26 |
25
|
rspcev |
|- ( ( z e. ZZ /\ A. y e. A z <_ y ) -> E. x e. ZZ A. y e. A x <_ y ) |
27 |
23 26
|
syl6 |
|- ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> E. x e. ZZ A. y e. A x <_ y ) ) |
28 |
27
|
ex |
|- ( ( x e. RR /\ A C_ RR ) -> ( z < x -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
29 |
28
|
com23 |
|- ( ( x e. RR /\ A C_ RR ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
30 |
29
|
ancomsd |
|- ( ( x e. RR /\ A C_ RR ) -> ( ( A. y e. A x <_ y /\ z e. ZZ ) -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
31 |
30
|
expdimp |
|- ( ( ( x e. RR /\ A C_ RR ) /\ A. y e. A x <_ y ) -> ( z e. ZZ -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
32 |
31
|
rexlimdv |
|- ( ( ( x e. RR /\ A C_ RR ) /\ A. y e. A x <_ y ) -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) ) |
33 |
32
|
anasss |
|- ( ( x e. RR /\ ( A C_ RR /\ A. y e. A x <_ y ) ) -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) ) |
34 |
33
|
expcom |
|- ( ( A C_ RR /\ A. y e. A x <_ y ) -> ( x e. RR -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
35 |
4 34
|
mpdi |
|- ( ( A C_ RR /\ A. y e. A x <_ y ) -> ( x e. RR -> E. x e. ZZ A. y e. A x <_ y ) ) |
36 |
35
|
ex |
|- ( A C_ RR -> ( A. y e. A x <_ y -> ( x e. RR -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
37 |
36
|
com23 |
|- ( A C_ RR -> ( x e. RR -> ( A. y e. A x <_ y -> E. x e. ZZ A. y e. A x <_ y ) ) ) |
38 |
1 2 37
|
rexlimd |
|- ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y -> E. x e. ZZ A. y e. A x <_ y ) ) |
39 |
|
zssre |
|- ZZ C_ RR |
40 |
|
ssrexv |
|- ( ZZ C_ RR -> ( E. x e. ZZ A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y ) ) |
41 |
39 40
|
ax-mp |
|- ( E. x e. ZZ A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y ) |
42 |
38 41
|
impbid1 |
|- ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y <-> E. x e. ZZ A. y e. A x <_ y ) ) |