Metamath Proof Explorer

Theorem om2noseqfo

Description: Function statement for G . (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 om2noseqfo 
|- ( ph -> G : _om -onto-> Z )

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 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) Fn _om
5 2 fneq1d 
 |-  ( ph -> ( G Fn _om <-> ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) Fn _om ) )
6 4 5 mpbiri 
 |-  ( ph -> G Fn _om )
7 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om )
8 7 eqcomi 
 |-  ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om )
9 2 rneqd 
 |-  ( ph -> ran G = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
10 8 9 3 3eqtr4a 
 |-  ( ph -> ran G = Z )
11 df-fo 
 |-  ( G : _om -onto-> Z <-> ( G Fn _om /\ ran G = Z ) )
12 6 10 11 sylanbrc 
 |-  ( ph -> G : _om -onto-> Z )