seqvalcd - Intuitionistic Logic Explorer

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

Theorem seqvalcd 10678

Description: Value of the sequence builder function. Similar to seq3val 10677 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 10665	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
2		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
4		ssv 3246	. . . . . . 7 ⊢ 𝐶 ⊆ V
5	4	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
6		eqidd 2230	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
7		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
8		simprl 529	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
9	8	fvoveq1d 6022	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
10	7, 9	oveq12d 6018	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
11		simprl 529	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ_≥‘𝑀))
12		simprr 531	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
13		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
14	13	ralrimivva 2612	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
15		oveq1 6007	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
16	15	eleq1d 2298	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
17		oveq2 6008	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
18	17	eleq1d 2298	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
19	16, 18	cbvral2v 2778	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	14, 19	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21	20	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
22		fveq2 5626	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
23	22	eleq1d 2298	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
24		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
25	24	ralrimiva 2603	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
26		fveq2 5626	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
27	26	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
28	27	cbvralv 2765	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	25, 28	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30	29	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
31		eluzp1p1 9744	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
32	11, 31	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
33	23, 30, 32	rspcdva 2912	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
34		oveq12 6009	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
35	34	eleq1d 2298	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	35	rspc2gv 2919	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝐹‘(𝑥 + 1)) ∈ 𝐷) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
37	12, 33, 36	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
38	21, 37	mpd 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)
39	6, 10, 11, 12, 38	ovmpod 6131	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
40	39, 38	eqeltrd 2306	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
41		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
42	2, 3, 5, 40, 41	frecuzrdgrclt 10632	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
43	42	ffnd 5473	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
44		1st2nd2 6319	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
45	44	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
46	45	fveq2d 5630	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
47		df-ov 6003	. . . . . . . . . 10 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
48	46, 47	eqtr4di 2280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)))
49		xp1st 6309	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
50	49	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
51		xp2nd 6310	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘𝑢) ∈ 𝐶)
52	51	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ 𝐶)
53	52	elexd 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ V)
54		peano2uz 9774	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
55	50, 54	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
56	14	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
57		fveq2 5626	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1^st ‘𝑢) + 1)))
58	57	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷))
59	25	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
60		eluzp1p1 9744	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
61	50, 60	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
62	58, 59, 61	rspcdva 2912	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷)
63		oveq12 6009	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
64	63	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
65	64	rspc2gv 2919	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘𝑢) ∈ 𝐶 ∧ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
66	52, 62, 65	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
67	56, 66	mpd 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶)
68	55, 67	opelxpd 4751	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
69		oveq1 6007	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥 + 1) = ((1^st ‘𝑢) + 1))
70		fvoveq1 6023	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
71	70	oveq2d 6016	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))))
72	69, 71	opeq12d 3864	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
73		oveq1 6007	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘𝑢) → (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
74	73	opeq2d 3863	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
75		eqid 2229	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
76	72, 74, 75	ovmpog 6138	. . . . . . . . . 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 1271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
78	48, 77	eqtrd 2262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
79	78, 68	eqeltrd 2306	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
80	79	ralrimiva 2603	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
81		uzid 9732	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
82	2, 81	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
83	82, 3	opelxpd 4751	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
84	80, 83	jca 306	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)))
85		frecfcl 6549	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶))
86		ffn 5472	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87	84, 85, 86	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
88		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
89		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
90	88, 89	eqeq12d 2244	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
91	90	imbi2d 230	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
92		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
93		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
94	92, 93	eqeq12d 2244	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
95	94	imbi2d 230	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
96		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
97		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
98	96, 97	eqeq12d 2244	. . . . . . 7 ⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)))
99	98	imbi2d 230	. . . . . 6 ⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
100		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
101		fveq2 5626	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
102	100, 101	eqeq12d 2244	. . . . . . 7 ⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
103	102	imbi2d 230	. . . . . 6 ⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))))
104	41	fveq1i 5627	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
105		frec0g 6541	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	83, 105	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107	104, 106	eqtrid 2274	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108		frec0g 6541	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	83, 108	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
110	107, 109	eqtr4d 2265	. . . . . 6 ⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
111	42	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
112		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑘 ∈ ω)
113	111, 112	ffvelcdmd 5770	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶))
114		xp1st 6309	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
115	113, 114	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
116		xp2nd 6310	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	113, 116	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
118	117	elexd 2813	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ V)
119		peano2uz 9774	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘𝑀))
120	115, 119	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ_≥‘𝑀))
121	14	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
122		fveq2 5626	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
123	122	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
124	29	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
125		eluzp1p1 9744	. . . . . . . . . . . . . . 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 2912	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
128		oveq12 6009	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
129	128	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	129	rspc2gv 2919	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
131	117, 127, 130	syl2anc 411	. . . . . . . . . . . 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 4751	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
134		oveq1 6007	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1^st ‘(𝑅‘𝑘)) + 1))
135		fvoveq1 6023	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
136	135	oveq2d 6016	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
137	134, 136	opeq12d 3864	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
138		oveq1 6007	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
139	138	opeq2d 3863	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
140	137, 139, 75	ovmpog 6138	. . . . . . . . . 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 1271	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
142	80	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
143	83	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
144		frecsuc 6551	. . . . . . . . . . 11 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
145	142, 143, 112, 144	syl3anc 1271	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
146		simpr 110	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
147	146	fveq2d 5630	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
148		1st2nd2 6319	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
149	113, 148	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
150	149	fveq2d 5630	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
151		df-ov 6003	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
152	150, 151	eqtr4di 2280	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
153	145, 147, 152	3eqtr2d 2268	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
154	45	fveq2d 5630	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
155		df-ov 6003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
156	154, 155	eqtr4di 2280	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)))
157		fvoveq1 6023	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1^st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
158	157	oveq2d 6016	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1^st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))))
159		oveq1 6007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2^nd ‘𝑢) → (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
160		eqid 2229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
161	158, 159, 160	ovmpog 6138	. . . . . . . . . . . . . . . . . . . . . 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 1271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
163	162, 67	eqeltrd 2306	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) ∈ 𝐶)
164	55, 163	opelxpd 4751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
165		oveq1 6007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
166	69, 165	opeq12d 3864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
167		oveq2 6008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘𝑢) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)))
168	167	opeq2d 3863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
169		eqid 2229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170	166, 168, 169	ovmpog 6138	. . . . . . . . . . . . . . . . . . 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 1271	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
172	156, 171	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
173	172, 164	eqeltrd 2306	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
174	173	ralrimiva 2603	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
175	174	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
176		frecsuc 6551	. . . . . . . . . . . . . 14 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
177	175, 143, 112, 176	syl3anc 1271	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
178	41	fveq1i 5627	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
179	41	fveq1i 5627	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
180	179	fveq2i 5629	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
181	177, 178, 180	3eqtr4g 2287	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
182	149	fveq2d 5630	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
183	181, 182	eqtrd 2262	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
184		df-ov 6003	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
185	183, 184	eqtr4di 2280	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))))
186		fvoveq1 6023	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
187	186	oveq2d 6016	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
188		oveq1 6007	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2^nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
189	187, 188, 160	ovmpog 6138	. . . . . . . . . . . . . 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 1271	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
191	190, 132	eqeltrd 2306	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) ∈ 𝐶)
192	120, 191	opelxpd 4751	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
193		oveq1 6007	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
194	134, 193	opeq12d 3864	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
195		oveq2 6008	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))))
196	195	opeq2d 3863	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
197	194, 196, 169	ovmpog 6138	. . . . . . . . . . 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 1271	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
199	190	opeq2d 3863	. . . . . . . . . 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 2266	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
201	141, 153, 200	3eqtr4rd 2273	. . . . . . . 8 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
202	201	exp31 364	. . . . . . 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 4691	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
205	204	impcom 125	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
206	43, 87, 205	eqfnfvd 5734	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207	206	rneqd 4952	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
208	1, 207	eqtr4id 2281	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1395 ∈ wcel 2200 ∀wral 2508 Vcvv 2799 ⊆ wss 3197 ∅c0 3491 ⟨cop 3669 suc csuc 4455 ωcom 4681 × cxp 4716 ran crn 4719 Fn wfn 5312 ⟶wf 5313 ‘cfv 5317 (class class class)co 6000 ∈ cmpo 6002 1^st c1st 6282 2^nd c2nd 6283 freccfrec 6534 1c1 7996 + caddc 7998 ℤcz 9442 ℤ_≥cuz 9718 seqcseq 10664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-addcom 8095 ax-addass 8097 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-0id 8103 ax-rnegex 8104 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-ltadd 8111

This theorem depends on definitions: df-bi 117 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-frec 6535 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-inn 9107 df-n0 9366 df-z 9443 df-uz 9719 df-seqfrec 10665

This theorem is referenced by: seqf2 10685 seq1cd 10686 seqp1cd 10687

W3C validator