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 35637
Description: Lemma for sdc 35639. (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 (𝜑𝐺:𝑍𝐽)
32ffvelrnda 6904 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐽)
4 sdc.10 . . . . . . . . 9 𝐽 = {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)}
54eleq2i 2829 . . . . . . . 8 ((𝐺𝑘) ∈ 𝐽 ↔ (𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)})
6 nfcv 2904 . . . . . . . . . 10 𝑔𝑍
7 nfv 1922 . . . . . . . . . . 11 𝑔(𝐺𝑘):(𝑀...𝑛)⟶𝐴
8 nfsbc1v 3714 . . . . . . . . . . 11 𝑔[(𝐺𝑘) / 𝑔]𝜓
97, 8nfan 1907 . . . . . . . . . 10 𝑔((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
106, 9nfrex 3228 . . . . . . . . 9 𝑔𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
11 fvex 6730 . . . . . . . . 9 (𝐺𝑘) ∈ V
12 feq1 6526 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑛)⟶𝐴))
13 sbceq1a 3705 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝜓[(𝐺𝑘) / 𝑔]𝜓))
1412, 13anbi12d 634 . . . . . . . . . 10 (𝑔 = (𝐺𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1514rexbidv 3216 . . . . . . . . 9 (𝑔 = (𝐺𝑘) → (∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1610, 11, 15elabf 3584 . . . . . . . 8 ((𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)} ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
175, 16bitri 278 . . . . . . 7 ((𝐺𝑘) ∈ 𝐽 ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
183, 17sylib 221 . . . . . 6 ((𝜑𝑘𝑍) → ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
19 fdm 6554 . . . . . . . . . 10 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺𝑘) = (𝑀...𝑛))
2019adantr 484 . . . . . . . . 9 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → dom (𝐺𝑘) = (𝑀...𝑛))
21 fveq2 6717 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝐺𝑥) = (𝐺𝑀))
22 oveq2 7221 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
2322mpteq1d 5144 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
2421, 23eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑀 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
2524imbi2d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑀 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))))
26 fveq2 6717 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
27 oveq2 7221 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
2827mpteq1d 5144 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
2926, 28eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
3029imbi2d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))))
31 fveq2 6717 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝐺𝑥) = (𝐺‘(𝑤 + 1)))
32 oveq2 7221 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
3332mpteq1d 5144 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
3431, 33eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑤 + 1) → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
3534imbi2d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
36 fveq2 6717 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝐺𝑥) = (𝐺𝑘))
37 oveq2 7221 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
3837mpteq1d 5144 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
3936, 38eqeq12d 2753 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
4039imbi2d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))))
41 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
42 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘𝑚 = 𝑘)
4341, 42fveq12d 6724 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝐺𝑚)‘𝑚) = ((𝐺𝑘)‘𝑘))
44 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))
45 fvex 6730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘)‘𝑘) ∈ V
4643, 44, 45fvmpt 6818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
4746adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
48 elfz1eq 13123 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
4948adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
5049fveq2d 6721 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (𝑀...𝑀)) → (𝐺𝑘) = (𝐺𝑀))
5150fveq1d 6719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑘)‘𝑘) = ((𝐺𝑀)‘𝑘))
5247, 51eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
5352ex 416 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
541, 53ralrimi 3137 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
55 sdc.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺𝑀):(𝑀...𝑀)⟶𝐴)
5655ffnd 6546 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑀) Fn (𝑀...𝑀))
57 fvex 6730 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑚)‘𝑚) ∈ V
5857, 44fnmpti 6521 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)
59 eqfnfv 6852 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6056, 58, 59sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6154, 60mpbird 260 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
6261a1i 11 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
63 sdc.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
6463eleq2i 2829 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍𝑤 ∈ (ℤ𝑀))
652ffvelrnda 6904 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → (𝐺𝑤) ∈ 𝐽)
66 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → 𝑤𝑍)
67 3simpa 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6867reximi 3166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6968ss2abi 3980 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))}
7063fvexi 6731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑍 ∈ V
71 nfv 1922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘 𝑤𝑍
721, 71nfan 1907 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑘(𝜑𝑤𝑍)
73 sdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐴𝑉)
7473adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑤𝑍) → 𝐴𝑉)
75 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → :(𝑀...(𝑘 + 1))⟶𝐴)
76 ovex 7246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...(𝑘 + 1)) ∈ V
77 elmapg 8521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐴𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7876, 77mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴𝑉 → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7975, 78syl5ibr 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴𝑉 → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → ∈ (𝐴m (𝑀...(𝑘 + 1)))))
8079abssdv 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴𝑉 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
8174, 80syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
82 ovex 7246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴m (𝑀...(𝑘 + 1))) ∈ V
83 ssexg 5216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({ ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))) ∧ (𝐴m (𝑀...(𝑘 + 1))) ∈ V) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8481, 82, 83sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑍) → (𝑘𝑍 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V))
8672, 85ralrimi 3137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑍) → ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
87 abrexex2g 7737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ V ∧ ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8870, 86, 87sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
89 ssexg 5216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
9069, 88, 89sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝐺𝑤) → (𝑥 = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
92913anbi2d 1443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝐺𝑤) → ((:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9392rexbidv 3216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝐺𝑤) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9493abbidv 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
9594eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96 oveq2 7221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺𝑤)))
9796, 94eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ((𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))
9895, 97imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐺𝑤) → (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
9998imbi2d 344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐺𝑤) → ((𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100 sdc.11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐹 = (𝑤𝑍, 𝑥𝐽 ↦ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
101100ovmpt4g 7356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝑍𝑥𝐽 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1021013com12 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐽𝑤𝑍 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1031023exp 1121 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10499, 103vtoclga 3489 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) ∈ 𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10565, 66, 90, 104syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
106105, 69eqsstrdi 3955 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
107 sdc.15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺𝑤)))
108106, 107sseldd 3902 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
109 fvex 6730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑤 + 1)) ∈ V
110 feq1 6526 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → (:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111 reseq1 5845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = (𝐺‘(𝑤 + 1)) → ( ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112111eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → ((𝐺𝑤) = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113110, 112anbi12d 634 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = (𝐺‘(𝑤 + 1)) → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114113rexbidv 3216 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝐺‘(𝑤 + 1)) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115109, 114elab 3587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116108, 115sylib 221 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117 nfv 1922 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
118 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119 fzssp1 13155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120 fssres 6585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121118, 119, 120sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122121fdmd 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
12457, 123fnmpti 6521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)
125 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
126125fneq1d 6472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127124, 126mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128127fndmd 6483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129122, 128eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
130 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘𝑍)
131130, 63eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ𝑀))
132 fzopth 13149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
134129, 133mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀 = 𝑀𝑘 = 𝑤))
135134simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 = 𝑤)
136135oveq1d 7228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
137136oveq2d 7229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
138 elfzp1 13162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
139131, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140129reseq2d 5851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
141 fzssp1 13155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
142 resmpt 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
143141, 142ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
144140, 143eqtr2di 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
145125, 144eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146145fveq1d 6719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
147 fvres 6736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
148 fvres 6736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
149147, 148eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
150146, 149syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
151136eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
152135, 131eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ𝑀))
153 peano2uz 12497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (ℤ𝑀))
154 eluzfz2 13120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
155 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → (𝐺𝑚) = (𝐺‘(𝑤 + 1)))
156 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
157155, 156fveq12d 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 = (𝑤 + 1) → ((𝐺𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
158 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))
159 fvex 6730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
160157, 158, 159fvmpt 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
161152, 153, 154, 1604syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162161eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
163 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
164 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
165163, 164eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1))))
166162, 165syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
167151, 166sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
168150, 167jaod 859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
169139, 168sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
170169ralrimiv 3104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
171 ffn 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
172171ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
17357, 158fnmpti 6521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
174 eqfnfv2 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
175172, 173, 174sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
176137, 170, 175mpbir2and 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
177176expr 460 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
178 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
179178imbi1d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
180177, 179syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
181180expimpd 457 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑍) ∧ 𝑘𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
182181ex 416 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝑘𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))))
18372, 117, 182rexlimd 3236 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → (∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
184116, 183mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑍) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
185184expcom 417 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍 → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18664, 185sylbir 238 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (ℤ𝑀) → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
187186a2d 29 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (ℤ𝑀) → ((𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18825, 30, 35, 40, 62, 187uzind4 12502 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
189188, 63eleq2s 2856 . . . . . . . . . . . . . . 15 (𝑘𝑍 → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
190189impcom 411 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
191190dmeqd 5774 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
192 dmmptg 6105 . . . . . . . . . . . . . 14 (∀𝑚 ∈ (𝑀...𝑘)((𝐺𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘))
19357a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝑀...𝑘) → ((𝐺𝑚)‘𝑚) ∈ V)
194192, 193mprg 3075 . . . . . . . . . . . . 13 dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘)
195191, 194eqtrdi 2794 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = (𝑀...𝑘))
196195eqeq1d 2739 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
197 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑘𝑍)
198197, 63eleqtrdi 2848 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
199 fzopth 13149 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
200198, 199syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
201196, 200bitrd 282 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
202 simpr 488 . . . . . . . . . 10 ((𝑀 = 𝑀𝑘 = 𝑛) → 𝑘 = 𝑛)
203201, 202syl6bi 256 . . . . . . . . 9 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
20420, 203syl5 34 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
205 oveq2 7221 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
206205feq2d 6531 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑘)⟶𝐴))
207 sdc.4 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝜓𝜃))
208207sbcbidv 3753 . . . . . . . . . . 11 (𝑛 = 𝑘 → ([(𝐺𝑘) / 𝑔]𝜓[(𝐺𝑘) / 𝑔]𝜃))
209206, 208anbi12d 634 . . . . . . . . . 10 (𝑛 = 𝑘 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
210209equcoms 2028 . . . . . . . . 9 (𝑘 = 𝑛 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
211210biimpcd 252 . . . . . . . 8 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
212204, 211sylcom 30 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
213212rexlimdvw 3209 . . . . . 6 ((𝜑𝑘𝑍) → (∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
21418, 213mpd 15 . . . . 5 ((𝜑𝑘𝑍) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃))
215214simpld 498 . . . 4 ((𝜑𝑘𝑍) → (𝐺𝑘):(𝑀...𝑘)⟶𝐴)
216 eluzfz2 13120 . . . . 5 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
217198, 216syl 17 . . . 4 ((𝜑𝑘𝑍) → 𝑘 ∈ (𝑀...𝑘))
218215, 217ffvelrnd 6905 . . 3 ((𝜑𝑘𝑍) → ((𝐺𝑘)‘𝑘) ∈ 𝐴)
21943cbvmptv 5158 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) = (𝑘𝑍 ↦ ((𝐺𝑘)‘𝑘))
2201, 218, 219fmptdf 6934 . 2 (𝜑 → (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴)
221214simprd 499 . . . . . 6 ((𝜑𝑘𝑍) → [(𝐺𝑘) / 𝑔]𝜃)
222190, 221sbceq1dd 3700 . . . . 5 ((𝜑𝑘𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
223222ex 416 . . . 4 (𝜑 → (𝑘𝑍[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
2241, 223ralrimi 3137 . . 3 (𝜑 → ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
225 mpteq1 5143 . . . . . 6 ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
226 dfsbcq 3696 . . . . . 6 ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
227205, 225, 2263syl 18 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
228207sbcbidv 3753 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
229227, 228bitrd 282 . . . 4 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
230229cbvralvw 3358 . . 3 (∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
231224, 230sylibr 237 . 2 (𝜑 → ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)
23270mptex 7039 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ∈ V
233 feq1 6526 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓:𝑍𝐴 ↔ (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴))
234 vex 3412 . . . . . . . 8 𝑓 ∈ V
235234resex 5899 . . . . . . 7 (𝑓 ↾ (𝑀...𝑛)) ∈ V
236 sdc.2 . . . . . . 7 (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓𝜒))
237235, 236sbcie 3737 . . . . . 6 ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓𝜒)
238 reseq1 5845 . . . . . . . 8 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
239 fzssuz 13153 . . . . . . . . . 10 (𝑀...𝑛) ⊆ (ℤ𝑀)
240239, 63sseqtrri 3938 . . . . . . . . 9 (𝑀...𝑛) ⊆ 𝑍
241 resmpt 5905 . . . . . . . . 9 ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
242240, 241ax-mp 5 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚))
243238, 242eqtrdi 2794 . . . . . . 7 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
244243sbceq1d 3699 . . . . . 6 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
245237, 244bitr3id 288 . . . . 5 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝜒[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
246245ralbidv 3118 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (∀𝑛𝑍 𝜒 ↔ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
247233, 246anbi12d 634 . . 3 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ((𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒) ↔ ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)))
248232, 247spcev 3521 . 2 (((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
249220, 231, 248syl2anc 587 1 (𝜑 → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wex 1787  wnf 1791  wcel 2110  {cab 2714  wral 3061  wrex 3062  Vcvv 3408  [wsbc 3694  wss 3866  {csn 4541  cmpt 5135  dom cdm 5551  cres 5553   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  cmpo 7215  m cmap 8508  1c1 10730   + caddc 10732  cz 12176  cuz 12438  ...cfz 13095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096
This theorem is referenced by:  sdclem1  35638
  Copyright terms: Public domain W3C validator