Theorem iseqvalt 9568

Description: Value of the sequence builder function. (Contributed by Jim Kingdon, 27-Apr-2022.)

Hypotheses

Ref	Expression
iseqvalt.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
iseqvalt.r	⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
iseqvalt.f	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
iseqvalt.pl	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
iseqvalt.t	⊢ (𝜑 → 𝑆 ⊆ 𝑇)

Assertion

Ref	Expression
iseqvalt	⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑇) = ran 𝑅)

Distinct variable groups:   𝑤, + ,𝑥,𝑦,𝑧   𝑤,𝐹,𝑥,𝑦,𝑧   𝑤,𝑀,𝑥,𝑦,𝑧   𝑤,𝑅,𝑥,𝑦,𝑧   𝑤,𝑆,𝑥,𝑦,𝑧   𝑥,𝑇,𝑦   𝜑,𝑤,𝑥,𝑦,𝑧

Allowed substitution hints:   𝑇(𝑧,𝑤)

Proof of Theorem iseqvalt

Dummy variables 𝑎 𝑏 𝑘 𝑐 𝑛 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseqvalt.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
2		fveq2 5230	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀))
3	2	eleq1d 2151	. . . . . . 7 ⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑀) ∈ 𝑆))
4		iseqvalt.f	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
5	4	ralrimiva 2439	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆)
6		uzid 8750	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
7	1, 6	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
8	3, 5, 7	rspcdva 2716	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆)
9		iseqvalt.t	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ 𝑇)
10		iseqvalt.pl	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
11	4, 10	iseqovex 9565	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝑆)
12		iseqvalt.r	. . . . . 6 ⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
13	1, 8, 9, 11, 12	frecuzrdgrclt 9533	. . . . 5 ⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆))
14		ffn 5098	. . . . 5 ⊢ (𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆) → 𝑅 Fn ω)
15	13, 14	syl 14	. . . 4 ⊢ (𝜑 → 𝑅 Fn ω)
16		1st2nd2 5853	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
17	16	adantl 271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
18	17	fveq2d 5234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
19		df-ov 5567	. . . . . . . . . 10 ⊢ ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
20	18, 19	syl6eqr 2133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)))
21		xp1st 5844	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆) → (1st ‘𝑢) ∈ (ℤ≥‘𝑀))
22	21	adantl 271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (1st ‘𝑢) ∈ (ℤ≥‘𝑀))
23	9	adantr 270	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → 𝑆 ⊆ 𝑇)
24		xp2nd 5845	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆) → (2nd ‘𝑢) ∈ 𝑆)
25	24	adantl 271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (2nd ‘𝑢) ∈ 𝑆)
26	23, 25	sseldd 3010	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (2nd ‘𝑢) ∈ 𝑇)
27		peano2uz 8788	. . . . . . . . . . . 12 ⊢ ((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀))
28	22, 27	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀))
29	10	caovclg 5705	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆)
30	29	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆)
31		fveq2 5230	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((1st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1st ‘𝑢) + 1)))
32	31	eleq1d 2151	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((1st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝑆))
33	5	adantr 270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆)
34	32, 33, 28	rspcdva 2716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝑆)
35	30, 25, 34	caovcld 5706	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝑆)
36		opelxpi 4423	. . . . . . . . . . 11 ⊢ ((((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀) ∧ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝑆) → ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
37	28, 35, 36	syl2anc 403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
38		oveq1 5571	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑢) → (𝑥 + 1) = ((1st ‘𝑢) + 1))
39	38	fveq2d 5234	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘𝑢) + 1)))
40	39	oveq2d 5580	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘𝑢) + 1))))
41	38, 40	opeq12d 3599	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘𝑢) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1st ‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))⟩)
42		oveq1 5571	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘𝑢) → (𝑦 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
43	42	opeq2d 3598	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘𝑢) → ⟨((1st ‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))⟩ = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
44		eqid 2083	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)
45	41, 43, 44	ovmpt2g 5687	. . . . . . . . . 10 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ 𝑇 ∧ ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
46	22, 26, 37, 45	syl3anc 1170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
47	20, 46	eqtrd 2115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) = ⟨((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))⟩)
48	47, 37	eqeltrd 2159	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
49	48	ralrimiva 2439	. . . . . 6 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
50		opelxpi 4423	. . . . . . 7 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ (𝐹‘𝑀) ∈ 𝑆) → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
51	7, 8, 50	syl2anc 403	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
52	49, 51	jca 300	. . . . 5 ⊢ (𝜑 → (∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)))
53		frecfcl 6075	. . . . 5 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ≥‘𝑀) × 𝑆))
54		ffn 5098	. . . . 5 ⊢ (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩):ω⟶((ℤ≥‘𝑀) × 𝑆) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
55	52, 53, 54	3syl 17	. . . 4 ⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) Fn ω)
56		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅))
57		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = ∅ → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
58	56, 57	eqeq12d 2097	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)))
59	58	imbi2d 228	. . . . . 6 ⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))))
60		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘))
61		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
62	60, 61	eqeq12d 2097	. . . . . . 7 ⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
63	62	imbi2d 228	. . . . . 6 ⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))))
64		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘))
65		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
66	64, 65	eqeq12d 2097	. . . . . . 7 ⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)))
67	66	imbi2d 228	. . . . . 6 ⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
68		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛))
69		fveq2 5230	. . . . . . . 8 ⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
70	68, 69	eqeq12d 2097	. . . . . . 7 ⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
71	70	imbi2d 228	. . . . . 6 ⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))))
72	12	fveq1i 5231	. . . . . . . 8 ⊢ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅)
73		frec0g 6067	. . . . . . . . 9 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
74	51, 73	syl 14	. . . . . . . 8 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
75	72, 74	syl5eq 2127	. . . . . . 7 ⊢ (𝜑 → (𝑅‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
76		frec0g 6067	. . . . . . . 8 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
77	51, 76	syl 14	. . . . . . 7 ⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅) = ⟨𝑀, (𝐹‘𝑀)⟩)
78	75, 77	eqtr4d 2118	. . . . . 6 ⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘∅))
79	13	ad2antlr 473	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆))
80		simpll 496	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑘 ∈ ω)
81	79, 80	ffvelrnd 5356	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆))
82		xp1st 5844	. . . . . . . . . . 11 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀))
83	81, 82	syl 14	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀))
84	9	ad2antlr 473	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → 𝑆 ⊆ 𝑇)
85		xp2nd 5845	. . . . . . . . . . . 12 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆)
86	81, 85	syl 14	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆)
87	84, 86	sseldd 3010	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑇)
88	29	adantll 460	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆)
89	88	adantlr 461	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆)
90		fveq2 5230	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((1st ‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
91	90	eleq1d 2151	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ((1st ‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝑆 ↔ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝑆))
92		fveq2 5230	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
93	92	eleq1d 2151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑎) ∈ 𝑆))
94	93	cbvralv 2582	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 ↔ ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆)
95	5, 94	sylib 120	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆)
96	95	ad2antlr 473	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆)
97		peano2uz 8788	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘𝑀))
98	83, 97	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘𝑀))
99	91, 96, 98	rspcdva 2716	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝑆)
100	89, 86, 99	caovcld 5706	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝑆)
101		oveq1 5571	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝑧 + 1) = ((1st ‘(𝑅‘𝑘)) + 1))
102	101	fveq2d 5234	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
103	102	oveq2d 5580	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
104		oveq1 5571	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (2nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
105		eqid 2083	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))
106	103, 104, 105	ovmpt2g 5687	. . . . . . . . . . . . 13 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ 𝑆 ∧ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝑆) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
107	83, 86, 100, 106	syl3anc 1170	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
108	107	opeq2d 3598	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
109	107, 100	eqeltrd 2159	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝑆)
110		opelxpi 4423	. . . . . . . . . . . 12 ⊢ ((((1st ‘(𝑅‘𝑘)) + 1) ∈ (ℤ≥‘𝑀) ∧ ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
111	98, 109, 110	syl2anc 403	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
112	108, 111	eqeltrrd 2160	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
113		oveq1 5571	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1st ‘(𝑅‘𝑘)) + 1))
114	113	fveq2d 5234	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))
115	114	oveq2d 5580	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
116	113, 115	opeq12d 3599	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
117		oveq1 5571	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))))
118	117	opeq2d 3598	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
119	116, 118, 44	ovmpt2g 5687	. . . . . . . . . 10 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ 𝑇 ∧ ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
120	83, 87, 112, 119	syl3anc 1170	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
121	49	ad2antlr 473	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
122	51	ad2antlr 473	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
123		frecsuc 6077	. . . . . . . . . . . 12 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
124	121, 122, 80, 123	syl3anc 1170	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
125		simpr 108	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
126	125	fveq2d 5234	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
127	124, 126	eqtr4d 2118	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)))
128		1st2nd2 5853	. . . . . . . . . . . . 13 ⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (𝑅‘𝑘) = ⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
129	81, 128	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘𝑘) = ⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
130	129	fveq2d 5234	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
131		df-ov 5567	. . . . . . . . . . 11 ⊢ ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
132	130, 131	syl6eqr 2133	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)‘(𝑅‘𝑘)) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))))
133	127, 132	eqtrd 2115	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩)(2nd ‘(𝑅‘𝑘))))
134	12	fveq1i 5231	. . . . . . . . . . . . . . 15 ⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘)
135	17	fveq2d 5234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
136		df-ov 5567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
137	135, 136	syl6eqr 2133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)))
138		oveq1 5571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (1st ‘𝑢) → (𝑧 + 1) = ((1st ‘𝑢) + 1))
139	138	fveq2d 5234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (1st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘𝑢) + 1)))
140	139	oveq2d 5580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (1st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘𝑢) + 1))))
141		oveq1 5571	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (2nd ‘𝑢) → (𝑤 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
142	140, 141, 105	ovmpt2g 5687	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ 𝑆 ∧ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝑆) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
143	22, 25, 35, 142	syl3anc 1170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))))
144	143, 35	eqeltrd 2159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝑆)
145		opelxpi 4423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((1st ‘𝑢) + 1) ∈ (ℤ≥‘𝑀) ∧ ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝑆) → ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
146	28, 144, 145	syl2anc 403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆))
147		oveq1 5571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (1st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
148	38, 147	opeq12d 3599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (1st ‘𝑢) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
149		oveq2 5572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (2nd ‘𝑢) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)))
150	149	opeq2d 3598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (2nd ‘𝑢) → ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
151		eqid 2083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
152	148, 150, 151	ovmpt2g 5687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘𝑢) ∈ 𝑇 ∧ ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
153	22, 26, 146, 152	syl3anc 1170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘𝑢)) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
154	137, 153	eqtrd 2115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) = ⟨((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))⟩)
155	154, 146	eqeltrd 2159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
156	155	ralrimiva 2439	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
157	156	ad2antlr 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆))
158		frecsuc 6077	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
159	157, 122, 80, 158	syl3anc 1170	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
160	134, 159	syl5eq 2127	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)))
161	12	fveq1i 5231	. . . . . . . . . . . . . . 15 ⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)
162	161	fveq2i 5233	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘))
163	160, 162	syl6eqr 2133	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)))
164	129	fveq2d 5234	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
165	163, 164	eqtrd 2115	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩))
166		df-ov 5567	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)‘⟨(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))⟩)
167	165, 166	syl6eqr 2133	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))))
168		oveq1 5571	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦))
169	113, 168	opeq12d 3599	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)
170		oveq2 5572	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))))
171	170	opeq2d 3598	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩ = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
172	169, 171, 151	ovmpt2g 5687	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd ‘(𝑅‘𝑘)) ∈ 𝑇 ∧ ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩ ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
173	83, 87, 111, 172	syl3anc 1170	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩)(2nd ‘(𝑅‘𝑘))) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
174	167, 173	eqtrd 2115	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))⟩)
175	174, 108	eqtrd 2115	. . . . . . . . 9 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = ⟨((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))⟩)
176	120, 133, 175	3eqtr4rd 2126	. . . . . . . 8 ⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))
177	176	exp31 356	. . . . . . 7 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
178	177	a2d 26	. . . . . 6 ⊢ (𝑘 ∈ ω → ((𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑘)) → (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘suc 𝑘))))
179	59, 63, 67, 71, 78, 178	finds 4370	. . . . 5 ⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛)))
180	179	impcom 123	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)‘𝑛))
181	15, 55, 180	eqfnfvd 5321	. . 3 ⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
182	181	rneqd 4612	. 2 ⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩))
183		df-iseq 9558	. 2 ⊢ seq𝑀( + , 𝐹, 𝑇) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
184	182, 183	syl6reqr 2134	1 ⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑇) = ran 𝑅)

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1285   ∈ wcel 1434  ∀wral 2353   ⊆ wss 2983  ∅c0 3268  ⟨cop 3420  suc csuc 4149  ωcom 4360   × cxp 4390  ran crn 4393   Fn wfn 4948  ⟶wf 4949  ‘cfv 4953  (class class class)co 5564   ↦ cmpt2 5566  1^st c1st 5817  2^nd c2nd 5818  freccfrec 6060  1c1 7080   + caddc 7082  ℤcz 8468  ℤ_≥cuz 8736  seqcseq 9557

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3914  ax-sep 3917  ax-nul 3925  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-iinf 4358  ax-cnex 7165  ax-resscn 7166  ax-1cn 7167  ax-1re 7168  ax-icn 7169  ax-addcl 7170  ax-addrcl 7171  ax-mulcl 7172  ax-addcom 7174  ax-addass 7176  ax-distr 7178  ax-i2m1 7179  ax-0lt1 7180  ax-0id 7182  ax-rnegex 7183  ax-cnre 7185  ax-pre-ltirr 7186  ax-pre-ltwlin 7187  ax-pre-lttrn 7188  ax-pre-ltadd 7190

This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2826  df-csb 2919  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-nul 3269  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-iun 3701  df-br 3807  df-opab 3861  df-mpt 3862  df-tr 3897  df-id 4077  df-iord 4150  df-on 4152  df-ilim 4153  df-suc 4155  df-iom 4361  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-rn 4403  df-res 4404  df-ima 4405  df-iota 4918  df-fun 4955  df-fn 4956  df-f 4957  df-f1 4958  df-fo 4959  df-f1o 4960  df-fv 4961  df-riota 5520  df-ov 5567  df-oprab 5568  df-mpt2 5569  df-1st 5819  df-2nd 5820  df-recs 5975  df-frec 6061  df-pnf 7253  df-mnf 7254  df-xr 7255  df-ltxr 7256  df-le 7257  df-sub 7384  df-neg 7385  df-inn 8143  df-n0 8392  df-z 8469  df-uz 8737  df-iseq 9558

This theorem is referenced by:  iseq1t  9570  iseqfclt  9572  iseqp1t  9575