Metamath Proof Explorer

Theorem om2noseqoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 
|- ( ph -> C e. No )
om2noseq.2 
|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
om2noseq.3 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
Assertion om2noseqoi 
|- ( ph -> G = OrdIso (

Proof

Step Hyp Ref Expression
1 om2noseq.1 
 |-  ( ph -> C e. No )
2 om2noseq.2 
 |-  ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3 om2noseq.3 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
4 1 2 3 om2noseqiso 
 |-  ( ph -> G Isom _E ,
5 ordom 
 |-  Ord _om
6 4 5 jctil 
 |-  ( ph -> ( Ord _om /\ G Isom _E ,
7 ordwe 
 |-  ( Ord _om -> _E We _om )
8 5 7 ax-mp 
 |-  _E We _om
9 isowe 
 |-  ( G Isom _E ,  ( _E We _om <->
10 4 9 syl 
 |-  ( ph -> ( _E We _om <->
11 8 10 mpbii 
 |-  ( ph ->
12 3 noseqex 
 |-  ( ph -> Z e. _V )
13 exse 
 |-  ( Z e. _V ->
14 12 13 syl 
 |-  ( ph ->
15 eqid 
 |-  OrdIso (
16 15 oieu 
 |-  ( (  ( ( Ord _om /\ G Isom _E ,  ( _om = dom OrdIso (
17 11 14 16 syl2anc 
 |-  ( ph -> ( ( Ord _om /\ G Isom _E ,  ( _om = dom OrdIso (
18 6 17 mpbid 
 |-  ( ph -> ( _om = dom OrdIso (
19 18 simprd 
 |-  ( ph -> G = OrdIso (