Metamath Proof Explorer


Theorem om2uzlt2i

Description: The mapping G (see om2uz0i ) preserves order. (Contributed by NM, 4-May-2005) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1
|- C e. ZZ
om2uz.2
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
Assertion om2uzlt2i
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> ( G ` A ) < ( G ` B ) ) )

Proof

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 ) ) )