seqvalcd - Intuitionistic Logic Explorer

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

Theorem seqvalcd 10492

Description: Value of the sequence builder function. Similar to seq3val 10491 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 10479	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
2		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
4		ssv 3192	. . . . . . 7 ⊢ 𝐶 ⊆ V
5	4	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
6		eqidd 2190	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
7		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
8		simprl 529	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
9	8	fvoveq1d 5919	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
10	7, 9	oveq12d 5915	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
11		simprl 529	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ_≥‘𝑀))
12		simprr 531	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
13		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
14	13	ralrimivva 2572	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
15		oveq1 5904	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
16	15	eleq1d 2258	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
17		oveq2 5905	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
18	17	eleq1d 2258	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
19	16, 18	cbvral2v 2731	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	14, 19	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21	20	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
22		fveq2 5534	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
23	22	eleq1d 2258	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
24		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
25	24	ralrimiva 2563	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
26		fveq2 5534	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
27	26	eleq1d 2258	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
28	27	cbvralv 2718	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	25, 28	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30	29	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
31		eluzp1p1 9585	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
32	11, 31	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
33	23, 30, 32	rspcdva 2861	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
34		oveq12 5906	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
35	34	eleq1d 2258	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	35	rspc2gv 2868	. . . . . . . . . 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 6025	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
40	39, 38	eqeltrd 2266	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
41		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
42	2, 3, 5, 40, 41	frecuzrdgrclt 10448	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
43	42	ffnd 5385	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
44		1st2nd2 6201	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
45	44	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
46	45	fveq2d 5538	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
47		df-ov 5900	. . . . . . . . . 10 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
48	46, 47	eqtr4di 2240	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)))
49		xp1st 6191	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
50	49	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
51		xp2nd 6192	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘𝑢) ∈ 𝐶)
52	51	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ 𝐶)
53	52	elexd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ V)
54		peano2uz 9615	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
55	50, 54	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
56	14	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
57		fveq2 5534	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1^st ‘𝑢) + 1)))
58	57	eleq1d 2258	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷))
59	25	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
60		eluzp1p1 9585	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
61	50, 60	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
62	58, 59, 61	rspcdva 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷)
63		oveq12 5906	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
64	63	eleq1d 2258	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
65	64	rspc2gv 2868	. . . . . . . . . . . . 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 4677	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
69		oveq1 5904	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥 + 1) = ((1^st ‘𝑢) + 1))
70		fvoveq1 5920	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
71	70	oveq2d 5913	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))))
72	69, 71	opeq12d 3801	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
73		oveq1 5904	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘𝑢) → (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
74	73	opeq2d 3800	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
75		eqid 2189	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
76	72, 74, 75	ovmpog 6032	. . . . . . . . . 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 2222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
79	78, 68	eqeltrd 2266	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
80	79	ralrimiva 2563	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
81		uzid 9573	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
82	2, 81	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
83	82, 3	opelxpd 4677	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
84	80, 83	jca 306	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)))
85		frecfcl 6431	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶))
86		ffn 5384	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87	84, 85, 86	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
88		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
89		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
90	88, 89	eqeq12d 2204	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
91	90	imbi2d 230	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
92		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
93		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
94	92, 93	eqeq12d 2204	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
95	94	imbi2d 230	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
96		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
97		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
98	96, 97	eqeq12d 2204	. . . . . . 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 5534	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
101		fveq2 5534	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
102	100, 101	eqeq12d 2204	. . . . . . 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 5535	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
105		frec0g 6423	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	83, 105	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107	104, 106	eqtrid 2234	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108		frec0g 6423	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	83, 108	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
110	107, 109	eqtr4d 2225	. . . . . 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 5673	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶))
114		xp1st 6191	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
115	113, 114	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
116		xp2nd 6192	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	113, 116	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
118	117	elexd 2765	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ V)
119		peano2uz 9615	. . . . . . . . . . . 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 5534	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
123	122	eleq1d 2258	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
124	29	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
125		eluzp1p1 9585	. . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
128		oveq12 5906	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
129	128	eleq1d 2258	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	129	rspc2gv 2868	. . . . . . . . . . . . 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 4677	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
134		oveq1 5904	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1^st ‘(𝑅‘𝑘)) + 1))
135		fvoveq1 5920	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
136	135	oveq2d 5913	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
137	134, 136	opeq12d 3801	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
138		oveq1 5904	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
139	138	opeq2d 3800	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
140	137, 139, 75	ovmpog 6032	. . . . . . . . . 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 6433	. . . . . . . . . . 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 5538	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
148		1st2nd2 6201	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
149	113, 148	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
150	149	fveq2d 5538	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
151		df-ov 5900	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
152	150, 151	eqtr4di 2240	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
153	145, 147, 152	3eqtr2d 2228	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
154	45	fveq2d 5538	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
155		df-ov 5900	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
156	154, 155	eqtr4di 2240	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)))
157		fvoveq1 5920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1^st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
158	157	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1^st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))))
159		oveq1 5904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2^nd ‘𝑢) → (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
160		eqid 2189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
161	158, 159, 160	ovmpog 6032	. . . . . . . . . . . . . . . . . . . . . 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 2266	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) ∈ 𝐶)
164	55, 163	opelxpd 4677	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
165		oveq1 5904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
166	69, 165	opeq12d 3801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
167		oveq2 5905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘𝑢) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)))
168	167	opeq2d 3800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
169		eqid 2189	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170	166, 168, 169	ovmpog 6032	. . . . . . . . . . . . . . . . . . 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 2222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
173	172, 164	eqeltrd 2266	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
174	173	ralrimiva 2563	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
175	174	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
176		frecsuc 6433	. . . . . . . . . . . . . 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 5535	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
179	41	fveq1i 5535	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
180	179	fveq2i 5537	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
181	177, 178, 180	3eqtr4g 2247	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
182	149	fveq2d 5538	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
183	181, 182	eqtrd 2222	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
184		df-ov 5900	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
185	183, 184	eqtr4di 2240	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))))
186		fvoveq1 5920	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
187	186	oveq2d 5913	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
188		oveq1 5904	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2^nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
189	187, 188, 160	ovmpog 6032	. . . . . . . . . . . . . 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 2266	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) ∈ 𝐶)
192	120, 191	opelxpd 4677	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
193		oveq1 5904	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
194	134, 193	opeq12d 3801	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
195		oveq2 5905	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))))
196	195	opeq2d 3800	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
197	194, 196, 169	ovmpog 6032	. . . . . . . . . . 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 3800	. . . . . . . . . 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 2226	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
201	141, 153, 200	3eqtr4rd 2233	. . . . . . . 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 4617	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
205	204	impcom 125	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
206	43, 87, 205	eqfnfvd 5637	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207	206	rneqd 4874	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
208	1, 207	eqtr4id 2241	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 ∈ wcel 2160 ∀wral 2468 Vcvv 2752 ⊆ wss 3144 ∅c0 3437 ⟨cop 3610 suc csuc 4383 ωcom 4607 × cxp 4642 ran crn 4645 Fn wfn 5230 ⟶wf 5231 ‘cfv 5235 (class class class)co 5897 ∈ cmpo 5899 1^st c1st 6164 2^nd c2nd 6165 freccfrec 6416 1c1 7843 + caddc 7845 ℤcz 9284 ℤ_≥cuz 9559 seqcseq 10478

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 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-addcom 7942 ax-addass 7944 ax-distr 7946 ax-i2m1 7947 ax-0lt1 7948 ax-0id 7950 ax-rnegex 7951 ax-cnre 7953 ax-pre-ltirr 7954 ax-pre-ltwlin 7955 ax-pre-lttrn 7956 ax-pre-ltadd 7958

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 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-riota 5852 df-ov 5900 df-oprab 5901 df-mpo 5902 df-1st 6166 df-2nd 6167 df-recs 6331 df-frec 6417 df-pnf 8025 df-mnf 8026 df-xr 8027 df-ltxr 8028 df-le 8029 df-sub 8161 df-neg 8162 df-inn 8951 df-n0 9208 df-z 9285 df-uz 9560 df-seqfrec 10479

This theorem is referenced by: seqf2 10497 seq1cd 10498 seqp1cd 10499

W3C validator