Description: The mapping G is a one-to-one mapping from _om onto a countable sequence of surreals that will be used to show the properties of seq_s . This theorem shows the value of G at ordinal zero. Compare the series of theorems starting at om2uz0i . (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 ) ) |
||
| Assertion | om2noseq0 | |- ( ph -> ( G ` (/) ) = C ) |
| 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 | 2 | fveq1d | |- ( ph -> ( G ` (/) ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` (/) ) ) |
| 4 | fr0g | |- ( C e. No -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` (/) ) = C ) |
|
| 5 | 1 4 | syl | |- ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` (/) ) = C ) |
| 6 | 3 5 | eqtrd | |- ( ph -> ( G ` (/) ) = C ) |