Theorem noseq0

Description: The surreal A is a member of the sequence starting at A . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
	noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
Assertion	noseq0	⊢ ( 𝜑 → 𝐴 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2		noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
3		fr0g	⊢ ( 𝐴 ∈ No → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
4	2 3	syl	⊢ ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
5		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω
6		peano1	⊢ ∅ ∈ ω
7		fnfvelrn	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
8	5 6 7	mp2an	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
9	4 8	eqeltrrdi	⊢ ( 𝜑 → 𝐴 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
10		df-ima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
11	1 10	eqtrdi	⊢ ( 𝜑 → 𝑍 = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
12	9 11	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ 𝑍 )