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