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