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	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
	noseq.2	|- ( ph -> A e. No )
Assertion	noseq0	|- ( ph -> A e. Z )

Proof

Step	Hyp	Ref	Expression
1		noseq.1	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
2		noseq.2	|- ( ph -> A e. No )
3		fr0g	|- ( A e. No -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) = A )
4	2 3	syl	|- ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) = A )
5		frfnom	|- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om
6		peano1	|- (/) e. _om
7		fnfvelrn	|- ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
8	5 6 7	mp2an	|- ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
9	4 8	eqeltrrdi	|- ( ph -> A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
10		df-ima	|- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
11	1 10	eqtrdi	|- ( ph -> Z = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
12	9 11	eleqtrrd	|- ( ph -> A e. Z )