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 35011

Description: Lemma for sdc 35013. (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	ffvelrnda 6845	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐽)
4		sdc.10	. . . . . . . . 9 ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}
5	4	eleq2i 2904	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ (𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)})
6		nfcv 2977	. . . . . . . . . 10 ⊢ Ⅎ𝑔𝑍
7		nfv 1911	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(𝐺‘𝑘):(𝑀...𝑛)⟶𝐴
8		nfsbc1v 3791	. . . . . . . . . . 11 ⊢ Ⅎ𝑔[(𝐺‘𝑘) / 𝑔]𝜓
9	7, 8	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑔((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
10	6, 9	nfrex 3309	. . . . . . . . 9 ⊢ Ⅎ𝑔∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
11		fvex 6677	. . . . . . . . 9 ⊢ (𝐺‘𝑘) ∈ V
12		feq1 6489	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑛)⟶𝐴))
13		sbceq1a 3782	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜓))
14	12, 13	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = (𝐺‘𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
15	14	rexbidv 3297	. . . . . . . . 9 ⊢ (𝑔 = (𝐺‘𝑘) → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
16	10, 11, 15	elabf 3664	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
17	5, 16	bitri 277	. . . . . . 7 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
18	3, 17	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
19		fdm 6516	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺‘𝑘) = (𝑀...𝑛))
20	19	adantr 483	. . . . . . . . 9 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → dom (𝐺‘𝑘) = (𝑀...𝑛))
21		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀))
22		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
23	22	mpteq1d 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
24	21, 23	eqeq12d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
25	24	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))))
26		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
27		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
28	27	mpteq1d 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
29	26, 28	eqeq12d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
30	29	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))))
31		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑤 + 1)))
32		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
33	32	mpteq1d 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
34	31, 33	eqeq12d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
35	34	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
36		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘))
37		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
38	37	mpteq1d 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
39	36, 38	eqeq12d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
40	39	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑘 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))))
41		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
42		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
43	41, 42	fveq12d 6671	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑘 → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘𝑘)‘𝑘))
44		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))
45		fvex 6677	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘)‘𝑘) ∈ V
46	43, 44, 45	fvmpt 6762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
47	46	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
48		elfz1eq 12912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
49	48	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
50	49	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑀))
51	50	fveq1d 6666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑘)‘𝑘) = ((𝐺‘𝑀)‘𝑘))
52	47, 51	eqtr2d 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
53	52	ex 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
54	1, 53	ralrimi 3216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
55		sdc.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴)
56	55	ffnd 6509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺‘𝑀) Fn (𝑀...𝑀))
57		fvex 6677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑚)‘𝑚) ∈ V
58	57, 44	fnmpti 6485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)
59		eqfnfv 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
60	56, 58, 59	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
61	54, 60	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
62	61	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℤ → (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
63		sdc.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑍 = (ℤ_≥‘𝑀)
64	63	eleq2i 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 ↔ 𝑤 ∈ (ℤ_≥‘𝑀))
65	2	ffvelrnda 6845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘𝑤) ∈ 𝐽)
66		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
67		3simpa 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
68	67	reximi 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
69	68	ss2abi 4042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}
70	63	fvexi 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑍 ∈ V
71		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑘 𝑤 ∈ 𝑍
72	1, 71	nfan 1896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑤 ∈ 𝑍)
73		sdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
74	73	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝐴 ∈ 𝑉)
75		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ:(𝑀...(𝑘 + 1))⟶𝐴)
76		ovex 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...(𝑘 + 1)) ∈ V
77		elmapg 8413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
78	76, 77	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐴 ∈ 𝑉 → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
79	75, 78	syl5ibr 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐴 ∈ 𝑉 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1)))))
80	79	abssdv 4044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
81	74, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
82		ovex 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V
83		ssexg 5219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (({ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∧ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
84	81, 82, 83	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
85	84	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V))
86	72, 85	ralrimi 3216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
87		abrexex2g 7659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑍 ∈ V ∧ ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
88	70, 86, 87	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
89		ssexg 5219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
90	69, 88, 89	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91		eqeq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑥 = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
92	91	3anbi2d 1437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝐺‘𝑤) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
93	92	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝐺‘𝑤) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
94	93	abbidv 2885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
95	94	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺‘𝑤)))
97	96, 94	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
102	101	3com12 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
103	102	3exp 1115	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
104	99, 103	vtoclga 3573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
105	65, 66, 90, 104	syl3c 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
106	105, 69	eqsstrdi 4020	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
107		sdc.15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤)))
108	106, 107	sseldd 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
109		fvex 6677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑤 + 1)) ∈ V
110		feq1 6489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111		reseq1 5841	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112	111	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113	110, 112	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114	113	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115	109, 114	elab 3666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116	108, 115	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117		nfv 1911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
118		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119		fzssp1 12944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120		fssres 6538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121	118, 119, 120	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122	121	fdmd 6517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
124	57, 123	fnmpti 6485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)
125		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
126	125	fneq1d 6440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127	124, 126	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128		fndm 6449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
130	122, 129	eqtr3d 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
131		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ 𝑍)
132	131, 63	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ_≥‘𝑀))
133		fzopth 12938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
135	130, 134	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀 = 𝑀 ∧ 𝑘 = 𝑤))
136	135	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 = 𝑤)
137	136	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
138	137	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
139		elfzp1 12951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140	132, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
141	130	reseq2d 5847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
142		fzssp1 12944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
143		resmpt 5899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
144	142, 143	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
145	141, 144	syl6req 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146	125, 145	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
147	146	fveq1d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
148		fvres 6683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
149		fvres 6683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
150	148, 149	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
151	147, 150	syl5ibcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
152	137	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
153	136, 132	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ_≥‘𝑀))
154		peano2uz 12295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (ℤ_≥‘𝑀))
155		eluzfz2 12909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
156		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → (𝐺‘𝑚) = (𝐺‘(𝑤 + 1)))
157		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
158	156, 157	fveq12d 6671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = (𝑤 + 1) → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
159		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))
160		fvex 6677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
161	158, 159, 160	fvmpt 6762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162	153, 154, 155, 161	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
163	162	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
164		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
165		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
166	164, 165	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1))))
167	163, 166	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
168	152, 167	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
169	151, 168	jaod 855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
170	140, 169	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
171	170	ralrimiv 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
172		ffn 6508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
173	172	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
174	57, 159	fnmpti 6485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
175		eqfnfv2 6797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
176	173, 174, 175	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
177	138, 171, 176	mpbir2and 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
178	177	expr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
179		eqeq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
180	179	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
181	178, 180	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
182	181	expimpd 456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
183	182	ex 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))))
184	72, 117, 183	rexlimd 3317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
185	116, 184	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
186	185	expcom 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
187	64, 186	sylbir 237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
188	187	a2d 29	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → ((𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
189	25, 30, 35, 40, 62, 188	uzind4 12300	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
190	189, 63	eleq2s 2931	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑍 → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
191	190	impcom 410	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
192	191	dmeqd 5768	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
193		dmmptg 6090	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ (𝑀...𝑘)((𝐺‘𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘))
194	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝑀...𝑘) → ((𝐺‘𝑚)‘𝑚) ∈ V)
195	193, 194	mprg 3152	. . . . . . . . . . . . 13 ⊢ dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘)
196	192, 195	syl6eq 2872	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = (𝑀...𝑘))
197	196	eqeq1d 2823	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
198		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍)
199	198, 63	eleqtrdi 2923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ_≥‘𝑀))
200		fzopth 12938	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
201	199, 200	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
202	197, 201	bitrd 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
203		simpr 487	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑀 ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
204	202, 203	syl6bi 255	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
205	20, 204	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
206		oveq2 7158	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
207	206	feq2d 6494	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴))
208		sdc.4	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃))
209	208	sbcbidv 3826	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ([(𝐺‘𝑘) / 𝑔]𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜃))
210	207, 209	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
211	210	equcoms 2023	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
212	211	biimpcd 251	. . . . . . . 8 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
213	205, 212	sylcom 30	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
214	213	rexlimdvw 3290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
215	18, 214	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))
216	215	simpld 497	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴)
217		eluzfz2 12909	. . . . 5 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘))
218	199, 217	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘))
219	216, 218	ffvelrnd 6846	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)‘𝑘) ∈ 𝐴)
220	43	cbvmptv 5161	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑘 ∈ 𝑍 ↦ ((𝐺‘𝑘)‘𝑘))
221	1, 219, 220	fmptdf 6875	. 2 ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴)
222	215	simprd 498	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝐺‘𝑘) / 𝑔]𝜃)
223	191, 222	sbceq1dd 3777	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
224	223	ex 415	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝑍 → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
225	1, 224	ralrimi 3216	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
226		mpteq1 5146	. . . . . 6 ⊢ ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
227		dfsbcq 3773	. . . . . 6 ⊢ ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
228	206, 226, 227	3syl 18	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
229	208	sbcbidv 3826	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
230	228, 229	bitrd 281	. . . 4 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
231	230	cbvralvw 3449	. . 3 ⊢ (∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
232	225, 231	sylibr 236	. 2 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)
233	70	mptex 6980	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ∈ V
234		feq1 6489	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓:𝑍⟶𝐴 ↔ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴))
235		vex 3497	. . . . . . . 8 ⊢ 𝑓 ∈ V
236	235	resex 5893	. . . . . . 7 ⊢ (𝑓 ↾ (𝑀...𝑛)) ∈ V
237		sdc.2	. . . . . . 7 ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒))
238	236, 237	sbcie 3811	. . . . . 6 ⊢ ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ 𝜒)
239		reseq1 5841	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
240		fzssuz 12942	. . . . . . . . . 10 ⊢ (𝑀...𝑛) ⊆ (ℤ_≥‘𝑀)
241	240, 63	sseqtrri 4003	. . . . . . . . 9 ⊢ (𝑀...𝑛) ⊆ 𝑍
242		resmpt 5899	. . . . . . . . 9 ⊢ ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
243	241, 242	ax-mp 5	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))
244	239, 243	syl6eq 2872	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
245	244	sbceq1d 3776	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
246	238, 245	syl5bbr 287	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝜒 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
247	246	ralbidv 3197	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (∀𝑛 ∈ 𝑍 𝜒 ↔ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
248	234, 247	anbi12d 632	. . 3 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ((𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒) ↔ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)))
249	233, 248	spcev 3606	. 2 ⊢ (((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))
250	221, 232, 249	syl2anc 586	1 ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∃wex 1776 Ⅎwnf 1780 ∈ wcel 2110 {cab 2799 ∀wral 3138 ∃wrex 3139 Vcvv 3494 [wsbc 3771 ⊆ wss 3935 {csn 4560 ↦ cmpt 5138 dom cdm 5549 ↾ cres 5551 Fn wfn 6344 ⟶wf 6345 ‘cfv 6349 (class class class)co 7150 ∈ cmpo 7152 ↑_m cmap 8400 1c1 10532 + caddc 10534 ℤcz 11975 ℤ_≥cuz 12237 ...cfz 12886

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-n0 11892 df-z 11976 df-uz 12238 df-fz 12887

This theorem is referenced by: sdclem1 35012

W3C validator