seqvalcd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > seqvalcd		GIF version

Theorem seqvalcd 10415

Description: Value of the sequence builder function. Similar to seq3val 10414 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		df-seqfrec 10402	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
2		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
4		ssv 3169	. . . . . . 7 ⊢ 𝐶 ⊆ V
5	4	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
6		eqidd 2171	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
7		simprr 527	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
8		simprl 526	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
9	8	fvoveq1d 5875	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
10	7, 9	oveq12d 5871	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
11		simprl 526	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ_≥‘𝑀))
12		simprr 527	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
13		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
14	13	ralrimivva 2552	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
15		oveq1 5860	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
16	15	eleq1d 2239	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
17		oveq2 5861	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
18	17	eleq1d 2239	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
19	16, 18	cbvral2v 2709	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	14, 19	sylib 121	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21	20	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
22		fveq2 5496	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
23	22	eleq1d 2239	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
24		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
25	24	ralrimiva 2543	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
26		fveq2 5496	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
27	26	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
28	27	cbvralv 2696	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	25, 28	sylib 121	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30	29	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
31		eluzp1p1 9512	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
32	11, 31	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
33	23, 30, 32	rspcdva 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
34		oveq12 5862	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
35	34	eleq1d 2239	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	35	rspc2gv 2846	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝐹‘(𝑥 + 1)) ∈ 𝐷) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
37	12, 33, 36	syl2anc 409	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
38	21, 37	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)
39	6, 10, 11, 12, 38	ovmpod 5980	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
40	39, 38	eqeltrd 2247	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
41		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
42	2, 3, 5, 40, 41	frecuzrdgrclt 10371	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
43	42	ffnd 5348	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
44		1st2nd2 6154	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
45	44	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
46	45	fveq2d 5500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
47		df-ov 5856	. . . . . . . . . 10 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
48	46, 47	eqtr4di 2221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)))
49		xp1st 6144	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
50	49	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
51		xp2nd 6145	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘𝑢) ∈ 𝐶)
52	51	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ 𝐶)
53	52	elexd 2743	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ V)
54		peano2uz 9542	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
55	50, 54	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
56	14	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
57		fveq2 5496	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1^st ‘𝑢) + 1)))
58	57	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷))
59	25	adantr 274	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
60		eluzp1p1 9512	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
61	50, 60	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
62	58, 59, 61	rspcdva 2839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷)
63		oveq12 5862	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
64	63	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
65	64	rspc2gv 2846	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑢) ∈ 𝐶 ∧ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
66	52, 62, 65	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
67	56, 66	mpd 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶)
68	55, 67	opelxpd 4644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
69		oveq1 5860	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥 + 1) = ((1^st ‘𝑢) + 1))
70		fvoveq1 5876	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
71	70	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))))
72	69, 71	opeq12d 3773	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
73		oveq1 5860	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘𝑢) → (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
74	73	opeq2d 3772	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
75		eqid 2170	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
76	72, 74, 75	ovmpog 5987	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘𝑢) ∈ V ∧ ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
77	50, 53, 68, 76	syl3anc 1233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
78	48, 77	eqtrd 2203	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
79	78, 68	eqeltrd 2247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
80	79	ralrimiva 2543	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
81		uzid 9501	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
82	2, 81	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
83	82, 3	opelxpd 4644	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
84	80, 83	jca 304	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)))
85		frecfcl 6384	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶))
86		ffn 5347	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87	84, 85, 86	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
88		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
89		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
90	88, 89	eqeq12d 2185	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
91	90	imbi2d 229	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
92		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
93		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
94	92, 93	eqeq12d 2185	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
95	94	imbi2d 229	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
96		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
97		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
98	96, 97	eqeq12d 2185	. . . . . . 7 ⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)))
99	98	imbi2d 229	. . . . . 6 ⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
100		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
101		fveq2 5496	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
102	100, 101	eqeq12d 2185	. . . . . . 7 ⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
103	102	imbi2d 229	. . . . . 6 ⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))))
104	41	fveq1i 5497	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
105		frec0g 6376	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	83, 105	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107	104, 106	eqtrid 2215	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108		frec0g 6376	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	83, 108	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
110	107, 109	eqtr4d 2206	. . . . . 6 ⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
111	42	ad2antlr 486	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
112		simpll 524	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑘 ∈ ω)
113	111, 112	ffvelrnd 5632	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶))
114		xp1st 6144	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
115	113, 114	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
116		xp2nd 6145	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	113, 116	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
118	117	elexd 2743	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ V)
119		peano2uz 9542	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘𝑀))
120	115, 119	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘𝑀))
121	14	ad2antlr 486	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
122		fveq2 5496	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
123	122	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
124	29	ad2antlr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
125		eluzp1p1 9512	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
126	115, 125	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
127	123, 124, 126	rspcdva 2839	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
128		oveq12 5862	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
129	128	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	129	rspc2gv 2846	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
131	117, 127, 130	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
132	121, 131	mpd 13	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶)
133	120, 132	opelxpd 4644	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
134		oveq1 5860	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1^st ‘(𝑅‘𝑘)) + 1))
135		fvoveq1 5876	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
136	135	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
137	134, 136	opeq12d 3773	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
138		oveq1 5860	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
139	138	opeq2d 3772	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
140	137, 139, 75	ovmpog 5987	. . . . . . . . . 10 ⊢ (((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘(𝑅‘𝑘)) ∈ V ∧ ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
141	115, 118, 133, 140	syl3anc 1233	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
142	80	ad2antlr 486	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
143	83	ad2antlr 486	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
144		frecsuc 6386	. . . . . . . . . . 11 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
145	142, 143, 112, 144	syl3anc 1233	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
146		simpr 109	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
147	146	fveq2d 5500	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
148		1st2nd2 6154	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
149	113, 148	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
150	149	fveq2d 5500	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
151		df-ov 5856	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
152	150, 151	eqtr4di 2221	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
153	145, 147, 152	3eqtr2d 2209	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
154	45	fveq2d 5500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
155		df-ov 5856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
156	154, 155	eqtr4di 2221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)))
157		fvoveq1 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1^st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
158	157	oveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1^st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))))
159		oveq1 5860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2^nd ‘𝑢) → (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
160		eqid 2170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
161	158, 159, 160	ovmpog 5987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘𝑢) ∈ 𝐶 ∧ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
162	50, 52, 67, 161	syl3anc 1233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
163	162, 67	eqeltrd 2247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) ∈ 𝐶)
164	55, 163	opelxpd 4644	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
165		oveq1 5860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
166	69, 165	opeq12d 3773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
167		oveq2 5861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘𝑢) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)))
168	167	opeq2d 3772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
169		eqid 2170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170	166, 168, 169	ovmpog 5987	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘𝑢) ∈ V ∧ ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
171	50, 53, 164, 170	syl3anc 1233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
172	156, 171	eqtrd 2203	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
173	172, 164	eqeltrd 2247	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
174	173	ralrimiva 2543	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
175	174	ad2antlr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
176		frecsuc 6386	. . . . . . . . . . . . . 14 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
177	175, 143, 112, 176	syl3anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
178	41	fveq1i 5497	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
179	41	fveq1i 5497	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
180	179	fveq2i 5499	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
181	177, 178, 180	3eqtr4g 2228	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
182	149	fveq2d 5500	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
183	181, 182	eqtrd 2203	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
184		df-ov 5856	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
185	183, 184	eqtr4di 2221	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))))
186		fvoveq1 5876	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
187	186	oveq2d 5869	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
188		oveq1 5860	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2^nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
189	187, 188, 160	ovmpog 5987	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
190	115, 117, 132, 189	syl3anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
191	190, 132	eqeltrd 2247	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) ∈ 𝐶)
192	120, 191	opelxpd 4644	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
193		oveq1 5860	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
194	134, 193	opeq12d 3773	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
195		oveq2 5861	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))))
196	195	opeq2d 3772	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
197	194, 196, 169	ovmpog 5987	. . . . . . . . . . 11 ⊢ (((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) ∧ (2^nd ‘(𝑅‘𝑘)) ∈ V ∧ ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
198	115, 118, 192, 197	syl3anc 1233	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
199	190	opeq2d 3772	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
200	185, 198, 199	3eqtrd 2207	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
201	141, 153, 200	3eqtr4rd 2214	. . . . . . . 8 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
202	201	exp31 362	. . . . . . 7 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
203	202	a2d 26	. . . . . 6 ⊢ (𝑘 ∈ ω → ((𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
204	91, 95, 99, 103, 110, 203	finds 4584	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
205	204	impcom 124	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
206	43, 87, 205	eqfnfvd 5596	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207	206	rneqd 4840	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
208	1, 207	eqtr4id 2222	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 = wceq 1348 ∈ wcel 2141 ∀wral 2448 Vcvv 2730 ⊆ wss 3121 ∅c0 3414 ⟨cop 3586 suc csuc 4350 ωcom 4574 × cxp 4609 ran crn 4612 Fn wfn 5193 ⟶wf 5194 ‘cfv 5198 (class class class)co 5853 ∈ cmpo 5855 1^st c1st 6117 2^nd c2nd 6118 freccfrec 6369 1c1 7775 + caddc 7777 ℤcz 9212 ℤ_≥cuz 9487 seqcseq 10401

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-addcom 7874 ax-addass 7876 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-0id 7882 ax-rnegex 7883 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-ltadd 7890

This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-inn 8879 df-n0 9136 df-z 9213 df-uz 9488 df-seqfrec 10402

This theorem is referenced by: seqf2 10420 seq1cd 10421 seqp1cd 10422

W3C validator