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