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 36598

Description: Lemma for sdc 36600. (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 7083	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐽)
4		sdc.10	. . . . . . . . 9 ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}
5	4	eleq2i 2825	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ (𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)})
6		nfcv 2903	. . . . . . . . . 10 ⊢ Ⅎ𝑔𝑍
7		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑔(𝐺‘𝑘):(𝑀...𝑛)⟶𝐴
8		nfsbc1v 3796	. . . . . . . . . . 11 ⊢ Ⅎ𝑔[(𝐺‘𝑘) / 𝑔]𝜓
9	7, 8	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑔((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
10	6, 9	nfrexw 3310	. . . . . . . . 9 ⊢ Ⅎ𝑔∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)
11		fvex 6901	. . . . . . . . 9 ⊢ (𝐺‘𝑘) ∈ V
12		feq1 6695	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑛)⟶𝐴))
13		sbceq1a 3787	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐺‘𝑘) → (𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜓))
14	12, 13	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑔 = (𝐺‘𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
15	14	rexbidv 3178	. . . . . . . . 9 ⊢ (𝑔 = (𝐺‘𝑘) → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)))
16	10, 11, 15	elabf 3664	. . . . . . . 8 ⊢ ((𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
17	5, 16	bitri 274	. . . . . . 7 ⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
18	3, 17	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))
19		fdm 6723	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺‘𝑘) = (𝑀...𝑛))
20	19	adantr 481	. . . . . . . . 9 ⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → dom (𝐺‘𝑘) = (𝑀...𝑛))
21		fveq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀))
22		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
23	22	mpteq1d 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))
24	21, 23	eqeq12d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))
25	24	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))))
26		fveq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
27		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
28	27	mpteq1d 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
29	26, 28	eqeq12d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
30	29	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))))
31		fveq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑤 + 1)))
32		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
33	32	mpteq1d 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
34	31, 33	eqeq12d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
35	34	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))
36		fveq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘))
37		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
38	37	mpteq1d 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
39	36, 38	eqeq12d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
40	39	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑘 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))))
41		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
42		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
43	41, 42	fveq12d 6895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑘 → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘𝑘)‘𝑘))
44		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))
45		fvex 6901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘)‘𝑘) ∈ V
46	43, 44, 45	fvmpt 6995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
47	46	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘))
48		elfz1eq 13508	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
49	48	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
50	49	fveq2d 6892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑀))
51	50	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑘)‘𝑘) = ((𝐺‘𝑀)‘𝑘))
52	47, 51	eqtr2d 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
53	52	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)))
54	1, 53	ralrimi 3254	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))
55		sdc.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴)
56	55	ffnd 6715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐺‘𝑀) Fn (𝑀...𝑀))
57		fvex 6901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑚)‘𝑚) ∈ V
58	57, 44	fnmpti 6690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)
59		eqfnfv 7029	. . . . . . . . . . . . . . . . . . . 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 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝑍 ↔ 𝑤 ∈ (ℤ_≥‘𝑀))
65	2	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘𝑤) ∈ 𝐽)
66		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
67		3simpa 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
68	67	reximi 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
69	68	ss2abi 4062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}
70	63	fvexi 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...(𝑘 + 1)) ∈ V
77		elmapg 8829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
78	76, 77	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐴 ∈ 𝑉 → (ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴))
79	75, 78	imbitrrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐴 ∈ 𝑉 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ ∈ (𝐴 ↑_m (𝑀...(𝑘 + 1)))))
80	79	abssdv 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
81	74, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑_m (𝑀...(𝑘 + 1))))
82		ovex 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐴 ↑_m (𝑀...(𝑘 + 1))) ∈ V
83		ssexg 5322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
87		abrexex2g 7947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑍 ∈ V ∧ ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
88	70, 86, 87	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)
89		ssexg 5322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
90	69, 88, 89	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91		eqeq1 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑥 = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))))
92	91	3anbi2d 1441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = (𝐺‘𝑤) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
93	92	rexbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = (𝐺‘𝑤) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)))
94	93	abbidv 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
95	94	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96		oveq2 7413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐺‘𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺‘𝑤)))
97	96, 94	eqeq12d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))
98	95, 97	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐺‘𝑤) → (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
99	98	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100		sdc.11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
101	100	ovmpt4g 7551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
102	101	3com12 1123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
103	102	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
104	99, 103	vtoclga 3565	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘𝑤) ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))
105	65, 66, 90, 104	syl3c 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})
106	105, 69	eqsstrdi 4035	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
107		sdc.15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤)))
108	106, 107	sseldd 3982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))})
109		fvex 6901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑤 + 1)) ∈ V
110		feq1 6695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111		reseq1 5973	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112	111	eqeq2d 2743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113	110, 112	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114	113	rexbidv 3178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115	109, 114	elab 3667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116	108, 115	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117		nfv 1917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
118		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119		fzssp1 13540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120		fssres 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121	118, 119, 120	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122	121	fdmd 6725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
124	57, 123	fnmpti 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)
125		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
126	125	fneq1d 6639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127	124, 126	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128	127	fndmd 6651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129	122, 128	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
130		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ 𝑍)
131	130, 63	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ_≥‘𝑀))
132		fzopth 13534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
137	136	oveq2d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
138		elfzp1 13547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
139	131, 138	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140	129	reseq2d 5979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
141		fzssp1 13540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
142		resmpt 6035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))
144	140, 143	eqtr2di 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
145	125, 144	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146	145	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
147		fvres 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
148		fvres 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
149	147, 148	eqeq12d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
150	146, 149	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
151	136	eqeq2d 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
152	135, 131	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ_≥‘𝑀))
153		peano2uz 12881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (ℤ_≥‘𝑀))
154		eluzfz2 13505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑤 + 1) ∈ (ℤ_≥‘𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
155		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → (𝐺‘𝑚) = (𝐺‘(𝑤 + 1)))
156		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
157	155, 156	fveq12d 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = (𝑤 + 1) → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
158		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))
159		fvex 6901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
160	157, 158, 159	fvmpt 6995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
163		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
164		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))
165	163, 164	eqeq12d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
169	139, 168	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))
170	169	ralrimiv 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))
171		ffn 6714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
172	171	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
173	57, 158	fnmpti 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
174		eqfnfv2 7030	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))
177	176	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))
178		eqeq1 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))
179	178	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . 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 3263	. . . . . . . . . . . . . . . . . . . . 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 12886	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
189	188, 63	eleq2s 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑍 → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))
190	189	impcom 408	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
191	190	dmeqd 5903	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
192		dmmptg 6238	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ (𝑀...𝑘)((𝐺‘𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘))
193	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝑀...𝑘) → ((𝐺‘𝑚)‘𝑚) ∈ V)
194	192, 193	mprg 3067	. . . . . . . . . . . . 13 ⊢ dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘)
195	191, 194	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = (𝑀...𝑘))
196	195	eqeq1d 2734	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
197		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍)
198	197, 63	eleqtrdi 2843	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ_≥‘𝑀))
199		fzopth 13534	. . . . . . . . . . . 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 7413	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
206	205	feq2d 6700	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴))
207		sdc.4	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃))
208	207	sbcbidv 3835	. . . . . . . . . . 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 3160	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)))
214	18, 213	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))
215	214	simpld 495	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴)
216		eluzfz2 13505	. . . . 5 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘))
217	198, 216	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘))
218	215, 217	ffvelcdmd 7084	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)‘𝑘) ∈ 𝐴)
219	43	cbvmptv 5260	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑘 ∈ 𝑍 ↦ ((𝐺‘𝑘)‘𝑘))
220	1, 218, 219	fmptdf 7113	. 2 ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴)
221	214	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝐺‘𝑘) / 𝑔]𝜃)
222	190, 221	sbceq1dd 3782	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
223	222	ex 413	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝑍 → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
224	1, 223	ralrimi 3254	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
225		mpteq1 5240	. . . . . 6 ⊢ ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))
226		dfsbcq 3778	. . . . . 6 ⊢ ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
227	205, 225, 226	3syl 18	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
228	207	sbcbidv 3835	. . . . 5 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
229	227, 228	bitrd 278	. . . 4 ⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃))
230	229	cbvralvw 3234	. . 3 ⊢ (∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)
231	224, 230	sylibr 233	. 2 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)
232	70	mptex 7221	. . 3 ⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ∈ V
233		feq1 6695	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓:𝑍⟶𝐴 ↔ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴))
234		vex 3478	. . . . . . . 8 ⊢ 𝑓 ∈ V
235	234	resex 6027	. . . . . . 7 ⊢ (𝑓 ↾ (𝑀...𝑛)) ∈ V
236		sdc.2	. . . . . . 7 ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒))
237	235, 236	sbcie 3819	. . . . . 6 ⊢ ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ 𝜒)
238		reseq1 5973	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
239		fzssuz 13538	. . . . . . . . . 10 ⊢ (𝑀...𝑛) ⊆ (ℤ_≥‘𝑀)
240	239, 63	sseqtrri 4018	. . . . . . . . 9 ⊢ (𝑀...𝑛) ⊆ 𝑍
241		resmpt 6035	. . . . . . . . 9 ⊢ ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
242	240, 241	ax-mp 5	. . . . . . . 8 ⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))
243	238, 242	eqtrdi 2788	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)))
244	243	sbceq1d 3781	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
245	237, 244	bitr3id 284	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝜒 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
246	245	ralbidv 3177	. . . 4 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (∀𝑛 ∈ 𝑍 𝜒 ↔ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))
247	233, 246	anbi12d 631	. . 3 ⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ((𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒) ↔ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)))
248	232, 247	spcev 3596	. 2 ⊢ (((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))
249	220, 231, 248	syl2anc 584	1 ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 Vcvv 3474 [wsbc 3776 ⊆ wss 3947 {csn 4627 ↦ cmpt 5230 dom cdm 5675 ↾ cres 5677 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 ↑_m cmap 8816 1c1 11107 + caddc 11109 ℤcz 12554 ℤ_≥cuz 12818 ...cfz 13480

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-n0 12469 df-z 12555 df-uz 12819 df-fz 13481

This theorem is referenced by: sdclem1 36599

W3C validator