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

Theorem sdclem2 37077
Description: Lemma for sdc 37079. (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.
StepHypRef Expression
1 sdc.12 . . 3 𝑘𝜑
2 sdc.13 . . . . . . . 8 (𝜑𝐺:𝑍𝐽)
32ffvelcdmda 7086 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐽)
4 sdc.10 . . . . . . . . 9 𝐽 = {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)}
54eleq2i 2824 . . . . . . . 8 ((𝐺𝑘) ∈ 𝐽 ↔ (𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)})
6 nfcv 2902 . . . . . . . . . 10 𝑔𝑍
7 nfv 1916 . . . . . . . . . . 11 𝑔(𝐺𝑘):(𝑀...𝑛)⟶𝐴
8 nfsbc1v 3797 . . . . . . . . . . 11 𝑔[(𝐺𝑘) / 𝑔]𝜓
97, 8nfan 1901 . . . . . . . . . 10 𝑔((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
106, 9nfrexw 3309 . . . . . . . . 9 𝑔𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
11 fvex 6904 . . . . . . . . 9 (𝐺𝑘) ∈ V
12 feq1 6698 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑛)⟶𝐴))
13 sbceq1a 3788 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝜓[(𝐺𝑘) / 𝑔]𝜓))
1412, 13anbi12d 630 . . . . . . . . . 10 (𝑔 = (𝐺𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1514rexbidv 3177 . . . . . . . . 9 (𝑔 = (𝐺𝑘) → (∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1610, 11, 15elabf 3665 . . . . . . . 8 ((𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)} ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
175, 16bitri 275 . . . . . . 7 ((𝐺𝑘) ∈ 𝐽 ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
183, 17sylib 217 . . . . . 6 ((𝜑𝑘𝑍) → ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
19 fdm 6726 . . . . . . . . . 10 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺𝑘) = (𝑀...𝑛))
2019adantr 480 . . . . . . . . 9 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → dom (𝐺𝑘) = (𝑀...𝑛))
21 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝐺𝑥) = (𝐺𝑀))
22 oveq2 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
2322mpteq1d 5243 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
2421, 23eqeq12d 2747 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑀 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
2524imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑀 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))))
26 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
27 oveq2 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
2827mpteq1d 5243 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
2926, 28eqeq12d 2747 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
3029imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))))
31 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝐺𝑥) = (𝐺‘(𝑤 + 1)))
32 oveq2 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
3332mpteq1d 5243 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
3431, 33eqeq12d 2747 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑤 + 1) → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
3534imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
36 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝐺𝑥) = (𝐺𝑘))
37 oveq2 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
3837mpteq1d 5243 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
3936, 38eqeq12d 2747 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
4039imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))))
41 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
42 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘𝑚 = 𝑘)
4341, 42fveq12d 6898 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝐺𝑚)‘𝑚) = ((𝐺𝑘)‘𝑘))
44 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))
45 fvex 6904 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘)‘𝑘) ∈ V
4643, 44, 45fvmpt 6998 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
4746adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
48 elfz1eq 13519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
4948adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
5049fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (𝑀...𝑀)) → (𝐺𝑘) = (𝐺𝑀))
5150fveq1d 6893 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑘)‘𝑘) = ((𝐺𝑀)‘𝑘))
5247, 51eqtr2d 2772 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
5352ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
541, 53ralrimi 3253 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
55 sdc.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺𝑀):(𝑀...𝑀)⟶𝐴)
5655ffnd 6718 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑀) Fn (𝑀...𝑀))
57 fvex 6904 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑚)‘𝑚) ∈ V
5857, 44fnmpti 6693 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)
59 eqfnfv 7032 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6056, 58, 59sylancl 585 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6154, 60mpbird 257 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
6261a1i 11 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
63 sdc.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
6463eleq2i 2824 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍𝑤 ∈ (ℤ𝑀))
652ffvelcdmda 7086 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → (𝐺𝑤) ∈ 𝐽)
66 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → 𝑤𝑍)
67 3simpa 1147 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6867reximi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6968ss2abi 4063 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))}
7063fvexi 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑍 ∈ V
71 nfv 1916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘 𝑤𝑍
721, 71nfan 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑘(𝜑𝑤𝑍)
73 sdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐴𝑉)
7473adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑤𝑍) → 𝐴𝑉)
75 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → :(𝑀...(𝑘 + 1))⟶𝐴)
76 ovex 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...(𝑘 + 1)) ∈ V
77 elmapg 8839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐴𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7876, 77mpan2 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴𝑉 → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7975, 78imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴𝑉 → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → ∈ (𝐴m (𝑀...(𝑘 + 1)))))
8079abssdv 4065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴𝑉 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
8174, 80syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
82 ovex 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴m (𝑀...(𝑘 + 1))) ∈ V
83 ssexg 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({ ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))) ∧ (𝐴m (𝑀...(𝑘 + 1))) ∈ V) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8481, 82, 83sylancl 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑍) → (𝑘𝑍 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V))
8672, 85ralrimi 3253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑍) → ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
87 abrexex2g 7955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ V ∧ ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8870, 86, 87sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
89 ssexg 5323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
9069, 88, 89sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91 eqeq1 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝐺𝑤) → (𝑥 = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
92913anbi2d 1440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝐺𝑤) → ((:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9392rexbidv 3177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝐺𝑤) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9493abbidv 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
9594eleq1d 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96 oveq2 7420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺𝑤)))
9796, 94eqeq12d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ((𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))
9895, 97imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐺𝑤) → (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
9998imbi2d 340 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐺𝑤) → ((𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100 sdc.11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐹 = (𝑤𝑍, 𝑥𝐽 ↦ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
101100ovmpt4g 7558 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝑍𝑥𝐽 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1021013com12 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐽𝑤𝑍 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1031023exp 1118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10499, 103vtoclga 3566 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) ∈ 𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10565, 66, 90, 104syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
106105, 69eqsstrdi 4036 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
107 sdc.15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺𝑤)))
108106, 107sseldd 3983 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
109 fvex 6904 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑤 + 1)) ∈ V
110 feq1 6698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → (:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111 reseq1 5975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = (𝐺‘(𝑤 + 1)) → ( ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112111eqeq2d 2742 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → ((𝐺𝑤) = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113110, 112anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = (𝐺‘(𝑤 + 1)) → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114113rexbidv 3177 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝐺‘(𝑤 + 1)) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115109, 114elab 3668 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116108, 115sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117 nfv 1916 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
118 simprl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119 fzssp1 13551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120 fssres 6757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121118, 119, 120sylancl 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122121fdmd 6728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
12457, 123fnmpti 6693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)
125 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
126125fneq1d 6642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127124, 126mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128127fndmd 6654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129122, 128eqtr3d 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
130 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘𝑍)
131130, 63eleqtrdi 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ𝑀))
132 fzopth 13545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
134129, 133mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀 = 𝑀𝑘 = 𝑤))
135134simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 = 𝑤)
136135oveq1d 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
137136oveq2d 7428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
138 elfzp1 13558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
139131, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140129reseq2d 5981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
141 fzssp1 13551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
142 resmpt 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
143141, 142ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
144140, 143eqtr2di 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
145125, 144eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146145fveq1d 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
147 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
148 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
149147, 148eqeq12d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
150146, 149syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
151136eqeq2d 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
152135, 131eqeltrrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ𝑀))
153 peano2uz 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (ℤ𝑀))
154 eluzfz2 13516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
155 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → (𝐺𝑚) = (𝐺‘(𝑤 + 1)))
156 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
157155, 156fveq12d 6898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 = (𝑤 + 1) → ((𝐺𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
158 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))
159 fvex 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
160157, 158, 159fvmpt 6998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
161152, 153, 154, 1604syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162161eqcomd 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
163 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
164 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
165163, 164eqeq12d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1))))
166162, 165syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
167151, 166sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
168150, 167jaod 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
169139, 168sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
170169ralrimiv 3144 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
171 ffn 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
172171ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
17357, 158fnmpti 6693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
174 eqfnfv2 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
175172, 173, 174sylancl 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
176137, 170, 175mpbir2and 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
177176expr 456 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
178 eqeq1 2735 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
179178imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
180177, 179syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
181180expimpd 453 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑍) ∧ 𝑘𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
182181ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝑘𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))))
18372, 117, 182rexlimd 3262 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → (∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
184116, 183mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑍) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
185184expcom 413 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍 → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18664, 185sylbir 234 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (ℤ𝑀) → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
187186a2d 29 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (ℤ𝑀) → ((𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18825, 30, 35, 40, 62, 187uzind4 12897 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
189188, 63eleq2s 2850 . . . . . . . . . . . . . . 15 (𝑘𝑍 → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
190189impcom 407 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
191190dmeqd 5905 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
192 dmmptg 6241 . . . . . . . . . . . . . 14 (∀𝑚 ∈ (𝑀...𝑘)((𝐺𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘))
19357a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝑀...𝑘) → ((𝐺𝑚)‘𝑚) ∈ V)
194192, 193mprg 3066 . . . . . . . . . . . . 13 dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘)
195191, 194eqtrdi 2787 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = (𝑀...𝑘))
196195eqeq1d 2733 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
197 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑘𝑍)
198197, 63eleqtrdi 2842 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
199 fzopth 13545 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
200198, 199syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
201196, 200bitrd 279 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
202 simpr 484 . . . . . . . . . 10 ((𝑀 = 𝑀𝑘 = 𝑛) → 𝑘 = 𝑛)
203201, 202syl6bi 253 . . . . . . . . 9 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
20420, 203syl5 34 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
205 oveq2 7420 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
206205feq2d 6703 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑘)⟶𝐴))
207 sdc.4 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝜓𝜃))
208207sbcbidv 3836 . . . . . . . . . . 11 (𝑛 = 𝑘 → ([(𝐺𝑘) / 𝑔]𝜓[(𝐺𝑘) / 𝑔]𝜃))
209206, 208anbi12d 630 . . . . . . . . . 10 (𝑛 = 𝑘 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
210209equcoms 2022 . . . . . . . . 9 (𝑘 = 𝑛 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
211210biimpcd 248 . . . . . . . 8 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
212204, 211sylcom 30 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
213212rexlimdvw 3159 . . . . . 6 ((𝜑𝑘𝑍) → (∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
21418, 213mpd 15 . . . . 5 ((𝜑𝑘𝑍) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃))
215214simpld 494 . . . 4 ((𝜑𝑘𝑍) → (𝐺𝑘):(𝑀...𝑘)⟶𝐴)
216 eluzfz2 13516 . . . . 5 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
217198, 216syl 17 . . . 4 ((𝜑𝑘𝑍) → 𝑘 ∈ (𝑀...𝑘))
218215, 217ffvelcdmd 7087 . . 3 ((𝜑𝑘𝑍) → ((𝐺𝑘)‘𝑘) ∈ 𝐴)
21943cbvmptv 5261 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) = (𝑘𝑍 ↦ ((𝐺𝑘)‘𝑘))
2201, 218, 219fmptdf 7118 . 2 (𝜑 → (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴)
221214simprd 495 . . . . . 6 ((𝜑𝑘𝑍) → [(𝐺𝑘) / 𝑔]𝜃)
222190, 221sbceq1dd 3783 . . . . 5 ((𝜑𝑘𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
223222ex 412 . . . 4 (𝜑 → (𝑘𝑍[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
2241, 223ralrimi 3253 . . 3 (𝜑 → ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
225 mpteq1 5241 . . . . . 6 ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
226 dfsbcq 3779 . . . . . 6 ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
227205, 225, 2263syl 18 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
228207sbcbidv 3836 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
229227, 228bitrd 279 . . . 4 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
230229cbvralvw 3233 . . 3 (∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
231224, 230sylibr 233 . 2 (𝜑 → ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)
23270mptex 7227 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ∈ V
233 feq1 6698 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓:𝑍𝐴 ↔ (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴))
234 vex 3477 . . . . . . . 8 𝑓 ∈ V
235234resex 6029 . . . . . . 7 (𝑓 ↾ (𝑀...𝑛)) ∈ V
236 sdc.2 . . . . . . 7 (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓𝜒))
237235, 236sbcie 3820 . . . . . 6 ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓𝜒)
238 reseq1 5975 . . . . . . . 8 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
239 fzssuz 13549 . . . . . . . . . 10 (𝑀...𝑛) ⊆ (ℤ𝑀)
240239, 63sseqtrri 4019 . . . . . . . . 9 (𝑀...𝑛) ⊆ 𝑍
241 resmpt 6037 . . . . . . . . 9 ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
242240, 241ax-mp 5 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚))
243238, 242eqtrdi 2787 . . . . . . 7 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
244243sbceq1d 3782 . . . . . 6 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
245237, 244bitr3id 285 . . . . 5 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝜒[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
246245ralbidv 3176 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (∀𝑛𝑍 𝜒 ↔ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
247233, 246anbi12d 630 . . 3 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ((𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒) ↔ ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)))
248232, 247spcev 3596 . 2 (((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
249220, 231, 248syl2anc 583 1 (𝜑 → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844  w3a 1086   = wceq 1540  wex 1780  wnf 1784  wcel 2105  {cab 2708  wral 3060  wrex 3069  Vcvv 3473  [wsbc 3777  wss 3948  {csn 4628  cmpt 5231  dom cdm 5676  cres 5678   Fn wfn 6538  wf 6539  cfv 6543  (class class class)co 7412  cmpo 7414  m cmap 8826  1c1 11117   + caddc 11119  cz 12565  cuz 12829  ...cfz 13491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-n0 12480  df-z 12566  df-uz 12830  df-fz 13492
This theorem is referenced by:  sdclem1  37078
  Copyright terms: Public domain W3C validator