Step |
Hyp |
Ref |
Expression |
1 |
|
df-inf |
|- inf ( A , RR , < ) = sup ( A , RR , `' < ) |
2 |
|
df-sup |
|- sup ( A , RR , `' < ) = U. { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) } |
3 |
|
ssel2 |
|- ( ( A C_ RR /\ y e. A ) -> y e. RR ) |
4 |
|
vex |
|- x e. _V |
5 |
|
vex |
|- y e. _V |
6 |
4 5
|
brcnv |
|- ( x `' < y <-> y < x ) |
7 |
6
|
notbii |
|- ( -. x `' < y <-> -. y < x ) |
8 |
|
lenlt |
|- ( ( x e. RR /\ y e. RR ) -> ( x <_ y <-> -. y < x ) ) |
9 |
7 8
|
bitr4id |
|- ( ( x e. RR /\ y e. RR ) -> ( -. x `' < y <-> x <_ y ) ) |
10 |
3 9
|
sylan2 |
|- ( ( x e. RR /\ ( A C_ RR /\ y e. A ) ) -> ( -. x `' < y <-> x <_ y ) ) |
11 |
10
|
ancoms |
|- ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( -. x `' < y <-> x <_ y ) ) |
12 |
11
|
an32s |
|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( -. x `' < y <-> x <_ y ) ) |
13 |
12
|
ralbidva |
|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A -. x `' < y <-> A. y e. A x <_ y ) ) |
14 |
5 4
|
brcnv |
|- ( y `' < x <-> x < y ) |
15 |
|
vex |
|- z e. _V |
16 |
5 15
|
brcnv |
|- ( y `' < z <-> z < y ) |
17 |
16
|
rexbii |
|- ( E. z e. A y `' < z <-> E. z e. A z < y ) |
18 |
14 17
|
imbi12i |
|- ( ( y `' < x -> E. z e. A y `' < z ) <-> ( x < y -> E. z e. A z < y ) ) |
19 |
18
|
ralbii |
|- ( A. y e. RR ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR ( x < y -> E. z e. A z < y ) ) |
20 |
19
|
a1i |
|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. RR ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR ( x < y -> E. z e. A z < y ) ) ) |
21 |
13 20
|
anbi12d |
|- ( ( A C_ RR /\ x e. RR ) -> ( ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) ) ) |
22 |
21
|
rabbidva |
|- ( A C_ RR -> { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) } = { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } ) |
23 |
22
|
unieqd |
|- ( A C_ RR -> U. { x e. RR | ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) } = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } ) |
24 |
2 23
|
eqtrid |
|- ( A C_ RR -> sup ( A , RR , `' < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } ) |
25 |
1 24
|
eqtrid |
|- ( A C_ RR -> inf ( A , RR , < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } ) |