Step |
Hyp |
Ref |
Expression |
1 |
|
df-le |
|- <_ = ( ( RR* X. RR* ) \ `' < ) |
2 |
1
|
ineq1i |
|- ( <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) \ `' < ) i^i ( A X. A ) ) |
3 |
|
indif1 |
|- ( ( ( RR* X. RR* ) \ `' < ) i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < ) |
4 |
2 3
|
eqtri |
|- ( <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < ) |
5 |
|
xpss12 |
|- ( ( A C_ RR* /\ A C_ RR* ) -> ( A X. A ) C_ ( RR* X. RR* ) ) |
6 |
5
|
anidms |
|- ( A C_ RR* -> ( A X. A ) C_ ( RR* X. RR* ) ) |
7 |
|
sseqin2 |
|- ( ( A X. A ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) ) |
8 |
6 7
|
sylib |
|- ( A C_ RR* -> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) ) |
9 |
8
|
difeq1d |
|- ( A C_ RR* -> ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < ) = ( ( A X. A ) \ `' < ) ) |
10 |
4 9
|
eqtr2id |
|- ( A C_ RR* -> ( ( A X. A ) \ `' < ) = ( <_ i^i ( A X. A ) ) ) |
11 |
|
isoeq2 |
|- ( ( ( A X. A ) \ `' < ) = ( <_ i^i ( A X. A ) ) -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) ) ) |
12 |
10 11
|
syl |
|- ( A C_ RR* -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) ) ) |
13 |
1
|
ineq1i |
|- ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) ) |
14 |
|
indif1 |
|- ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < ) |
15 |
13 14
|
eqtri |
|- ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < ) |
16 |
|
xpss12 |
|- ( ( B C_ RR* /\ B C_ RR* ) -> ( B X. B ) C_ ( RR* X. RR* ) ) |
17 |
16
|
anidms |
|- ( B C_ RR* -> ( B X. B ) C_ ( RR* X. RR* ) ) |
18 |
|
sseqin2 |
|- ( ( B X. B ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) ) |
19 |
17 18
|
sylib |
|- ( B C_ RR* -> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) ) |
20 |
19
|
difeq1d |
|- ( B C_ RR* -> ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < ) = ( ( B X. B ) \ `' < ) ) |
21 |
15 20
|
eqtr2id |
|- ( B C_ RR* -> ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) ) |
22 |
|
isoeq3 |
|- ( ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) -> ( F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) ) |
23 |
21 22
|
syl |
|- ( B C_ RR* -> ( F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) ) |
24 |
12 23
|
sylan9bb |
|- ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) ) |
25 |
|
isocnv2 |
|- ( F Isom < , < ( A , B ) <-> F Isom `' < , `' < ( A , B ) ) |
26 |
|
eqid |
|- ( ( A X. A ) \ `' < ) = ( ( A X. A ) \ `' < ) |
27 |
|
eqid |
|- ( ( B X. B ) \ `' < ) = ( ( B X. B ) \ `' < ) |
28 |
26 27
|
isocnv3 |
|- ( F Isom `' < , `' < ( A , B ) <-> F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) ) |
29 |
25 28
|
bitri |
|- ( F Isom < , < ( A , B ) <-> F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) ) |
30 |
|
isores1 |
|- ( F Isom <_ , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , <_ ( A , B ) ) |
31 |
|
isores2 |
|- ( F Isom ( <_ i^i ( A X. A ) ) , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) |
32 |
30 31
|
bitri |
|- ( F Isom <_ , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) |
33 |
24 29 32
|
3bitr4g |
|- ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , < ( A , B ) <-> F Isom <_ , <_ ( A , B ) ) ) |