Metamath Proof Explorer

Theorem om2uzoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Mario Carneiro, 2-Jun-2015)

Ref Expression
Hypotheses om2uz.1 
|- C e. ZZ
om2uz.2 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
Assertion om2uzoi 
|- G = OrdIso ( < , ( ZZ>= ` C ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 ordom 
 |-  Ord _om
4 1 2 om2uzisoi 
 |-  G Isom _E , < ( _om , ( ZZ>= ` C ) )
5 3 4 pm3.2i 
 |-  ( Ord _om /\ G Isom _E , < ( _om , ( ZZ>= ` C ) ) )
6 ordwe 
 |-  ( Ord _om -> _E We _om )
7 3 6 ax-mp 
 |-  _E We _om
8 isowe 
 |-  ( G Isom _E , < ( _om , ( ZZ>= ` C ) ) -> ( _E We _om <-> < We ( ZZ>= ` C ) ) )
9 4 8 ax-mp 
 |-  ( _E We _om <-> < We ( ZZ>= ` C ) )
10 7 9 mpbi 
 |-  < We ( ZZ>= ` C )
11 fvex 
 |-  ( ZZ>= ` C ) e. _V
12 exse 
 |-  ( ( ZZ>= ` C ) e. _V -> < Se ( ZZ>= ` C ) )
13 11 12 ax-mp 
 |-  < Se ( ZZ>= ` C )
14 eqid 
 |-  OrdIso ( < , ( ZZ>= ` C ) ) = OrdIso ( < , ( ZZ>= ` C ) )
15 14 oieu 
 |-  ( ( < We ( ZZ>= ` C ) /\ < Se ( ZZ>= ` C ) ) -> ( ( Ord _om /\ G Isom _E , < ( _om , ( ZZ>= ` C ) ) ) <-> ( _om = dom OrdIso ( < , ( ZZ>= ` C ) ) /\ G = OrdIso ( < , ( ZZ>= ` C ) ) ) ) )
16 10 13 15 mp2an 
 |-  ( ( Ord _om /\ G Isom _E , < ( _om , ( ZZ>= ` C ) ) ) <-> ( _om = dom OrdIso ( < , ( ZZ>= ` C ) ) /\ G = OrdIso ( < , ( ZZ>= ` C ) ) ) )
17 5 16 mpbi 
 |-  ( _om = dom OrdIso ( < , ( ZZ>= ` C ) ) /\ G = OrdIso ( < , ( ZZ>= ` C ) ) )
18 17 simpri 
 |-  G = OrdIso ( < , ( ZZ>= ` C ) )