om2noseqrdg

Description: A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function F ( x , y ) and initial value A . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	$⊢ φ \to C \in No$
	om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
	om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
	noseqrdg.1	$⊢ φ \to A \in V$
	noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
Assertion	om2noseqrdg	$⊢ (φ \land B \in ω) \to R (B) = ⟨G (B), 2^{nd} (R (B))⟩$

Proof

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		fveq2	$⊢ z = \emptyset \to R (z) = R (\emptyset)$
7		fveq2	$⊢ z = \emptyset \to G (z) = G (\emptyset)$
8		2fveq3	$⊢ z = \emptyset \to 2^{nd} (R (z)) = 2^{nd} (R (\emptyset))$
9	7 8	opeq12d	$⊢ z = \emptyset \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩$
10	6 9	eqeq12d	$⊢ z = \emptyset \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (\emptyset) = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩)$
11	10	imbi2d	$⊢ z = \emptyset \to ((φ \to R (z) = ⟨G (z), 2^{nd} (R (z))⟩) \leftrightarrow (φ \to R (\emptyset) = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩))$
12		fveq2	$⊢ z = v \to R (z) = R (v)$
13		fveq2	$⊢ z = v \to G (z) = G (v)$
14		2fveq3	$⊢ z = v \to 2^{nd} (R (z)) = 2^{nd} (R (v))$
15	13 14	opeq12d	$⊢ z = v \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (v), 2^{nd} (R (v))⟩$
16	12 15	eqeq12d	$⊢ z = v \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (v) = ⟨G (v), 2^{nd} (R (v))⟩)$
17	16	imbi2d	$⊢ z = v \to ((φ \to R (z) = ⟨G (z), 2^{nd} (R (z))⟩) \leftrightarrow (φ \to R (v) = ⟨G (v), 2^{nd} (R (v))⟩))$
18		fveq2	$⊢ z = suc v \to R (z) = R (suc v)$
19		fveq2	$⊢ z = suc v \to G (z) = G (suc v)$
20		2fveq3	$⊢ z = suc v \to 2^{nd} (R (z)) = 2^{nd} (R (suc v))$
21	19 20	opeq12d	$⊢ z = suc v \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (suc v), 2^{nd} (R (suc v))⟩$
22	18 21	eqeq12d	$⊢ z = suc v \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩)$
23	22	imbi2d	$⊢ z = suc v \to ((φ \to R (z) = ⟨G (z), 2^{nd} (R (z))⟩) \leftrightarrow (φ \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩))$
24		fveq2	$⊢ z = B \to R (z) = R (B)$
25		fveq2	$⊢ z = B \to G (z) = G (B)$
26		2fveq3	$⊢ z = B \to 2^{nd} (R (z)) = 2^{nd} (R (B))$
27	25 26	opeq12d	$⊢ z = B \to ⟨G (z), 2^{nd} (R (z))⟩ = ⟨G (B), 2^{nd} (R (B))⟩$
28	24 27	eqeq12d	$⊢ z = B \to (R (z) = ⟨G (z), 2^{nd} (R (z))⟩ \leftrightarrow R (B) = ⟨G (B), 2^{nd} (R (B))⟩)$
29	28	imbi2d	$⊢ z = B \to ((φ \to R (z) = ⟨G (z), 2^{nd} (R (z))⟩) \leftrightarrow (φ \to R (B) = ⟨G (B), 2^{nd} (R (B))⟩))$
30	5	fveq1d	$⊢ φ \to R (\emptyset) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset)$
31		opex	$⊢ ⟨C, A⟩ \in V$
32		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⟩$
33	31 32	ax-mp	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (\emptyset) = ⟨C, A⟩$
34	30 33	eqtrdi	$⊢ φ \to R (\emptyset) = ⟨C, A⟩$
35	1 2	om2noseq0	$⊢ φ \to G (\emptyset) = C$
36	34	fveq2d	$⊢ φ \to 2^{nd} (R (\emptyset)) = 2^{nd} (⟨C, A⟩)$
37		op2ndg	$⊢ (C \in No \land A \in V) \to 2^{nd} (⟨C, A⟩) = A$
38	1 4 37	syl2anc	$⊢ φ \to 2^{nd} (⟨C, A⟩) = A$
39	36 38	eqtrd	$⊢ φ \to 2^{nd} (R (\emptyset)) = A$
40	35 39	opeq12d	$⊢ φ \to ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩ = ⟨C, A⟩$
41	34 40	eqtr4d	$⊢ φ \to R (\emptyset) = ⟨G (\emptyset), 2^{nd} (R (\emptyset))⟩$
42		frsuc	$⊢ v \in ω \to ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v))$
43	42	adantl	$⊢ (φ \land v \in ω) \to ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v))$
44	5	fveq1d	$⊢ φ \to R (suc v) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v)$
45	44	adantr	$⊢ (φ \land v \in ω) \to R (suc v) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc v)$
46	5	fveq1d	$⊢ φ \to R (v) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v)$
47	46	fveq2d	$⊢ φ \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v)) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v))$
48	47	adantr	$⊢ (φ \land v \in ω) \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v)) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (v))$
49	43 45 48	3eqtr4d	$⊢ (φ \land v \in ω) \to R (suc v) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v))$
50	49	adantrr	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to R (suc v) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v))$
51		fveq2	$⊢ R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v)) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩)$
52		df-ov	$⊢ G (v) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (v)) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩)$
53		fvex	$⊢ G (v) \in V$
54		fvex	$⊢ 2^{nd} (R (v)) \in V$
55		oveq1	$⊢ w = G (v) \to w +_{s} 1_{s} = G (v) +_{s} 1_{s}$
56		oveq1	$⊢ w = G (v) \to w F z = G (v) F z$
57	55 56	opeq12d	$⊢ w = G (v) \to ⟨w +_{s} 1_{s}, w F z⟩ = ⟨G (v) +_{s} 1_{s}, G (v) F z⟩$
58		oveq2	$⊢ z = 2^{nd} (R (v)) \to G (v) F z = G (v) F 2^{nd} (R (v))$
59	58	opeq2d	$⊢ z = 2^{nd} (R (v)) \to ⟨G (v) +_{s} 1_{s}, G (v) F z⟩ = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
60		oveq1	$⊢ x = w \to x +_{s} 1_{s} = w +_{s} 1_{s}$
61		oveq1	$⊢ x = w \to x F y = w F y$
62	60 61	opeq12d	$⊢ x = w \to ⟨x +_{s} 1_{s}, x F y⟩ = ⟨w +_{s} 1_{s}, w F y⟩$
63		oveq2	$⊢ y = z \to w F y = w F z$
64	63	opeq2d	$⊢ y = z \to ⟨w +_{s} 1_{s}, w F y⟩ = ⟨w +_{s} 1_{s}, w F z⟩$
65	62 64	cbvmpov	$⊢ (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) = (w \in V, z \in V ⟼ ⟨w +_{s} 1_{s}, w F z⟩)$
66		opex	$⊢ ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩ \in V$
67	57 59 65 66	ovmpo	$⊢ (G (v) \in V \land 2^{nd} (R (v)) \in V) \to G (v) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (v)) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
68	53 54 67	mp2an	$⊢ G (v) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (v)) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
69	52 68	eqtr3i	$⊢ (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (⟨G (v), 2^{nd} (R (v))⟩) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
70	51 69	eqtrdi	$⊢ R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v)) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
71	70	ad2antll	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (v)) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
72	50 71	eqtrd	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to R (suc v) = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
73	1	adantr	$⊢ (φ \land v \in ω) \to C \in No$
74	2	adantr	$⊢ (φ \land v \in ω) \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
75		simpr	$⊢ (φ \land v \in ω) \to v \in ω$
76	73 74 75	om2noseqsuc	$⊢ (φ \land v \in ω) \to G (suc v) = G (v) +_{s} 1_{s}$
77	76	adantrr	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to G (suc v) = G (v) +_{s} 1_{s}$
78	72	fveq2d	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to 2^{nd} (R (suc v)) = 2^{nd} (⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩)$
79		ovex	$⊢ G (v) +_{s} 1_{s} \in V$
80		ovex	$⊢ G (v) F 2^{nd} (R (v)) \in V$
81	79 80	op2nd	$⊢ 2^{nd} (⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩) = G (v) F 2^{nd} (R (v))$
82	78 81	eqtrdi	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to 2^{nd} (R (suc v)) = G (v) F 2^{nd} (R (v))$
83	77 82	opeq12d	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to ⟨G (suc v), 2^{nd} (R (suc v))⟩ = ⟨G (v) +_{s} 1_{s}, G (v) F 2^{nd} (R (v))⟩$
84	72 83	eqtr4d	$⊢ (φ \land (v \in ω \land R (v) = ⟨G (v), 2^{nd} (R (v))⟩)) \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩$
85	84	exp32	$⊢ φ \to (v \in ω \to (R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩))$
86	85	com12	$⊢ v \in ω \to (φ \to (R (v) = ⟨G (v), 2^{nd} (R (v))⟩ \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩))$
87	86	a2d	$⊢ v \in ω \to ((φ \to R (v) = ⟨G (v), 2^{nd} (R (v))⟩) \to (φ \to R (suc v) = ⟨G (suc v), 2^{nd} (R (suc v))⟩))$
88	11 17 23 29 41 87	finds	$⊢ B \in ω \to (φ \to R (B) = ⟨G (B), 2^{nd} (R (B))⟩)$
89	88	impcom	$⊢ (φ \land B \in ω) \to R (B) = ⟨G (B), 2^{nd} (R (B))⟩$

Metamath Proof Explorer

Theorem om2noseqrdg

Proof