sdclem2 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sdclem2		Structured version Visualization version GIF version

Theorem sdclem2 38644

Description: Lemma for sdc 38646. (Contributed by Jeff Madsen, 2-Sep-2009.)

**Hypotheses**
Ref	Expression
sdc.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
sdc.2	⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒))
sdc.3	⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏))
sdc.4	⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃))
sdc.5	⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎))
sdc.6	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sdc.7	⊢ (𝜑 → 𝑀 ∈ ℤ)
sdc.8	⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏))
sdc.9	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
sdc.10	⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}
sdc.11	⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
sdc.12	⊢ Ⅎ𝑘𝜑
sdc.13	⊢ (𝜑 → 𝐺:𝑍⟶𝐽)
sdc.14	⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴)
sdc.15	⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤)))

**Assertion**
Ref	Expression
sdclem2	⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))

Distinct variable groups: 𝑓,𝑔,ℎ,𝑘,𝑛,𝑤,𝑥,𝐴 ℎ,𝐽,𝑘,𝑤,𝑥 𝑓,𝑀,𝑔,ℎ,𝑘,𝑛,𝑤,𝑥 𝜒,𝑔 𝑛,𝐹,𝑤,𝑥 𝜓,𝑓,ℎ,𝑘,𝑥 𝜎,𝑓,𝑔,𝑛,𝑥 𝑓,𝐺,𝑔,ℎ,𝑘,𝑛,𝑤,𝑥 𝜑,𝑛,𝑤,𝑥 𝜃,𝑛,𝑤,𝑥 ℎ,𝑉 𝜏,ℎ,𝑘,𝑛,𝑤,𝑥 𝑓,𝑍,𝑔,ℎ,𝑘,𝑛,𝑤,𝑥 Allowed substitution hints: 𝜑(𝑓, 𝑔, ℎ, 𝑘) 𝜓(𝑤, 𝑔, 𝑛) 𝜒(𝑥, 𝑤, 𝑓, ℎ, 𝑘, 𝑛) 𝜃(𝑓, 𝑔, ℎ, 𝑘) 𝜏(𝑓, 𝑔) 𝜎(𝑤, ℎ, 𝑘) 𝐹(𝑓, 𝑔, ℎ, 𝑘) 𝐽(𝑓, 𝑔, 𝑛) 𝑉(𝑥, 𝑤, 𝑓, 𝑔, 𝑘, 𝑛)

Proof of Theorem sdclem2 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sdc.12	. . 3 ⊢ Ⅎ𝑘𝜑
2		sdc.13	. . . . . . . 8 ⊢ (𝜑 → 𝐺:𝑍⟶𝐽)
3	2	ffvelcdmda 7076	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐽)
4		sdc.10	. . . . . . . . 9 ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}
5	4	eleq2i 2853	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ (𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)})
6		nfcv 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑔𝑍
7		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(𝐺‘𝑘):(𝑀...𝑛)⟶𝐴
8		nfsbc1v 3759	. . . . . . . . . . 11 ⊢ Ⅎ𝑔[(𝐺‘𝑘) / 𝑔]𝜓
9	7, 8	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑔((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
10	6, 9	nfrexw 3311	. . . . . . . . 9 ⊢ Ⅎ𝑔∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
11		fvex 6890	. . . . . . . . 9 ⊢ (𝐺‘𝑘) ∈ V
12		feq1 6679	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑛)⟶𝐴))
13		sbceq1a 3750	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜓))
14	12, 13	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = (𝐺‘𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
15	14	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑔 = (𝐺‘𝑘) → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
16	10, 11, 15	elabf 3629	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
17	5, 16	bitri 278	. . . . . . 7 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
18	3, 17	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
19		fdm 6711	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺‘𝑘) = (𝑀...𝑛))
20	19	adantr 486	. . . . . . . . 9 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → dom (𝐺‘𝑘) = (𝑀...𝑛))
21		fveq2 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀))
22		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
23	22	mpteq1d 5195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
24	21, 23	eqeq12d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
25	24	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))))
26		fveq2 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
27		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
28	27	mpteq1d 5195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
29	26, 28	eqeq12d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
30	29	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))))
31		fveq2 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑤 + 1)))
32		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
33	32	mpteq1d 5195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
34	31, 33	eqeq12d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
35	34	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
36		fveq2 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘))
37		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
38	37	mpteq1d 5195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
39	36, 38	eqeq12d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
40	39	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑘 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))))
41		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
42		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
43	41, 42	fveq12d 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑘 → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘𝑘)‘𝑘))
44		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))
45		fvex 6890	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘)‘𝑘) ∈ V
46	43, 44, 45	fvmpt 6985	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
47	46	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
48		elfz1eq 13648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
49	48	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
50	49	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑀))
51	50	fveq1d 6879	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑘)‘𝑘) = ((𝐺‘𝑀)‘𝑘))
52	47, 51	eqtr2d 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
53	52	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
54	1, 53	ralrimi 3261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
55		sdc.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴)
56	55	ffnd 6702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺‘𝑀) Fn (𝑀...𝑀))
57		fvex 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑚)‘𝑚) ∈ V
58	57, 44	fnmpti 6674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)
59		eqfnfv 7021	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
60	56, 58, 59	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
61	54, 60	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
62	61	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℤ → (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
63		sdc.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑍 = (ℤ_≥‘𝑀)
64	63	eleq2i 2853	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 ↔ 𝑤 ∈ (ℤ_≥‘𝑀))
65	2	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘𝑤) ∈ 𝐽)
66		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
67		3simpa 1166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
68	67	reximi 3101	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
69	68	ss2abi 4014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}
70	63	fvexi 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑍 ∈ V
71		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑘 𝑤 ∈ 𝑍
72	1, 71	nfan 1932	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑤 ∈ 𝑍)
73		sdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
74	73	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝐴 ∈ 𝑉)
75		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ:(𝑀...(𝑘 + 1))⟶𝐴)
76		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...(𝑘 + 1)) ∈ V
77		elmapg 8843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
78	76, 77	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐴 ∈ 𝑉 → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
79	75, 78	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐴 ∈ 𝑉 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1)))))
80	79	abssdv 4015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
81	74, 80	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
82		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V
83		ssexg 5281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (({ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∧ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
84	81, 82, 83	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
85	84	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V))
86	72, 85	ralrimi 3261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
87		abrexex2g 7965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑍 ∈ V ∧ ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
88	70, 86, 87	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
89		ssexg 5281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
90	69, 88, 89	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑥 = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
92	91	3anbi2d 1469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝐺‘𝑤) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
93	92	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝐺‘𝑤) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
94	93	abbidv 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
95	94	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺‘𝑤)))
97	96, 94	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))
98	95, 97	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐺‘𝑤) → (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
99	98	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100		sdc.11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
101	100	ovmpt4g 7559	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
102	101	3com12 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
103	102	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
104	99, 103	vtoclga 3537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
105	65, 66, 90, 104	syl3c 67	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
106	105, 69	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
107		sdc.15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤)))
108	106, 107	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
109		fvex 6890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑤 + 1)) ∈ V
110		feq1 6679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111		reseq1 5964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112	111	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113	110, 112	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114	113	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115	109, 114	elab 3633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116	108, 115	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117		nfv 1947	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
118		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119		fzssp1 13681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120		fssres 6740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121	118, 119, 120	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122	121	fdmd 6712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
124	57, 123	fnmpti 6674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)
125		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
126	125	fneq1d 6624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127	124, 126	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128	127	fndmd 6636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129	122, 128	eqtr3d 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
130		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ 𝑍)
131	130, 63	eleqtrdi 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ_≥‘𝑀))
132		fzopth 13675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
133	131, 132	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
134	129, 133	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀 = 𝑀 ∧ 𝑘 = 𝑤))
135	134	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 = 𝑤)
136	135	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
137	136	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
138		elfzp1 13688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
139	131, 138	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140	129	reseq2d 5970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
141		fzssp1 13681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
142		resmpt 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
144	140, 143	eqtr2di 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
145	125, 144	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146	145	fveq1d 6879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
147		fvres 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
148		fvres 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
149	147, 148	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
150	146, 149	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
151	136	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
152	135, 131	eqeltrrd 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ_≥‘𝑀))
153		peano2uz 13009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (ℤ_≥‘𝑀))
154		eluzfz2 13645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
155		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → (𝐺‘𝑚) = (𝐺‘(𝑤 + 1)))
156		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
157	155, 156	fveq12d 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = (𝑤 + 1) → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
158		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))
159		fvex 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
160	157, 158, 159	fvmpt 6985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
161	152, 153, 154, 160	4syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162	161	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
163		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
164		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
165	163, 164	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1))))
166	162, 165	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
167	151, 166	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
168	150, 167	jaod 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
169	139, 168	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
170	169	ralrimiv 3154	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
171		ffn 6701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
172	171	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
173	57, 158	fnmpti 6674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
174		eqfnfv2 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
175	172, 173, 174	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
176	137, 170, 175	mpbir2and 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
177	176	expr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
178		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
179	178	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
180	177, 179	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
181	180	expimpd 459	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
182	181	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))))
183	72, 117, 182	rexlimd 3270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
184	116, 183	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
185	184	expcom 419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
186	64, 185	sylbir 238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
187	186	a2d 30	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → ((𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
188	25, 30, 35, 40, 62, 187	uzind4 13014	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
189	188, 63	eleq2s 2879	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑍 → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
190	189	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
191	190	dmeqd 5887	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
192		dmmptg 6236	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ (𝑀...𝑘)((𝐺‘𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘))
193	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝑀...𝑘) → ((𝐺‘𝑚)‘𝑚) ∈ V)
194	192, 193	mprg 3083	. . . . . . . . . . . . 13 ⊢ dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘)
195	191, 194	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = (𝑀...𝑘))
196	195	eqeq1d 2763	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
197		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍)
198	197, 63	eleqtrdi 2871	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ_≥‘𝑀))
199		fzopth 13675	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
200	198, 199	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
201	196, 200	bitrd 282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
202		simpr 490	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑀 ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
203	201, 202	biimtrdi 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
204	20, 203	syl5 35	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
205		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
206	205	feq2d 6685	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴))
207		sdc.4	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃))
208	207	sbcbidv 3794	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ([(𝐺‘𝑘) / 𝑔]𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜃))
209	206, 208	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
210	209	equcoms 2053	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
211	210	biimpcd 252	. . . . . . . 8 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
212	204, 211	sylcom 31	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
213	212	rexlimdvw 3169	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
214	18, 213	mpd 16	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))
215	214	simpld 500	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴)
216		eluzfz2 13645	. . . . 5 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘))
217	198, 216	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘))
218	215, 217	ffvelcdmd 7077	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)‘𝑘) ∈ 𝐴)
219	43	cbvmptv 5209	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑘 ∈ 𝑍 ↦ ((𝐺‘𝑘)‘𝑘))
220	1, 218, 219	fmptdf 7109	. 2 ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴)
221	214	simprd 501	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝐺‘𝑘) / 𝑔]𝜃)
222	190, 221	sbceq1dd 3745	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
223	222	ex 418	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝑍 → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
224	1, 223	ralrimi 3261	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
225		mpteq1 5194	. . . . . 6 ⊢ ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
226		dfsbcq 3741	. . . . . 6 ⊢ ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
227	205, 225, 226	3syl 19	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
228	207	sbcbidv 3794	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
229	227, 228	bitrd 282	. . . 4 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
230	229	cbvralvw 3241	. . 3 ⊢ (∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
231	224, 230	sylibr 237	. 2 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)
232	70	mptex 7221	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ∈ V
233		feq1 6679	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓:𝑍⟶𝐴 ↔ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴))
234		vex 3455	. . . . . . . 8 ⊢ 𝑓 ∈ V
235	234	resex 6020	. . . . . . 7 ⊢ (𝑓 ↾ (𝑀...𝑛)) ∈ V
236		sdc.2	. . . . . . 7 ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒))
237	235, 236	sbcie 3780	. . . . . 6 ⊢ ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ 𝜒)
238		reseq1 5964	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
239		fzssuz 13679	. . . . . . . . . 10 ⊢ (𝑀...𝑛) ⊆ (ℤ_≥‘𝑀)
240	239, 63	sseqtrri 3980	. . . . . . . . 9 ⊢ (𝑀...𝑛) ⊆ 𝑍
241		resmpt 6031	. . . . . . . . 9 ⊢ ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
242	240, 241	ax-mp 5	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))
243	238, 242	eqtrdi 2812	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
244	243	sbceq1d 3744	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
245	237, 244	bitr3id 288	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝜒 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
246	245	ralbidv 3186	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (∀𝑛 ∈ 𝑍 𝜒 ↔ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
247	233, 246	anbi12d 644	. . 3 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ((𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒) ↔ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)))
248	232, 247	spcev 3561	. 2 ⊢ (((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))
249	220, 231, 248	syl2anc 596	1 ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∃wex 1812 Ⅎwnf 1816 ∈ wcel 2145 {cab 2739 ∀wral 3077 ∃wrex 3087 Vcvv 3451 [wsbc 3739 ⊆ wss 3899 {csn 4584 ↦ cmpt 5186 dom cdm 5651 ↾ cres 5653 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ∈ cmpo 7414 ↑_m cmap 8831 1c1 11182 + caddc 11184 ℤcz 12674 ℤ_≥cuz 12946 ...cfz 13620

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-n0 12588 df-z 12675 df-uz 12947 df-fz 13621

This theorem is used by: sdclem1 38645

W3C validator