noseqrdgsuc

Description: Successor value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 19-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⟩) ↾}_{ω}$
	noseqrdg.3	$⊢ φ \to S = ran R$
Assertion	noseqrdgsuc	$⊢ (φ \land B \in Z) \to S (B +_{s} 1_{s}) = B F S (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		noseqrdg.3	$⊢ φ \to S = ran R$
7	1 2 3 4 5 6	noseqrdgfn	$⊢ φ \to S Fn Z$
8	7	adantr	$⊢ (φ \land B \in Z) \to S Fn Z$
9	8	fnfund	$⊢ (φ \land B \in Z) \to Fun S$
10	3	adantr	$⊢ (φ \land B \in Z) \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
11	1	adantr	$⊢ (φ \land B \in Z) \to C \in No$
12		simpr	$⊢ (φ \land B \in Z) \to B \in Z$
13	10 11 12	noseqp1	$⊢ (φ \land B \in Z) \to B +_{s} 1_{s} \in Z$
14	1 2 3 4 5	noseqrdglem	$⊢ (φ \land B +_{s} 1_{s} \in Z) \to ⟨B +_{s} 1_{s}, 2^{nd} (R (G^{-1} (B +_{s} 1_{s})))⟩ \in ran R$
15	13 14	syldan	$⊢ (φ \land B \in Z) \to ⟨B +_{s} 1_{s}, 2^{nd} (R (G^{-1} (B +_{s} 1_{s})))⟩ \in ran R$
16	6	adantr	$⊢ (φ \land B \in Z) \to S = ran R$
17	15 16	eleqtrrd	$⊢ (φ \land B \in Z) \to ⟨B +_{s} 1_{s}, 2^{nd} (R (G^{-1} (B +_{s} 1_{s})))⟩ \in S$
18		funopfv	$⊢ Fun S \to (⟨B +_{s} 1_{s}, 2^{nd} (R (G^{-1} (B +_{s} 1_{s})))⟩ \in S \to S (B +_{s} 1_{s}) = 2^{nd} (R (G^{-1} (B +_{s} 1_{s}))))$
19	9 17 18	sylc	$⊢ (φ \land B \in Z) \to S (B +_{s} 1_{s}) = 2^{nd} (R (G^{-1} (B +_{s} 1_{s})))$
20	1 2 3	om2noseqf1o	$⊢ φ \to G : ω \underset{1-1 onto}{⟶} Z$
21	20	adantr	$⊢ (φ \land B \in Z) \to G : ω \underset{1-1 onto}{⟶} Z$
22		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land B \in Z) \to G^{-1} (B) \in ω$
23	20 22	sylan	$⊢ (φ \land B \in Z) \to G^{-1} (B) \in ω$
24		peano2	$⊢ G^{-1} (B) \in ω \to suc G^{-1} (B) \in ω$
25	23 24	syl	$⊢ (φ \land B \in Z) \to suc G^{-1} (B) \in ω$
26	21 25	jca	$⊢ (φ \land B \in Z) \to (G : ω \underset{1-1 onto}{⟶} Z \land suc G^{-1} (B) \in ω)$
27	2	adantr	$⊢ (φ \land B \in Z) \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
28	11 27 23	om2noseqsuc	$⊢ (φ \land B \in Z) \to G (suc G^{-1} (B)) = G (G^{-1} (B)) +_{s} 1_{s}$
29		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land B \in Z) \to G (G^{-1} (B)) = B$
30	20 29	sylan	$⊢ (φ \land B \in Z) \to G (G^{-1} (B)) = B$
31	30	oveq1d	$⊢ (φ \land B \in Z) \to G (G^{-1} (B)) +_{s} 1_{s} = B +_{s} 1_{s}$
32	28 31	eqtrd	$⊢ (φ \land B \in Z) \to G (suc G^{-1} (B)) = B +_{s} 1_{s}$
33		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land suc G^{-1} (B) \in ω) \to (G (suc G^{-1} (B)) = B +_{s} 1_{s} \to G^{-1} (B +_{s} 1_{s}) = suc G^{-1} (B))$
34	26 32 33	sylc	$⊢ (φ \land B \in Z) \to G^{-1} (B +_{s} 1_{s}) = suc G^{-1} (B)$
35	34	fveq2d	$⊢ (φ \land B \in Z) \to R (G^{-1} (B +_{s} 1_{s})) = R (suc G^{-1} (B))$
36	35	fveq2d	$⊢ (φ \land B \in Z) \to 2^{nd} (R (G^{-1} (B +_{s} 1_{s}))) = 2^{nd} (R (suc G^{-1} (B)))$
37	19 36	eqtrd	$⊢ (φ \land B \in Z) \to S (B +_{s} 1_{s}) = 2^{nd} (R (suc G^{-1} (B)))$
38		frsuc	$⊢ G^{-1} (B) \in ω \to ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B)) = (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⟩) ↾}_{ω}) (G^{-1} (B)))$
39	38	adantl	$⊢ (φ \land G^{-1} (B) \in ω) \to ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B)) = (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⟩) ↾}_{ω}) (G^{-1} (B)))$
40	5	fveq1d	$⊢ φ \to R (suc G^{-1} (B)) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B))$
41	40	adantr	$⊢ (φ \land G^{-1} (B) \in ω) \to R (suc G^{-1} (B)) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (suc G^{-1} (B))$
42	5	fveq1d	$⊢ φ \to R (G^{-1} (B)) = ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) (G^{-1} (B))$
43	42	fveq2d	$⊢ φ \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (G^{-1} (B))) = (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⟩) ↾}_{ω}) (G^{-1} (B)))$
44	43	adantr	$⊢ (φ \land G^{-1} (B) \in ω) \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (G^{-1} (B))) = (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⟩) ↾}_{ω}) (G^{-1} (B)))$
45	39 41 44	3eqtr4d	$⊢ (φ \land G^{-1} (B) \in ω) \to R (suc G^{-1} (B)) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (G^{-1} (B)))$
46	1 2 3 4 5	om2noseqrdg	$⊢ (φ \land G^{-1} (B) \in ω) \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
47	46	fveq2d	$⊢ (φ \land G^{-1} (B) \in ω) \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (G^{-1} (B))) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩)$
48		df-ov	$⊢ G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (G^{-1} (B))) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩)$
49	47 48	eqtr4di	$⊢ (φ \land G^{-1} (B) \in ω) \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) (R (G^{-1} (B))) = G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (G^{-1} (B)))$
50	45 49	eqtrd	$⊢ (φ \land G^{-1} (B) \in ω) \to R (suc G^{-1} (B)) = G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (G^{-1} (B)))$
51		fvex	$⊢ G (G^{-1} (B)) \in V$
52		fvex	$⊢ 2^{nd} (R (G^{-1} (B))) \in V$
53		oveq1	$⊢ z = G (G^{-1} (B)) \to z +_{s} 1_{s} = G (G^{-1} (B)) +_{s} 1_{s}$
54		oveq1	$⊢ z = G (G^{-1} (B)) \to z F w = G (G^{-1} (B)) F w$
55	53 54	opeq12d	$⊢ z = G (G^{-1} (B)) \to ⟨z +_{s} 1_{s}, z F w⟩ = ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F w⟩$
56		oveq2	$⊢ w = 2^{nd} (R (G^{-1} (B))) \to G (G^{-1} (B)) F w = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
57	56	opeq2d	$⊢ w = 2^{nd} (R (G^{-1} (B))) \to ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F w⟩ = ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
58		oveq1	$⊢ x = z \to x +_{s} 1_{s} = z +_{s} 1_{s}$
59		oveq1	$⊢ x = z \to x F y = z F y$
60	58 59	opeq12d	$⊢ x = z \to ⟨x +_{s} 1_{s}, x F y⟩ = ⟨z +_{s} 1_{s}, z F y⟩$
61		oveq2	$⊢ y = w \to z F y = z F w$
62	61	opeq2d	$⊢ y = w \to ⟨z +_{s} 1_{s}, z F y⟩ = ⟨z +_{s} 1_{s}, z F w⟩$
63	60 62	cbvmpov	$⊢ (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) = (z \in V, w \in V ⟼ ⟨z +_{s} 1_{s}, z F w⟩)$
64		opex	$⊢ ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩ \in V$
65	55 57 63 64	ovmpo	$⊢ (G (G^{-1} (B)) \in V \land 2^{nd} (R (G^{-1} (B))) \in V) \to G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (G^{-1} (B))) = ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
66	51 52 65	mp2an	$⊢ G (G^{-1} (B)) (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩) 2^{nd} (R (G^{-1} (B))) = ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
67	50 66	eqtrdi	$⊢ (φ \land G^{-1} (B) \in ω) \to R (suc G^{-1} (B)) = ⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩$
68	67	fveq2d	$⊢ (φ \land G^{-1} (B) \in ω) \to 2^{nd} (R (suc G^{-1} (B))) = 2^{nd} (⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩)$
69		ovex	$⊢ G (G^{-1} (B)) +_{s} 1_{s} \in V$
70		ovex	$⊢ G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B))) \in V$
71	69 70	op2nd	$⊢ 2^{nd} (⟨G (G^{-1} (B)) +_{s} 1_{s}, G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))⟩) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
72	68 71	eqtrdi	$⊢ (φ \land G^{-1} (B) \in ω) \to 2^{nd} (R (suc G^{-1} (B))) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
73	23 72	syldan	$⊢ (φ \land B \in Z) \to 2^{nd} (R (suc G^{-1} (B))) = G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B)))$
74	1 2 3 4 5	noseqrdglem	$⊢ (φ \land B \in Z) \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$
75	74 16	eleqtrrd	$⊢ (φ \land B \in Z) \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in S$
76		funopfv	$⊢ Fun S \to (⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in S \to S (B) = 2^{nd} (R (G^{-1} (B))))$
77	9 75 76	sylc	$⊢ (φ \land B \in Z) \to S (B) = 2^{nd} (R (G^{-1} (B)))$
78	77	eqcomd	$⊢ (φ \land B \in Z) \to 2^{nd} (R (G^{-1} (B))) = S (B)$
79	30 78	oveq12d	$⊢ (φ \land B \in Z) \to G (G^{-1} (B)) F 2^{nd} (R (G^{-1} (B))) = B F S (B)$
80	37 73 79	3eqtrd	$⊢ (φ \land B \in Z) \to S (B +_{s} 1_{s}) = B F S (B)$

Metamath Proof Explorer

Theorem noseqrdgsuc

Proof