Theorem nfseqs

Description: Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	nfseqs.1	$$⊢\underset{\_}{Ⅎ}xM$$
	nfseqs.2	$$⊢\underset{\_}{Ⅎ}x\underset{\dot{}}{+}$$
	nfseqs.3	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	nfseqs	$$⊢\underset{\_}{Ⅎ}x{seq}_{s}M\left(\underset{\dot{}}{+},F\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfseqs.1	$$⊢\underset{\_}{Ⅎ}xM$$
2		nfseqs.2	$$⊢\underset{\_}{Ⅎ}x\underset{\dot{}}{+}$$
3		nfseqs.3	$$⊢\underset{\_}{Ⅎ}xF$$
4		df-seqs	$$⊢{seq}_{s}M\left(\underset{\dot{}}{+},F\right)=\mathrm{rec}\left(\left(y\in \mathrm{V},z\in \mathrm{V}⟼⟨y{+}_s{1}_s,z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)⟩\right),⟨M,F\left(M\right)⟩\right)\left[\mathrm{\omega }\right]$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(y{+}_s{1}_s\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
8	3 6	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y{+}_s{1}_s\right)$$
9	7 2 8	nfov	$$⊢\underset{\_}{Ⅎ}x\left(z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)\right)$$
10	6 9	nfop	$$⊢\underset{\_}{Ⅎ}x⟨y{+}_s{1}_s,z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)⟩$$
11	5 5 10	nfmpo	$$⊢\underset{\_}{Ⅎ}x\left(y\in \mathrm{V},z\in \mathrm{V}⟼⟨y{+}_s{1}_s,z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)⟩\right)$$
12	3 1	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(M\right)$$
13	1 12	nfop	$$⊢\underset{\_}{Ⅎ}x⟨M,F\left(M\right)⟩$$
14	11 13	nfrdg	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(\left(y\in \mathrm{V},z\in \mathrm{V}⟼⟨y{+}_s{1}_s,z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)⟩\right),⟨M,F\left(M\right)⟩\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{\omega }$$
16	14 15	nfima	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(\left(y\in \mathrm{V},z\in \mathrm{V}⟼⟨y{+}_s{1}_s,z\underset{\dot{}}{+}F\left(y{+}_s{1}_s\right)⟩\right),⟨M,F\left(M\right)⟩\right)\left[\mathrm{\omega }\right]$$
17	4 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}x{seq}_{s}M\left(\underset{\dot{}}{+},F\right)$$