seqvalcd - Intuitionistic Logic Explorer

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

Theorem seqvalcd 10847

Description: Value of the sequence builder function. Similar to seq3val 10846 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 10834	. 2 ⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
2		seqvalcd.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		seqvalcd.f0	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)
4		ssv 3264	. . . . . . 7 ⊢ 𝐶 ⊆ V
5	4	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ V)
6		eqidd 2235	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))))
7		simprr 533	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
8		simprl 531	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥)
9	8	fvoveq1d 6080	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1)))
10	7, 9	oveq12d 6076	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1))))
11		simprl 531	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ_≥‘𝑀))
12		simprr 533	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
13		seqvalcd.pl	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)
14	13	ralrimivva 2626	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
15		oveq1 6065	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
16	15	eleq1d 2303	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶))
17		oveq2 6066	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏))
18	17	eleq1d 2303	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶))
19	16, 18	cbvral2v 2793	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
20	14, 19	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
21	20	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶)
22		fveq2 5675	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1)))
23	22	eleq1d 2303	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷))
24		seqvalcd.fp1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)
25	24	ralrimiva 2617	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
26		fveq2 5675	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
27	26	eleq1d 2303	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷))
28	27	cbvralv 2780	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
29	25, 28	sylib 122	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
30	29	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
31		eluzp1p1 9898	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
32	11, 31	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
33	23, 30, 32	rspcdva 2928	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷)
34		oveq12 6067	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1))))
35	34	eleq1d 2303	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶))
36	35	rspc2gv 2936	. . . . . . . . . 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 6189	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))))
40	39, 38	eqeltrd 2311	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶)
41		seqvalcd.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
42	2, 3, 5, 40, 41	frecuzrdgrclt 10801	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ_≥‘𝑀) × 𝐶))
43	42	ffnd 5514	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
44		1st2nd2 6382	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
45	44	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → 𝑢 = ⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
46	45	fveq2d 5679	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
47		df-ov 6061	. . . . . . . . . 10 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
48	46, 47	eqtr4di 2285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)))
49		xp1st 6372	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
50	49	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (1^st ‘𝑢) ∈ (ℤ_≥‘𝑀))
51		xp2nd 6373	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘𝑢) ∈ 𝐶)
52	51	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ 𝐶)
53	52	elexd 2829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (2^nd ‘𝑢) ∈ V)
54		peano2uz 9933	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
55	50, 54	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘𝑀))
56	14	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶)
57		fveq2 5675	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1^st ‘𝑢) + 1)))
58	57	eleq1d 2303	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1^st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷))
59	25	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷)
60		eluzp1p1 9898	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) ∈ (ℤ_≥‘𝑀) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
61	50, 60	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
62	58, 59, 61	rspcdva 2928	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → (𝐹‘((1^st ‘𝑢) + 1)) ∈ 𝐷)
63		oveq12 6067	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
64	63	eleq1d 2303	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1^st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))) ∈ 𝐶))
65	64	rspc2gv 2936	. . . . . . . . . . . . 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 4787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
69		oveq1 6065	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥 + 1) = ((1^st ‘𝑢) + 1))
70		fvoveq1 6081	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
71	70	oveq2d 6074	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))))
72	69, 71	opeq12d 3896	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
73		oveq1 6065	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘𝑢) → (𝑦 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
74	73	opeq2d 3895	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), (𝑦 + (𝐹‘((1^st ‘𝑢) + 1)))⟩ = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
75		eqid 2234	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
76	72, 74, 75	ovmpog 6196	. . . . . . . . . 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 1274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
78	48, 77	eqtrd 2267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1)))⟩)
79	78, 68	eqeltrd 2311	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
80	79	ralrimiva 2617	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
81		uzid 9886	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
82	2, 81	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
83	82, 3	opelxpd 4787	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
84	80, 83	jca 306	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)))
85		frecfcl 6649	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶))
86		ffn 5513	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ_≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
87	84, 85, 86	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
88		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
89		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
90	88, 89	eqeq12d 2249	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
91	90	imbi2d 230	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
92		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
93		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
94	92, 93	eqeq12d 2249	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
95	94	imbi2d 230	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
96		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
97		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
98	96, 97	eqeq12d 2249	. . . . . . 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 5675	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
101		fveq2 5675	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
102	100, 101	eqeq12d 2249	. . . . . . 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 5676	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
105		frec0g 6641	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
106	83, 105	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
107	104, 106	eqtrid 2279	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
108		frec0g 6641	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
109	83, 108	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
110	107, 109	eqtr4d 2270	. . . . . 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 5818	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶))
114		xp1st 6372	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
115	113, 114	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1^st ‘(𝑅‘𝑘)) ∈ (ℤ_≥‘𝑀))
116		xp2nd 6373	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
117	113, 116	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ 𝐶)
118	117	elexd 2829	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2^nd ‘(𝑅‘𝑘)) ∈ V)
119		peano2uz 9933	. . . . . . . . . . . 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 5675	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
123	122	eleq1d 2303	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ((1^st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷))
124	29	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ_≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷)
125		eluzp1p1 9898	. . . . . . . . . . . . . . 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 2928	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)
128		oveq12 6067	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
129	128	eleq1d 2303	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (2^nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶))
130	129	rspc2gv 2936	. . . . . . . . . . . . 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 4787	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
134		oveq1 6065	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1^st ‘(𝑅‘𝑘)) + 1))
135		fvoveq1 6081	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
136	135	oveq2d 6074	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
137	134, 136	opeq12d 3896	. . . . . . . . . . 11 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
138		oveq1 6065	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
139	138	opeq2d 3895	. . . . . . . . . . 11 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
140	137, 139, 75	ovmpog 6196	. . . . . . . . . 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 1274	. . . . . . . . 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 6651	. . . . . . . . . . 11 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
145	142, 143, 112, 144	syl3anc 1274	. . . . . . . . . 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 5679	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
148		1st2nd2 6382	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ_≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
149	113, 148	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
150	149	fveq2d 5679	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
151		df-ov 6061	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
152	150, 151	eqtr4di 2285	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
153	145, 147, 152	3eqtr2d 2273	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2^nd ‘(𝑅‘𝑘))))
154	45	fveq2d 5679	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩))
155		df-ov 6061	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘𝑢), (2^nd ‘𝑢)⟩)
156	154, 155	eqtr4di 2285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)))
157		fvoveq1 6081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (1^st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘𝑢) + 1)))
158	157	oveq2d 6074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (1^st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))))
159		oveq1 6065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (2^nd ‘𝑢) → (𝑤 + (𝐹‘((1^st ‘𝑢) + 1))) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
160		eqid 2234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
161	158, 159, 160	ovmpog 6196	. . . . . . . . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) = ((2^nd ‘𝑢) + (𝐹‘((1^st ‘𝑢) + 1))))
163	162, 67	eqeltrd 2311	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)) ∈ 𝐶)
164	55, 163	opelxpd 4787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
165		oveq1 6065	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
166	69, 165	opeq12d 3896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
167		oveq2 6066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘𝑢) → ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢)))
168	167	opeq2d 3895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘𝑢) → ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
169		eqid 2234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170	166, 168, 169	ovmpog 6196	. . . . . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((1^st ‘𝑢)(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘𝑢)) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
172	156, 171	eqtrd 2267	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1^st ‘𝑢) + 1), ((1^st ‘𝑢)(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘𝑢))⟩)
173	172, 164	eqeltrd 2311	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
174	173	ralrimiva 2617	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
175	174	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶))
176		frecsuc 6651	. . . . . . . . . . . . . 14 ⊢ ((∀𝑢 ∈ ((ℤ_≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
177	175, 143, 112, 176	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
178	41	fveq1i 5676	. . . . . . . . . . . . 13 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
179	41	fveq1i 5676	. . . . . . . . . . . . . 14 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
180	179	fveq2i 5678	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
181	177, 178, 180	3eqtr4g 2292	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
182	149	fveq2d 5679	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
183	181, 182	eqtrd 2267	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩))
184		df-ov 6061	. . . . . . . . . . 11 ⊢ ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1^st ‘(𝑅‘𝑘)), (2^nd ‘(𝑅‘𝑘))⟩)
185	183, 184	eqtr4di 2285	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))))
186		fvoveq1 6081	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))
187	186	oveq2d 6074	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1^st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
188		oveq1 6065	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (2^nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
189	187, 188, 160	ovmpog 6196	. . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) = ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1))))
191	190, 132	eqeltrd 2311	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))) ∈ 𝐶)
192	120, 191	opelxpd 4787	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ_≥‘𝑀) × 𝐶))
193		oveq1 6065	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
194	134, 193	opeq12d 3896	. . . . . . . . . . . 12 ⊢ (𝑥 = (1^st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
195		oveq2 6066	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘))))
196	195	opeq2d 3895	. . . . . . . . . . . 12 ⊢ (𝑦 = (2^nd ‘(𝑅‘𝑘)) → ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
197	194, 196, 169	ovmpog 6196	. . . . . . . . . . 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 1274	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1^st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2^nd ‘(𝑅‘𝑘))) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((1^st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ_≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2^nd ‘(𝑅‘𝑘)))⟩)
199	190	opeq2d 3895	. . . . . . . . . 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 2271	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1^st ‘(𝑅‘𝑘)) + 1), ((2^nd ‘(𝑅‘𝑘)) + (𝐹‘((1^st ‘(𝑅‘𝑘)) + 1)))⟩)
201	141, 153, 200	3eqtr4rd 2278	. . . . . . . 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 4727	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
205	204	impcom 125	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
206	43, 87, 205	eqfnfvd 5783	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
207	206	rneqd 4991	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ_≥‘𝑀), 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
208	1, 207	eqtr4id 2286	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1398 ∈ wcel 2205 ∀wral 2522 Vcvv 2815 ⊆ wss 3214 ∅c0 3512 ⟨cop 3697 suc csuc 4491 ωcom 4717 × cxp 4752 ran crn 4755 Fn wfn 5352 ⟶wf 5353 ‘cfv 5357 (class class class)co 6058 ∈ cmpo 6060 1^st c1st 6345 2^nd c2nd 6346 freccfrec 6634 1c1 8144 + caddc 8146 ℤcz 9594 ℤ_≥cuz 9871 seqcseq 10833

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-addcom 8243 ax-addass 8245 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-0id 8251 ax-rnegex 8252 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-ltadd 8259

This theorem depends on definitions: df-bi 117 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-frec 6635 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-inn 9255 df-n0 9514 df-z 9595 df-uz 9872 df-seqfrec 10834

This theorem is referenced by: seqf2 10854 seq1cd 10855 seqp1cd 10856

W3C validator