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 35900

Description: Lemma for sdc 35902. (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 6961	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐽)
4		sdc.10	. . . . . . . . 9 ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}
5	4	eleq2i 2830	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ (𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)})
6		nfcv 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑔𝑍
7		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(𝐺‘𝑘):(𝑀...𝑛)⟶𝐴
8		nfsbc1v 3736	. . . . . . . . . . 11 ⊢ Ⅎ𝑔[(𝐺‘𝑘) / 𝑔]𝜓
9	7, 8	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑔((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
10	6, 9	nfrex 3242	. . . . . . . . 9 ⊢ Ⅎ𝑔∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
11		fvex 6787	. . . . . . . . 9 ⊢ (𝐺‘𝑘) ∈ V
12		feq1 6581	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑛)⟶𝐴))
13		sbceq1a 3727	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜓))
14	12, 13	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑔 = (𝐺‘𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
15	14	rexbidv 3226	. . . . . . . . 9 ⊢ (𝑔 = (𝐺‘𝑘) → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
16	10, 11, 15	elabf 3606	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
17	5, 16	bitri 274	. . . . . . 7 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
18	3, 17	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
19		fdm 6609	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺‘𝑘) = (𝑀...𝑛))
20	19	adantr 481	. . . . . . . . 9 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → dom (𝐺‘𝑘) = (𝑀...𝑛))
21		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀))
22		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
23	22	mpteq1d 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
24	21, 23	eqeq12d 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
25	24	imbi2d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))))
26		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
27		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
28	27	mpteq1d 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
29	26, 28	eqeq12d 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
30	29	imbi2d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))))
31		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑤 + 1)))
32		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
33	32	mpteq1d 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
34	31, 33	eqeq12d 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
35	34	imbi2d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
36		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘))
37		oveq2 7283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
38	37	mpteq1d 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
39	36, 38	eqeq12d 2754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
40	39	imbi2d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑘 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))))
41		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
42		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
43	41, 42	fveq12d 6781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑘 → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘𝑘)‘𝑘))
44		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))
45		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘)‘𝑘) ∈ V
46	43, 44, 45	fvmpt 6875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
47	46	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
48		elfz1eq 13267	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
49	48	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
50	49	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑀))
51	50	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑘)‘𝑘) = ((𝐺‘𝑀)‘𝑘))
52	47, 51	eqtr2d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
53	52	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
54	1, 53	ralrimi 3141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
55		sdc.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴)
56	55	ffnd 6601	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺‘𝑀) Fn (𝑀...𝑀))
57		fvex 6787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑚)‘𝑚) ∈ V
58	57, 44	fnmpti 6576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)
59		eqfnfv 6909	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
60	56, 58, 59	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
61	54, 60	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
62	61	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℤ → (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
63		sdc.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑍 = (ℤ_≥‘𝑀)
64	63	eleq2i 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 ↔ 𝑤 ∈ (ℤ_≥‘𝑀))
65	2	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘𝑤) ∈ 𝐽)
66		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
67		3simpa 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
68	67	reximi 3178	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
69	68	ss2abi 4000	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}
70	63	fvexi 6788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑍 ∈ V
71		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑘 𝑤 ∈ 𝑍
72	1, 71	nfan 1902	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑤 ∈ 𝑍)
73		sdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
74	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝐴 ∈ 𝑉)
75		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ:(𝑀...(𝑘 + 1))⟶𝐴)
76		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...(𝑘 + 1)) ∈ V
77		elmapg 8628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
78	76, 77	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐴 ∈ 𝑉 → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
79	75, 78	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐴 ∈ 𝑉 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1)))))
80	79	abssdv 4002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
81	74, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
82		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V
83		ssexg 5247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (({ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∧ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
84	81, 82, 83	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
85	84	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V))
86	72, 85	ralrimi 3141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
87		abrexex2g 7807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑍 ∈ V ∧ ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
88	70, 86, 87	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
89		ssexg 5247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
90	69, 88, 89	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑥 = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
92	91	3anbi2d 1440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝐺‘𝑤) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
93	92	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝐺‘𝑤) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
94	93	abbidv 2807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
95	94	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺‘𝑤)))
97	96, 94	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))
98	95, 97	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐺‘𝑤) → (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
99	98	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100		sdc.11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
101	100	ovmpt4g 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
102	101	3com12 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
103	102	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
104	99, 103	vtoclga 3513	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
105	65, 66, 90, 104	syl3c 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
106	105, 69	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
107		sdc.15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤)))
108	106, 107	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
109		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑤 + 1)) ∈ V
110		feq1 6581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111		reseq1 5885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112	111	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113	110, 112	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114	113	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115	109, 114	elab 3609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116	108, 115	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117		nfv 1917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
118		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119		fzssp1 13299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120		fssres 6640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121	118, 119, 120	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122	121	fdmd 6611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
124	57, 123	fnmpti 6576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)
125		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
126	125	fneq1d 6526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127	124, 126	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128	127	fndmd 6538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129	122, 128	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
130		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ 𝑍)
131	130, 63	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ_≥‘𝑀))
132		fzopth 13293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)))
134	129, 133	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀 = 𝑀 ∧ 𝑘 = 𝑤))
135	134	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 = 𝑤)
136	135	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
137	136	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
138		elfzp1 13306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
139	131, 138	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140	129	reseq2d 5891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
141		fzssp1 13299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
142		resmpt 5945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
144	140, 143	eqtr2di 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
145	125, 144	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146	145	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
147		fvres 6793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
148		fvres 6793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
149	147, 148	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
150	146, 149	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
151	136	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
152	135, 131	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ_≥‘𝑀))
153		peano2uz 12641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (ℤ_≥‘𝑀))
154		eluzfz2 13264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
155		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → (𝐺‘𝑚) = (𝐺‘(𝑤 + 1)))
156		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
157	155, 156	fveq12d 6781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = (𝑤 + 1) → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
158		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))
159		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
160	157, 158, 159	fvmpt 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
161	152, 153, 154, 160	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162	161	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
163		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
164		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
165	163, 164	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1))))
166	162, 165	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
167	151, 166	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
168	150, 167	jaod 856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
169	139, 168	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
170	169	ralrimiv 3102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
171		ffn 6600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
172	171	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
173	57, 158	fnmpti 6576	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
174		eqfnfv2 6910	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
175	172, 173, 174	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))))
176	137, 170, 175	mpbir2and 710	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
177	176	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
178		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
179	178	imbi1d 342	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
180	177, 179	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
181	180	expimpd 454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
182	181	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))))
183	72, 117, 182	rexlimd 3250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
184	116, 183	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
185	184	expcom 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
186	64, 185	sylbir 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
187	186	a2d 29	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → ((𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
188	25, 30, 35, 40, 62, 187	uzind4 12646	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
189	188, 63	eleq2s 2857	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑍 → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
190	189	impcom 408	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
191	190	dmeqd 5814	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
192		dmmptg 6145	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ (𝑀...𝑘)((𝐺‘𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘))
193	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝑀...𝑘) → ((𝐺‘𝑚)‘𝑚) ∈ V)
194	192, 193	mprg 3078	. . . . . . . . . . . . 13 ⊢ dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘)
195	191, 194	eqtrdi 2794	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = (𝑀...𝑘))
196	195	eqeq1d 2740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
197		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍)
198	197, 63	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ_≥‘𝑀))
199		fzopth 13293	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
200	198, 199	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
201	196, 200	bitrd 278	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛)))
202		simpr 485	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑀 ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
203	201, 202	syl6bi 252	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
204	20, 203	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
205		oveq2 7283	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
206	205	feq2d 6586	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴))
207		sdc.4	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃))
208	207	sbcbidv 3775	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ([(𝐺‘𝑘) / 𝑔]𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜃))
209	206, 208	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
210	209	equcoms 2023	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
211	210	biimpcd 248	. . . . . . . 8 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
212	204, 211	sylcom 30	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
213	212	rexlimdvw 3219	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
214	18, 213	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))
215	214	simpld 495	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴)
216		eluzfz2 13264	. . . . 5 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘))
217	198, 216	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘))
218	215, 217	ffvelrnd 6962	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)‘𝑘) ∈ 𝐴)
219	43	cbvmptv 5187	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑘 ∈ 𝑍 ↦ ((𝐺‘𝑘)‘𝑘))
220	1, 218, 219	fmptdf 6991	. 2 ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴)
221	214	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝐺‘𝑘) / 𝑔]𝜃)
222	190, 221	sbceq1dd 3722	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
223	222	ex 413	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝑍 → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
224	1, 223	ralrimi 3141	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
225		mpteq1 5167	. . . . . 6 ⊢ ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
226		dfsbcq 3718	. . . . . 6 ⊢ ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
227	205, 225, 226	3syl 18	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
228	207	sbcbidv 3775	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
229	227, 228	bitrd 278	. . . 4 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
230	229	cbvralvw 3383	. . 3 ⊢ (∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
231	224, 230	sylibr 233	. 2 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)
232	70	mptex 7099	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ∈ V
233		feq1 6581	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓:𝑍⟶𝐴 ↔ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴))
234		vex 3436	. . . . . . . 8 ⊢ 𝑓 ∈ V
235	234	resex 5939	. . . . . . 7 ⊢ (𝑓 ↾ (𝑀...𝑛)) ∈ V
236		sdc.2	. . . . . . 7 ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒))
237	235, 236	sbcie 3759	. . . . . 6 ⊢ ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ 𝜒)
238		reseq1 5885	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
239		fzssuz 13297	. . . . . . . . . 10 ⊢ (𝑀...𝑛) ⊆ (ℤ_≥‘𝑀)
240	239, 63	sseqtrri 3958	. . . . . . . . 9 ⊢ (𝑀...𝑛) ⊆ 𝑍
241		resmpt 5945	. . . . . . . . 9 ⊢ ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
242	240, 241	ax-mp 5	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))
243	238, 242	eqtrdi 2794	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
244	243	sbceq1d 3721	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
245	237, 244	bitr3id 285	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝜒 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
246	245	ralbidv 3112	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (∀𝑛 ∈ 𝑍 𝜒 ↔ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
247	233, 246	anbi12d 631	. . 3 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ((𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒) ↔ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)))
248	232, 247	spcev 3545	. 2 ⊢ (((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))
249	220, 231, 248	syl2anc 584	1 ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2106 {cab 2715 ∀wral 3064 ∃wrex 3065 Vcvv 3432 [wsbc 3716 ⊆ wss 3887 {csn 4561 ↦ cmpt 5157 dom cdm 5589 ↾ cres 5591 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ∈ cmpo 7277 ↑_m cmap 8615 1c1 10872 + caddc 10874 ℤcz 12319 ℤ_≥cuz 12582 ...cfz 13239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-fz 13240

This theorem is referenced by: sdclem1 35901

W3C validator