Step |
Hyp |
Ref |
Expression |
1 |
|
om2uz.1 |
|- C e. ZZ |
2 |
|
om2uz.2 |
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om ) |
3 |
1 2
|
om2uzlti |
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B -> ( G ` A ) < ( G ` B ) ) ) |
4 |
1 2
|
om2uzlti |
|- ( ( B e. _om /\ A e. _om ) -> ( B e. A -> ( G ` B ) < ( G ` A ) ) ) |
5 |
|
fveq2 |
|- ( B = A -> ( G ` B ) = ( G ` A ) ) |
6 |
5
|
a1i |
|- ( ( B e. _om /\ A e. _om ) -> ( B = A -> ( G ` B ) = ( G ` A ) ) ) |
7 |
4 6
|
orim12d |
|- ( ( B e. _om /\ A e. _om ) -> ( ( B e. A \/ B = A ) -> ( ( G ` B ) < ( G ` A ) \/ ( G ` B ) = ( G ` A ) ) ) ) |
8 |
7
|
ancoms |
|- ( ( A e. _om /\ B e. _om ) -> ( ( B e. A \/ B = A ) -> ( ( G ` B ) < ( G ` A ) \/ ( G ` B ) = ( G ` A ) ) ) ) |
9 |
|
nnon |
|- ( B e. _om -> B e. On ) |
10 |
|
nnon |
|- ( A e. _om -> A e. On ) |
11 |
|
onsseleq |
|- ( ( B e. On /\ A e. On ) -> ( B C_ A <-> ( B e. A \/ B = A ) ) ) |
12 |
|
ontri1 |
|- ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) ) |
13 |
11 12
|
bitr3d |
|- ( ( B e. On /\ A e. On ) -> ( ( B e. A \/ B = A ) <-> -. A e. B ) ) |
14 |
9 10 13
|
syl2anr |
|- ( ( A e. _om /\ B e. _om ) -> ( ( B e. A \/ B = A ) <-> -. A e. B ) ) |
15 |
1 2
|
om2uzuzi |
|- ( B e. _om -> ( G ` B ) e. ( ZZ>= ` C ) ) |
16 |
|
eluzelre |
|- ( ( G ` B ) e. ( ZZ>= ` C ) -> ( G ` B ) e. RR ) |
17 |
15 16
|
syl |
|- ( B e. _om -> ( G ` B ) e. RR ) |
18 |
1 2
|
om2uzuzi |
|- ( A e. _om -> ( G ` A ) e. ( ZZ>= ` C ) ) |
19 |
|
eluzelre |
|- ( ( G ` A ) e. ( ZZ>= ` C ) -> ( G ` A ) e. RR ) |
20 |
18 19
|
syl |
|- ( A e. _om -> ( G ` A ) e. RR ) |
21 |
|
leloe |
|- ( ( ( G ` B ) e. RR /\ ( G ` A ) e. RR ) -> ( ( G ` B ) <_ ( G ` A ) <-> ( ( G ` B ) < ( G ` A ) \/ ( G ` B ) = ( G ` A ) ) ) ) |
22 |
|
lenlt |
|- ( ( ( G ` B ) e. RR /\ ( G ` A ) e. RR ) -> ( ( G ` B ) <_ ( G ` A ) <-> -. ( G ` A ) < ( G ` B ) ) ) |
23 |
21 22
|
bitr3d |
|- ( ( ( G ` B ) e. RR /\ ( G ` A ) e. RR ) -> ( ( ( G ` B ) < ( G ` A ) \/ ( G ` B ) = ( G ` A ) ) <-> -. ( G ` A ) < ( G ` B ) ) ) |
24 |
17 20 23
|
syl2anr |
|- ( ( A e. _om /\ B e. _om ) -> ( ( ( G ` B ) < ( G ` A ) \/ ( G ` B ) = ( G ` A ) ) <-> -. ( G ` A ) < ( G ` B ) ) ) |
25 |
8 14 24
|
3imtr3d |
|- ( ( A e. _om /\ B e. _om ) -> ( -. A e. B -> -. ( G ` A ) < ( G ` B ) ) ) |
26 |
3 25
|
impcon4bid |
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> ( G ` A ) < ( G ` B ) ) ) |