Step |
Hyp |
Ref |
Expression |
1 |
|
cnvordtrestixx.1 |
|- A C_ RR* |
2 |
|
cnvordtrestixx.2 |
|- ( ( x e. A /\ y e. A ) -> ( x [,] y ) C_ A ) |
3 |
|
lern |
|- RR* = ran <_ |
4 |
|
df-rn |
|- ran <_ = dom `' <_ |
5 |
3 4
|
eqtri |
|- RR* = dom `' <_ |
6 |
|
letsr |
|- <_ e. TosetRel |
7 |
|
cnvtsr |
|- ( <_ e. TosetRel -> `' <_ e. TosetRel ) |
8 |
6 7
|
ax-mp |
|- `' <_ e. TosetRel |
9 |
8
|
a1i |
|- ( T. -> `' <_ e. TosetRel ) |
10 |
1
|
a1i |
|- ( T. -> A C_ RR* ) |
11 |
|
brcnvg |
|- ( ( y e. A /\ z e. RR* ) -> ( y `' <_ z <-> z <_ y ) ) |
12 |
11
|
adantlr |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( y `' <_ z <-> z <_ y ) ) |
13 |
|
simpr |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> z e. RR* ) |
14 |
|
simplr |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> x e. A ) |
15 |
|
brcnvg |
|- ( ( z e. RR* /\ x e. A ) -> ( z `' <_ x <-> x <_ z ) ) |
16 |
13 14 15
|
syl2anc |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( z `' <_ x <-> x <_ z ) ) |
17 |
12 16
|
anbi12d |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( ( y `' <_ z /\ z `' <_ x ) <-> ( z <_ y /\ x <_ z ) ) ) |
18 |
|
ancom |
|- ( ( z <_ y /\ x <_ z ) <-> ( x <_ z /\ z <_ y ) ) |
19 |
17 18
|
syl6bb |
|- ( ( ( y e. A /\ x e. A ) /\ z e. RR* ) -> ( ( y `' <_ z /\ z `' <_ x ) <-> ( x <_ z /\ z <_ y ) ) ) |
20 |
19
|
rabbidva |
|- ( ( y e. A /\ x e. A ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } = { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
21 |
|
simpr |
|- ( ( y e. A /\ x e. A ) -> x e. A ) |
22 |
1 21
|
sseldi |
|- ( ( y e. A /\ x e. A ) -> x e. RR* ) |
23 |
|
simpl |
|- ( ( y e. A /\ x e. A ) -> y e. A ) |
24 |
1 23
|
sseldi |
|- ( ( y e. A /\ x e. A ) -> y e. RR* ) |
25 |
|
iccval |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
26 |
22 24 25
|
syl2anc |
|- ( ( y e. A /\ x e. A ) -> ( x [,] y ) = { z e. RR* | ( x <_ z /\ z <_ y ) } ) |
27 |
2
|
ancoms |
|- ( ( y e. A /\ x e. A ) -> ( x [,] y ) C_ A ) |
28 |
26 27
|
eqsstrrd |
|- ( ( y e. A /\ x e. A ) -> { z e. RR* | ( x <_ z /\ z <_ y ) } C_ A ) |
29 |
20 28
|
eqsstrd |
|- ( ( y e. A /\ x e. A ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } C_ A ) |
30 |
29
|
adantl |
|- ( ( T. /\ ( y e. A /\ x e. A ) ) -> { z e. RR* | ( y `' <_ z /\ z `' <_ x ) } C_ A ) |
31 |
5 9 10 30
|
ordtrest2 |
|- ( T. -> ( ordTop ` ( `' <_ i^i ( A X. A ) ) ) = ( ( ordTop ` `' <_ ) |`t A ) ) |
32 |
31
|
mptru |
|- ( ordTop ` ( `' <_ i^i ( A X. A ) ) ) = ( ( ordTop ` `' <_ ) |`t A ) |
33 |
|
tsrps |
|- ( <_ e. TosetRel -> <_ e. PosetRel ) |
34 |
6 33
|
ax-mp |
|- <_ e. PosetRel |
35 |
|
ordtcnv |
|- ( <_ e. PosetRel -> ( ordTop ` `' <_ ) = ( ordTop ` <_ ) ) |
36 |
34 35
|
ax-mp |
|- ( ordTop ` `' <_ ) = ( ordTop ` <_ ) |
37 |
36
|
oveq1i |
|- ( ( ordTop ` `' <_ ) |`t A ) = ( ( ordTop ` <_ ) |`t A ) |
38 |
32 37
|
eqtr2i |
|- ( ( ordTop ` <_ ) |`t A ) = ( ordTop ` ( `' <_ i^i ( A X. A ) ) ) |