Theorem seqvalcd 10232

Description: Value of the sequence builder function. Similar to seq3val 10231 but the classes 𝐷 (type of each term) and 𝐶 (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.)

Hypotheses

Ref	Expression
seqvalcd.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
seqvalcd.r	⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
seqvalcd.f0	⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
seqvalcd.pl	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
seqvalcd.fp1	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)

Assertion

Ref	Expression
seqvalcd	⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Distinct variable groups:   𝑥, + ,𝑦,𝑤,𝑧   𝑥,𝐶,𝑦,𝑤,𝑧   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦,𝑤,𝑧   𝑥,𝑀,𝑦,𝑤,𝑧   𝑥,𝑅,𝑦,𝑤,𝑧   𝜑,𝑥,𝑦,𝑤,𝑧

Allowed substitution hints:   𝐷(𝑧,𝑤)

Proof of Theorem seqvalcd

Dummy variables 𝑎 𝑏 𝑐 𝑘 𝑛 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
2		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
3		ssv 3119	. . . . . . 7 ⊢ 𝐶 ⊆ V
4	3	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
5		eqidd 2140	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
6		simprr 521	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
7		simprl 520	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
8	7	fvoveq1d 5796	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
9	6, 8	oveq12d 5792	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
10		simprl 520	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ≥‘𝑀))
11		simprr 521	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
12		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
13	12	ralrimivva 2514	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
14		oveq1 5781	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
15	14	eleq1d 2208	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
16		oveq2 5782	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
17	16	eleq1d 2208	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
18	15, 17	cbvral2v 2665	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
19	13, 18	sylib 121	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	19	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21		fveq2 5421	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
22	21	eleq1d 2208	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
23		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
24	23	ralrimiva 2505	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
25		fveq2 5421	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
26	25	eleq1d 2208	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
27	26	cbvralv 2654	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
28	24, 27	sylib 121	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	28	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30		eluzp1p1 9351	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (𝑥 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
31	10, 30	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
32	22, 29, 31	rspcdva 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
33		oveq12 5783	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
34	33	eleq1d 2208	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
35	34	rspc2gv 2801	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝐹‘(𝑥 + 1)) ∈ 𝐷) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	11, 32, 35	syl2anc 408	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
37	20, 36	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)
38	5, 9, 10, 11, 37	ovmpod 5898	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
39	38, 37	eqeltrd 2216	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
40		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
41	1, 2, 4, 39, 40	frecuzrdgrclt 10188	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝐶))
42	41	ffnd 5273	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
43		1st2nd2 6073	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
44	43	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
45	44	fveq2d 5425	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
46		df-ov 5777	. . . . . . . . . 10 ⊢ ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
47	45, 46	syl6eqr 2190	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)))
48		xp1st 6063	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶) → (1st ‘𝑢) ∈ (ℤ≥‘𝑀))
49	48	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (1st ‘𝑢) ∈ (ℤ≥‘𝑀))
50		xp2nd 6064	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶) → (2nd ‘𝑢) ∈ 𝐶)
51	50	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (2nd ‘𝑢) ∈ 𝐶)
52	51	elexd 2699	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (2nd ‘𝑢) ∈ V)
53		peano2uz 9378	. . . . . . . . . . . 12 ⊢ ((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀))
54	49, 53	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀))
55	13	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
56		fveq2 5421	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1st ‘𝑢) + 1)))
57	56	eleq1d 2208	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷))
58	24	adantr 274	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
59		eluzp1p1 9351	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘(𝑀 + 1)))
60	49, 59	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘(𝑀 + 1)))
61	57, 58, 60	rspcdva 2794	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷)
62		oveq12 5783	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
63	62	eleq1d 2208	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶))
64	63	rspc2gv 2801	. . . . . . . . . . . . 13 ⊢ (((2nd ‘𝑢) ∈ 𝐶 ∧ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶))
65	51, 61, 64	syl2anc 408	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶))
66	55, 65	mpd 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶)
67	54, 66	opelxpd 4572	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
68		oveq1 5781	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑢) → (𝑥 + 1) = ((1st ‘𝑢) + 1))
69		fvoveq1 5797	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘𝑢) + 1)))
70	69	oveq2d 5790	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘𝑢) + 1))))
71	68, 70	opeq12d 3713	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1st ‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))⟩)
72		oveq1 5781	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘𝑢) → (𝑦 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
73	72	opeq2d 3712	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘𝑢) → ⟨((1st ‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))⟩ = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
74		eqid 2139	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
75	71, 73, 74	ovmpog 5905	. . . . . . . . . 10 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ V ∧ ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
76	49, 52, 67, 75	syl3anc 1216	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
77	47, 76	eqtrd 2172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
78	77, 67	eqeltrd 2216	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
79	78	ralrimiva 2505	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
80		uzid 9340	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
81	1, 80	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
82	81, 2	opelxpd 4572	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
83	79, 82	jca 304	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)))
84		frecfcl 6302	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ≥‘𝑀) × 𝐶))
85		ffn 5272	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
86	83, 84, 85	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
88		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
89	87, 88	eqeq12d 2154	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
90	89	imbi2d 229	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
91		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
92		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
93	91, 92	eqeq12d 2154	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
94	93	imbi2d 229	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
95		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
96		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
97	95, 96	eqeq12d 2154	. . . . . . 7 ⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)))
98	97	imbi2d 229	. . . . . 6 ⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
99		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
100		fveq2 5421	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
101	99, 100	eqeq12d 2154	. . . . . . 7 ⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
102	101	imbi2d 229	. . . . . 6 ⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))))
103	40	fveq1i 5422	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
104		frec0g 6294	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
105	82, 104	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	103, 105	syl5eq 2184	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107		frec0g 6294	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108	82, 107	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	106, 108	eqtr4d 2175	. . . . . 6 ⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
110	41	ad2antlr 480	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝐶))
111		simpll 518	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑘 ∈ ω)
112	110, 111	ffvelrnd 5556	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶))
113		xp1st 6063	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀))
114	112, 113	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀))
115		xp2nd 6064	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (2nd ‘(𝑅‘𝑘)) ∈ 𝐶)
116	112, 115	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	116	elexd 2699	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ V)
118		peano2uz 9378	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘𝑀))
119	114, 118	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘𝑀))
120	13	ad2antlr 480	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
121		fveq2 5421	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
122	121	eleq1d 2208	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
123	28	ad2antlr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
124		eluzp1p1 9351	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘(𝑀 + 1)))
125	114, 124	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘(𝑀 + 1)))
126	122, 123, 125	rspcdva 2794	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
127		oveq12 5783	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
128	127	eleq1d 2208	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
129	128	rspc2gv 2801	. . . . . . . . . . . . 13 ⊢ (((2nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	116, 126, 129	syl2anc 408	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
131	120, 130	mpd 13	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶)
132	119, 131	opelxpd 4572	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
133		oveq1 5781	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1st ‘(𝑅‘𝑘)) + 1))
134		fvoveq1 5797	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
135	134	oveq2d 5790	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
136	133, 135	opeq12d 3713	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
137		oveq1 5781	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
138	137	opeq2d 3712	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
139	136, 138, 74	ovmpog 5905	. . . . . . . . . 10 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ V ∧ ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
140	114, 117, 132, 139	syl3anc 1216	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
141	79	ad2antlr 480	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
142	82	ad2antlr 480	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
143		frecsuc 6304	. . . . . . . . . . 11 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
144	141, 142, 111, 143	syl3anc 1216	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
145		simpr 109	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
146	145	fveq2d 5425	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
147		1st2nd2 6073	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
148	112, 147	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
149	148	fveq2d 5425	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
150		df-ov 5777	. . . . . . . . . . 11 ⊢ ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
151	149, 150	syl6eqr 2190	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))))
152	144, 146, 151	3eqtr2d 2178	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))))
153	44	fveq2d 5425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
154		df-ov 5777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
155	153, 154	syl6eqr 2190	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)))
156		fvoveq1 5797	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘𝑢) + 1)))
157	156	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘𝑢) + 1))))
158		oveq1 5781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2nd ‘𝑢) → (𝑤 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
159		eqid 2139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
160	157, 158, 159	ovmpog 5905	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ 𝐶 ∧ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
161	49, 51, 66, 160	syl3anc 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
162	161, 66	eqeltrd 2216	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝐶)
163	54, 162	opelxpd 4572	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
164		oveq1 5781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
165	68, 164	opeq12d 3713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
166		oveq2 5782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2nd ‘𝑢) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)))
167	166	opeq2d 3712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2nd ‘𝑢) → ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
168		eqid 2139	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
169	165, 167, 168	ovmpog 5905	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ V ∧ ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
170	49, 52, 163, 169	syl3anc 1216	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
171	155, 170	eqtrd 2172	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
172	171, 163	eqeltrd 2216	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
173	172	ralrimiva 2505	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
174	173	ad2antlr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶))
175		frecsuc 6304	. . . . . . . . . . . . . 14 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
176	174, 142, 111, 175	syl3anc 1216	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
177	40	fveq1i 5422	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
178	40	fveq1i 5422	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
179	178	fveq2i 5424	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
180	176, 177, 179	3eqtr4g 2197	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
181	148	fveq2d 5425	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
182	180, 181	eqtrd 2172	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
183		df-ov 5777	. . . . . . . . . . 11 ⊢ ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
184	182, 183	syl6eqr 2190	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))))
185		fvoveq1 5797	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
186	185	oveq2d 5790	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
187		oveq1 5781	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
188	186, 187, 159	ovmpog 5905	. . . . . . . . . . . . . 14 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
189	114, 116, 131, 188	syl3anc 1216	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
190	189, 131	eqeltrd 2216	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝐶)
191	119, 190	opelxpd 4572	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶))
192		oveq1 5781	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
193	133, 192	opeq12d 3713	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
194		oveq2 5782	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))))
195	194	opeq2d 3712	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
196	193, 195, 168	ovmpog 5905	. . . . . . . . . . 11 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ V ∧ ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
197	114, 117, 191, 196	syl3anc 1216	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
198	189	opeq2d 3712	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
199	184, 197, 198	3eqtrd 2176	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
200	140, 152, 199	3eqtr4rd 2183	. . . . . . . 8 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
201	200	exp31 361	. . . . . . 7 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
202	201	a2d 26	. . . . . 6 ⊢ (𝑘 ∈ ω → ((𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
203	90, 94, 98, 102, 109, 202	finds 4514	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
204	203	impcom 124	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
205	42, 86, 204	eqfnfvd 5521	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
206	205	rneqd 4768	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207		df-seqfrec 10219	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
208	206, 207	syl6reqr 2191	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331   ∈ wcel 1480  ∀wral 2416  Vcvv 2686   ⊆ wss 3071  ∅c0 3363  ⟨cop 3530  suc csuc 4287  ωcom 4504   × cxp 4537  ran crn 4540   Fn wfn 5118  ⟶wf 5119  ‘cfv 5123  (class class class)co 5774   ∈ cmpo 5776  1^st c1st 6036  2^nd c2nd 6037  freccfrec 6287  1c1 7621   + caddc 7623  ℤcz 9054  ℤ_≥cuz 9326  seqcseq 10218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-addcom 7720  ax-addass 7722  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-0id 7728  ax-rnegex 7729  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-ltadd 7736

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-inn 8721  df-n0 8978  df-z 9055  df-uz 9327  df-seqfrec 10219

This theorem is referenced by:  seqf2  10237  seq1cd  10238  seqp1cd  10239