Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
|- ( y = A -> ( y < n <-> A < n ) ) |
2 |
1
|
rexbidv |
|- ( y = A -> ( E. n e. NN y < n <-> E. n e. NN A < n ) ) |
3 |
|
nnunb |
|- -. E. y e. RR A. n e. NN ( n < y \/ n = y ) |
4 |
|
ralnex |
|- ( A. y e. RR -. A. n e. NN ( n < y \/ n = y ) <-> -. E. y e. RR A. n e. NN ( n < y \/ n = y ) ) |
5 |
3 4
|
mpbir |
|- A. y e. RR -. A. n e. NN ( n < y \/ n = y ) |
6 |
|
rexnal |
|- ( E. n e. NN -. ( n < y \/ n = y ) <-> -. A. n e. NN ( n < y \/ n = y ) ) |
7 |
|
nnre |
|- ( n e. NN -> n e. RR ) |
8 |
|
axlttri |
|- ( ( y e. RR /\ n e. RR ) -> ( y < n <-> -. ( y = n \/ n < y ) ) ) |
9 |
7 8
|
sylan2 |
|- ( ( y e. RR /\ n e. NN ) -> ( y < n <-> -. ( y = n \/ n < y ) ) ) |
10 |
|
equcom |
|- ( y = n <-> n = y ) |
11 |
10
|
orbi1i |
|- ( ( y = n \/ n < y ) <-> ( n = y \/ n < y ) ) |
12 |
|
orcom |
|- ( ( n = y \/ n < y ) <-> ( n < y \/ n = y ) ) |
13 |
11 12
|
bitri |
|- ( ( y = n \/ n < y ) <-> ( n < y \/ n = y ) ) |
14 |
13
|
notbii |
|- ( -. ( y = n \/ n < y ) <-> -. ( n < y \/ n = y ) ) |
15 |
9 14
|
bitrdi |
|- ( ( y e. RR /\ n e. NN ) -> ( y < n <-> -. ( n < y \/ n = y ) ) ) |
16 |
15
|
biimprd |
|- ( ( y e. RR /\ n e. NN ) -> ( -. ( n < y \/ n = y ) -> y < n ) ) |
17 |
16
|
reximdva |
|- ( y e. RR -> ( E. n e. NN -. ( n < y \/ n = y ) -> E. n e. NN y < n ) ) |
18 |
6 17
|
syl5bir |
|- ( y e. RR -> ( -. A. n e. NN ( n < y \/ n = y ) -> E. n e. NN y < n ) ) |
19 |
18
|
ralimia |
|- ( A. y e. RR -. A. n e. NN ( n < y \/ n = y ) -> A. y e. RR E. n e. NN y < n ) |
20 |
5 19
|
ax-mp |
|- A. y e. RR E. n e. NN y < n |
21 |
2 20
|
vtoclri |
|- ( A e. RR -> E. n e. NN A < n ) |