seqvalcd - Intuitionistic Logic Explorer

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

Theorem seqvalcd 10532

Description: Value of the sequence builder function. Similar to seq3val 10531 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 10519	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
2		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
4		ssv 3201	. . . . . . 7 ⊢ 𝐶 ⊆ V
5	4	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
6		eqidd 2194	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
7		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
8		simprl 529	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
9	8	fvoveq1d 5940	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
10	7, 9	oveq12d 5936	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
11		simprl 529	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ_≥‘𝑀))
12		simprr 531	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
13		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
14	13	ralrimivva 2576	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
15		oveq1 5925	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
16	15	eleq1d 2262	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
17		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
18	17	eleq1d 2262	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
19	16, 18	cbvral2v 2739	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	14, 19	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21	20	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
22		fveq2 5554	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
23	22	eleq1d 2262	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
24		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
25	24	ralrimiva 2567	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
26		fveq2 5554	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
27	26	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
28	27	cbvralv 2726	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	25, 28	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30	29	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
31		eluzp1p1 9618	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
32	11, 31	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
33	23, 30, 32	rspcdva 2869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
34		oveq12 5927	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
35	34	eleq1d 2262	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	35	rspc2gv 2876	. . . . . . . . . 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 6046	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
40	39, 38	eqeltrd 2270	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
41		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
42	2, 3, 5, 40, 41	frecuzrdgrclt 10486	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
43	42	ffnd 5404	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
44		1st2nd2 6228	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
45	44	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
46	45	fveq2d 5558	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
47		df-ov 5921	. . . . . . . . . 10 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
48	46, 47	eqtr4di 2244	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)))
49		xp1st 6218	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
50	49	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
51		xp2nd 6219	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘𝑢) ∈ 𝐶)
52	51	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ 𝐶)
53	52	elexd 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ V)
54		peano2uz 9648	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
55	50, 54	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
56	14	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
57		fveq2 5554	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1^st ‘𝑢) + 1)))
58	57	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷))
59	25	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
60		eluzp1p1 9618	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
61	50, 60	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
62	58, 59, 61	rspcdva 2869	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷)
63		oveq12 5927	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
64	63	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
65	64	rspc2gv 2876	. . . . . . . . . . . . 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 4692	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
69		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥 + 1) = ((1^st ‘𝑢) + 1))
70		fvoveq1 5941	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
71	70	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))))
72	69, 71	opeq12d 3812	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
73		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘𝑢) → (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
74	73	opeq2d 3811	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
75		eqid 2193	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
76	72, 74, 75	ovmpog 6053	. . . . . . . . . 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 1249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
78	48, 77	eqtrd 2226	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
79	78, 68	eqeltrd 2270	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
80	79	ralrimiva 2567	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
81		uzid 9606	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
82	2, 81	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
83	82, 3	opelxpd 4692	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
84	80, 83	jca 306	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)))
85		frecfcl 6458	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶))
86		ffn 5403	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87	84, 85, 86	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
88		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
89		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
90	88, 89	eqeq12d 2208	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
91	90	imbi2d 230	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
92		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
93		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
94	92, 93	eqeq12d 2208	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
95	94	imbi2d 230	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
96		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
97		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
98	96, 97	eqeq12d 2208	. . . . . . 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 5554	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
101		fveq2 5554	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
102	100, 101	eqeq12d 2208	. . . . . . 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 5555	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
105		frec0g 6450	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	83, 105	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107	104, 106	eqtrid 2238	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108		frec0g 6450	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	83, 108	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
110	107, 109	eqtr4d 2229	. . . . . 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 5694	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶))
114		xp1st 6218	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
115	113, 114	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
116		xp2nd 6219	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	113, 116	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
118	117	elexd 2773	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ V)
119		peano2uz 9648	. . . . . . . . . . . 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 5554	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
123	122	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
124	29	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
125		eluzp1p1 9618	. . . . . . . . . . . . . . 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 2869	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
128		oveq12 5927	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
129	128	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	129	rspc2gv 2876	. . . . . . . . . . . . 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 4692	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
134		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1^st ‘(𝑅‘𝑘)) + 1))
135		fvoveq1 5941	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
136	135	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
137	134, 136	opeq12d 3812	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
138		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
139	138	opeq2d 3811	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
140	137, 139, 75	ovmpog 6053	. . . . . . . . . 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 1249	. . . . . . . . 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 6460	. . . . . . . . . . 11 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
145	142, 143, 112, 144	syl3anc 1249	. . . . . . . . . 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 5558	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
148		1st2nd2 6228	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
149	113, 148	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
150	149	fveq2d 5558	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
151		df-ov 5921	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
152	150, 151	eqtr4di 2244	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
153	145, 147, 152	3eqtr2d 2232	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
154	45	fveq2d 5558	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
155		df-ov 5921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
156	154, 155	eqtr4di 2244	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)))
157		fvoveq1 5941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1^st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
158	157	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1^st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))))
159		oveq1 5925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2^nd ‘𝑢) → (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
160		eqid 2193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
161	158, 159, 160	ovmpog 6053	. . . . . . . . . . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
163	162, 67	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) ∈ 𝐶)
164	55, 163	opelxpd 4692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
165		oveq1 5925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
166	69, 165	opeq12d 3812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
167		oveq2 5926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘𝑢) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)))
168	167	opeq2d 3811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
169		eqid 2193	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170	166, 168, 169	ovmpog 6053	. . . . . . . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
172	156, 171	eqtrd 2226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
173	172, 164	eqeltrd 2270	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
174	173	ralrimiva 2567	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
175	174	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
176		frecsuc 6460	. . . . . . . . . . . . . 14 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
177	175, 143, 112, 176	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
178	41	fveq1i 5555	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
179	41	fveq1i 5555	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
180	179	fveq2i 5557	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
181	177, 178, 180	3eqtr4g 2251	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
182	149	fveq2d 5558	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
183	181, 182	eqtrd 2226	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
184		df-ov 5921	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
185	183, 184	eqtr4di 2244	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))))
186		fvoveq1 5941	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
187	186	oveq2d 5934	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
188		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2^nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
189	187, 188, 160	ovmpog 6053	. . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
191	190, 132	eqeltrd 2270	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) ∈ 𝐶)
192	120, 191	opelxpd 4692	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
193		oveq1 5925	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
194	134, 193	opeq12d 3812	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
195		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))))
196	195	opeq2d 3811	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
197	194, 196, 169	ovmpog 6053	. . . . . . . . . . 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 1249	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
199	190	opeq2d 3811	. . . . . . . . . 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 2230	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
201	141, 153, 200	3eqtr4rd 2237	. . . . . . . 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 4632	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
205	204	impcom 125	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
206	43, 87, 205	eqfnfvd 5658	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207	206	rneqd 4891	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
208	1, 207	eqtr4id 2245	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 ∈ wcel 2164 ∀wral 2472 Vcvv 2760 ⊆ wss 3153 ∅c0 3446 ⟨cop 3621 suc csuc 4396 ωcom 4622 × cxp 4657 ran crn 4660 Fn wfn 5249 ⟶wf 5250 ‘cfv 5254 (class class class)co 5918 ∈ cmpo 5920 1^st c1st 6191 2^nd c2nd 6192 freccfrec 6443 1c1 7873 + caddc 7875 ℤcz 9317 ℤ_≥cuz 9592 seqcseq 10518

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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-0id 7980 ax-rnegex 7981 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-ltadd 7988

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-inn 8983 df-n0 9241 df-z 9318 df-uz 9593 df-seqfrec 10519

This theorem is referenced by: seqf2 10539 seq1cd 10540 seqp1cd 10541

W3C validator