noseqrdg0

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

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
4		noseqrdg.1	$⊢ φ \to A \in V$
5		noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
6		noseqrdg.3	$⊢ φ \to S = ran R$
7	1 2 3 4 5 6	noseqrdgfn	$⊢ φ \to S Fn Z$
8	7	fnfund	$⊢ φ \to Fun S$
9		frfnom	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω$
10	5	fneq1d	$⊢ φ \to (R Fn ω \leftrightarrow ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω)$
11	9 10	mpbiri	$⊢ φ \to R Fn ω$
12		peano1	$⊢ \emptyset \in ω$
13		fnfvelrn	$⊢ (R Fn ω \land \emptyset \in ω) \to R (\emptyset) \in ran R$
14	11 12 13	sylancl	$⊢ φ \to R (\emptyset) \in ran R$
15	5	fveq1d	$⊢ φ \to R (\emptyset) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset)$
16		opex	$⊢ ⟨C, A⟩ \in V$
17		fr0g	$⊢ ⟨C, A⟩ \in V \to ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
18	16 17	ax-mp	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
19	15 18	eqtr2di	$⊢ φ \to ⟨C, A⟩ = R (\emptyset)$
20	14 19 6	3eltr4d	$⊢ φ \to ⟨C, A⟩ \in S$
21		funopfv	$⊢ Fun S \to (⟨C, A⟩ \in S \to S (C) = A)$
22	8 20 21	sylc	$⊢ φ \to S (C) = A$

Metamath Proof Explorer