Step |
Hyp |
Ref |
Expression |
1 |
|
ssel |
|- ( A C_ RR -> ( y e. A -> y e. RR ) ) |
2 |
|
leloe |
|- ( ( y e. RR /\ x e. RR ) -> ( y <_ x <-> ( y < x \/ y = x ) ) ) |
3 |
2
|
expcom |
|- ( x e. RR -> ( y e. RR -> ( y <_ x <-> ( y < x \/ y = x ) ) ) ) |
4 |
1 3
|
syl9 |
|- ( A C_ RR -> ( x e. RR -> ( y e. A -> ( y <_ x <-> ( y < x \/ y = x ) ) ) ) ) |
5 |
4
|
imp31 |
|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y <_ x <-> ( y < x \/ y = x ) ) ) |
6 |
5
|
ralbidva |
|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y <_ x <-> A. y e. A ( y < x \/ y = x ) ) ) |
7 |
6
|
rexbidva |
|- ( A C_ RR -> ( E. x e. RR A. y e. A y <_ x <-> E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) |
8 |
7
|
anbi2d |
|- ( A C_ RR -> ( ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) ) |
9 |
8
|
pm5.32i |
|- ( ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) ) |
10 |
|
3anass |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) ) |
11 |
|
3anass |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) ) |
12 |
9 10 11
|
3bitr4i |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) |
13 |
|
sup2 |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) |
14 |
12 13
|
sylbi |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) |