seqsp1

Description: The value of the surreal sequence builder at a successor. (Contributed by Scott Fenton, 19-Apr-2025)

	Ref	Expression
Hypotheses	seqsp1.1	$⊢ φ \to M \in No$
	seqsp1.2	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω]$
	seqsp1.3	$⊢ φ \to N \in Z$
Assertion	seqsp1	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) (N +_{s} 1_{s}) = {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s})$

Proof

Step	Hyp	Ref	Expression
1		seqsp1.1	$⊢ φ \to M \in No$
2		seqsp1.2	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω]$
3		seqsp1.3	$⊢ φ \to N \in Z$
4		eqidd	$⊢ φ \to {rec ((y \in V ⟼ y +_{s} 1_{s}), M) ↾}_{ω} = {rec ((y \in V ⟼ y +_{s} 1_{s}), M) ↾}_{ω}$
5		oveq1	$⊢ x = y \to x +_{s} 1_{s} = y +_{s} 1_{s}$
6	5	cbvmptv	$⊢ (x \in V ⟼ x +_{s} 1_{s}) = (y \in V ⟼ y +_{s} 1_{s})$
7		rdgeq1	$⊢ (x \in V ⟼ x +_{s} 1_{s}) = (y \in V ⟼ y +_{s} 1_{s}) \to rec ((x \in V ⟼ x +_{s} 1_{s}), M) = rec ((y \in V ⟼ y +_{s} 1_{s}), M)$
8	6 7	ax-mp	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), M) = rec ((y \in V ⟼ y +_{s} 1_{s}), M)$
9	8	imaeq1i	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω] = rec ((y \in V ⟼ y +_{s} 1_{s}), M) [ω]$
10	2 9	eqtrdi	$⊢ φ \to Z = rec ((y \in V ⟼ y +_{s} 1_{s}), M) [ω]$
11		fvexd	$⊢ φ \to F (M) \in V$
12		eqidd	$⊢ φ \to {rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω} = {rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω}$
13	12	seqsval	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = ran ({rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω})$
14	1 4 10 11 12 13	noseqrdgsuc	$⊢ (φ \land N \in Z) \to {seq}_{s} M (\underset{˙}{+}, F) (N +_{s} 1_{s}) = N (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) {seq}_{s} M (\underset{˙}{+}, F) (N)$
15	3 14	mpdan	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) (N +_{s} 1_{s}) = N (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) {seq}_{s} M (\underset{˙}{+}, F) (N)$
16	3	elexd	$⊢ φ \to N \in V$
17		fvex	$⊢ {seq}_{s} M (\underset{˙}{+}, F) (N) \in V$
18		fvoveq1	$⊢ w = N \to F (w +_{s} 1_{s}) = F (N +_{s} 1_{s})$
19	18	oveq2d	$⊢ w = N \to t \underset{˙}{+} F (w +_{s} 1_{s}) = t \underset{˙}{+} F (N +_{s} 1_{s})$
20		oveq1	$⊢ t = {seq}_{s} M (\underset{˙}{+}, F) (N) \to t \underset{˙}{+} F (N +_{s} 1_{s}) = {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s})$
21		eqid	$⊢ (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) = (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s}))$
22		ovex	$⊢ {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s}) \in V$
23	19 20 21 22	ovmpo	$⊢ (N \in V \land {seq}_{s} M (\underset{˙}{+}, F) (N) \in V) \to N (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) {seq}_{s} M (\underset{˙}{+}, F) (N) = {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s})$
24	16 17 23	sylancl	$⊢ φ \to N (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) {seq}_{s} M (\underset{˙}{+}, F) (N) = {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s})$
25	15 24	eqtrd	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) (N +_{s} 1_{s}) = {seq}_{s} M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N +_{s} 1_{s})$

Metamath Proof Explorer

Theorem seqsp1

Proof