Theorem noseqrdg0

Description: Initial value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
	om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
	om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
	noseqrdg.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	noseqrdg.2	⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
	noseqrdg.3	⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
Assertion	noseqrdg0	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4		noseqrdg.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		noseqrdg.2	⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
6		noseqrdg.3	⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
7	1 2 3 4 5 6	noseqrdgfn	⊢ ( 𝜑 → 𝑆 Fn 𝑍 )
8	7	fnfund	⊢ ( 𝜑 → Fun 𝑆 )
9		frfnom	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
10	5	fneq1d	⊢ ( 𝜑 → ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω ) )
11	9 10	mpbiri	⊢ ( 𝜑 → 𝑅 Fn ω )
12		peano1	⊢ ∅ ∈ ω
13		fnfvelrn	⊢ ( ( 𝑅 Fn ω ∧ ∅ ∈ ω ) → ( 𝑅 ‘ ∅ ) ∈ ran 𝑅 )
14	11 12 13	sylancl	⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) ∈ ran 𝑅 )
15	5	fveq1d	⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) )
16		opex	⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ V
17		fr0g	⊢ ( ⟨ 𝐶 , 𝐴 ⟩ ∈ V → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
18	16 17	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
19	15 18	eqtr2di	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐴 ⟩ = ( 𝑅 ‘ ∅ ) )
20	14 19 6	3eltr4d	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑆 )
21		funopfv	⊢ ( Fun 𝑆 → ( ⟨ 𝐶 , 𝐴 ⟩ ∈ 𝑆 → ( 𝑆 ‘ 𝐶 ) = 𝐴 ) )
22	8 20 21	sylc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = 𝐴 )