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 | ⊢ ( 𝜑 → 𝐶 ∈ No ) | |
| om2noseq.2 | ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ) | ||
| Assertion | om2noseq0 | ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | om2noseq.1 | ⊢ ( 𝜑 → 𝐶 ∈ No ) | |
| 2 | om2noseq.2 | ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ) | |
| 3 | 2 | fveq1d | ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ ∅ ) ) |
| 4 | fr0g | ⊢ ( 𝐶 ∈ No → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ ∅ ) = 𝐶 ) | |
| 5 | 1 4 | syl | ⊢ ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ ∅ ) = 𝐶 ) |
| 6 | 3 5 | eqtrd | ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 ) |