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 34898
Description: Lemma for sdc 34900. (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 6843 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐽)
4 sdc.10 . . . . . . . . 9 𝐽 = {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)}
54eleq2i 2901 . . . . . . . 8 ((𝐺𝑘) ∈ 𝐽 ↔ (𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)})
6 nfcv 2974 . . . . . . . . . 10 𝑔𝑍
7 nfv 1906 . . . . . . . . . . 11 𝑔(𝐺𝑘):(𝑀...𝑛)⟶𝐴
8 nfsbc1v 3789 . . . . . . . . . . 11 𝑔[(𝐺𝑘) / 𝑔]𝜓
97, 8nfan 1891 . . . . . . . . . 10 𝑔((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
106, 9nfrex 3306 . . . . . . . . 9 𝑔𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
11 fvex 6676 . . . . . . . . 9 (𝐺𝑘) ∈ V
12 feq1 6488 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑛)⟶𝐴))
13 sbceq1a 3780 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝜓[(𝐺𝑘) / 𝑔]𝜓))
1412, 13anbi12d 630 . . . . . . . . . 10 (𝑔 = (𝐺𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1514rexbidv 3294 . . . . . . . . 9 (𝑔 = (𝐺𝑘) → (∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1610, 11, 15elabf 3662 . . . . . . . 8 ((𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)} ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
175, 16bitri 276 . . . . . . 7 ((𝐺𝑘) ∈ 𝐽 ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
183, 17sylib 219 . . . . . 6 ((𝜑𝑘𝑍) → ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
19 fdm 6515 . . . . . . . . . 10 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺𝑘) = (𝑀...𝑛))
2019adantr 481 . . . . . . . . 9 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → dom (𝐺𝑘) = (𝑀...𝑛))
21 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝐺𝑥) = (𝐺𝑀))
22 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
2322mpteq1d 5146 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
2421, 23eqeq12d 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑀 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
2524imbi2d 342 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑀 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))))
26 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
27 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
2827mpteq1d 5146 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
2926, 28eqeq12d 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
3029imbi2d 342 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))))
31 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝐺𝑥) = (𝐺‘(𝑤 + 1)))
32 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
3332mpteq1d 5146 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
3431, 33eqeq12d 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑤 + 1) → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
3534imbi2d 342 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
36 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝐺𝑥) = (𝐺𝑘))
37 oveq2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
3837mpteq1d 5146 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
3936, 38eqeq12d 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
4039imbi2d 342 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))))
41 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
42 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘𝑚 = 𝑘)
4341, 42fveq12d 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝐺𝑚)‘𝑚) = ((𝐺𝑘)‘𝑘))
44 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))
45 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘)‘𝑘) ∈ V
4643, 44, 45fvmpt 6761 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
4746adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
48 elfz1eq 12906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
4948adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
5049fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (𝑀...𝑀)) → (𝐺𝑘) = (𝐺𝑀))
5150fveq1d 6665 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑘)‘𝑘) = ((𝐺𝑀)‘𝑘))
5247, 51eqtr2d 2854 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
5352ex 413 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
541, 53ralrimi 3213 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
55 sdc.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺𝑀):(𝑀...𝑀)⟶𝐴)
5655ffnd 6508 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑀) Fn (𝑀...𝑀))
57 fvex 6676 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑚)‘𝑚) ∈ V
5857, 44fnmpti 6484 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)
59 eqfnfv 6794 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6056, 58, 59sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6154, 60mpbird 258 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
6261a1i 11 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
63 sdc.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
6463eleq2i 2901 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍𝑤 ∈ (ℤ𝑀))
652ffvelrnda 6843 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → (𝐺𝑤) ∈ 𝐽)
66 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → 𝑤𝑍)
67 3simpa 1140 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6867reximi 3240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6968ss2abi 4040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))}
7063fvexi 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑍 ∈ V
71 nfv 1906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘 𝑤𝑍
721, 71nfan 1891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑘(𝜑𝑤𝑍)
73 sdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐴𝑉)
7473adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑤𝑍) → 𝐴𝑉)
75 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → :(𝑀...(𝑘 + 1))⟶𝐴)
76 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...(𝑘 + 1)) ∈ V
77 elmapg 8408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐴𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7876, 77mpan2 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴𝑉 → ( ∈ (𝐴m (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
7975, 78syl5ibr 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴𝑉 → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → ∈ (𝐴m (𝑀...(𝑘 + 1)))))
8079abssdv 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴𝑉 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
8174, 80syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))))
82 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴m (𝑀...(𝑘 + 1))) ∈ V
83 ssexg 5218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({ ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴m (𝑀...(𝑘 + 1))) ∧ (𝐴m (𝑀...(𝑘 + 1))) ∈ V) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8481, 82, 83sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑍) → (𝑘𝑍 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V))
8672, 85ralrimi 3213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑍) → ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
87 abrexex2g 7654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ V ∧ ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8870, 86, 87sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
89 ssexg 5218 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
9069, 88, 89sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
91 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝐺𝑤) → (𝑥 = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
92913anbi2d 1432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝐺𝑤) → ((:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9392rexbidv 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝐺𝑤) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9493abbidv 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
9594eleq1d 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
96 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺𝑤)))
9796, 94eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ((𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))
9895, 97imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐺𝑤) → (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
9998imbi2d 342 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐺𝑤) → ((𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
100 sdc.11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐹 = (𝑤𝑍, 𝑥𝐽 ↦ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
101100ovmpt4g 7286 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝑍𝑥𝐽 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1021013com12 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐽𝑤𝑍 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1031023exp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10499, 103vtoclga 3571 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) ∈ 𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10565, 66, 90, 104syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
106105, 69eqsstrdi 4018 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
107 sdc.15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺𝑤)))
108106, 107sseldd 3965 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
109 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑤 + 1)) ∈ V
110 feq1 6488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → (:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
111 reseq1 5840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = (𝐺‘(𝑤 + 1)) → ( ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
112111eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → ((𝐺𝑤) = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
113110, 112anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = (𝐺‘(𝑤 + 1)) → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
114113rexbidv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝐺‘(𝑤 + 1)) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
115109, 114elab 3664 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
116108, 115sylib 219 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
117 nfv 1906 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
118 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
119 fzssp1 12938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
120 fssres 6537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
121118, 119, 120sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
122121fdmd 6516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
123 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
12457, 123fnmpti 6484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)
125 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
126125fneq1d 6439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)))
127124, 126mpbiri 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
128 fndm 6448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
130122, 129eqtr3d 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
131 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘𝑍)
132131, 63eleqtrdi 2920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ𝑀))
133 fzopth 12932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
135130, 134mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀 = 𝑀𝑘 = 𝑤))
136135simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 = 𝑤)
137136oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
138137oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
139 elfzp1 12945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
140132, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
141130reseq2d 5846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
142 fzssp1 12938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
143 resmpt 5898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
144142, 143ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
145141, 144syl6req 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
146125, 145eqtrd 2853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
147146fveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
148 fvres 6682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
149 fvres 6682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
150148, 149eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
151147, 150syl5ibcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
152137eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
153136, 132eqeltrrd 2911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ𝑀))
154 peano2uz 12289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (ℤ𝑀))
155 eluzfz2 12903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
156 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → (𝐺𝑚) = (𝐺‘(𝑤 + 1)))
157 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
158156, 157fveq12d 6670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 = (𝑤 + 1) → ((𝐺𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
159 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))
160 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
161158, 159, 160fvmpt 6761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162153, 154, 155, 1614syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
163162eqcomd 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
164 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
165 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
166164, 165eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1))))
167163, 166syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
168152, 167sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
169151, 168jaod 853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
170140, 169sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
171170ralrimiv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
172 ffn 6507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
173172ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
17457, 159fnmpti 6484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
175 eqfnfv2 6795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
176173, 174, 175sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
177138, 171, 176mpbir2and 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
178177expr 457 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
179 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
180179imbi1d 343 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
181178, 180syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
182181expimpd 454 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑍) ∧ 𝑘𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
183182ex 413 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝑘𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))))
18472, 117, 183rexlimd 3314 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → (∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
185116, 184mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑍) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
186185expcom 414 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍 → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18764, 186sylbir 236 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (ℤ𝑀) → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
188187a2d 29 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (ℤ𝑀) → ((𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
18925, 30, 35, 40, 62, 188uzind4 12294 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
190189, 63eleq2s 2928 . . . . . . . . . . . . . . 15 (𝑘𝑍 → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
191190impcom 408 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
192191dmeqd 5767 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
193 dmmptg 6089 . . . . . . . . . . . . . 14 (∀𝑚 ∈ (𝑀...𝑘)((𝐺𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘))
19457a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝑀...𝑘) → ((𝐺𝑚)‘𝑚) ∈ V)
195193, 194mprg 3149 . . . . . . . . . . . . 13 dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘)
196192, 195syl6eq 2869 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = (𝑀...𝑘))
197196eqeq1d 2820 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
198 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑘𝑍)
199198, 63eleqtrdi 2920 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
200 fzopth 12932 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
201199, 200syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
202197, 201bitrd 280 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
203 simpr 485 . . . . . . . . . 10 ((𝑀 = 𝑀𝑘 = 𝑛) → 𝑘 = 𝑛)
204202, 203syl6bi 254 . . . . . . . . 9 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
20520, 204syl5 34 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
206 oveq2 7153 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
207206feq2d 6493 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑘)⟶𝐴))
208 sdc.4 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝜓𝜃))
209208sbcbidv 3824 . . . . . . . . . . 11 (𝑛 = 𝑘 → ([(𝐺𝑘) / 𝑔]𝜓[(𝐺𝑘) / 𝑔]𝜃))
210207, 209anbi12d 630 . . . . . . . . . 10 (𝑛 = 𝑘 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
211210equcoms 2018 . . . . . . . . 9 (𝑘 = 𝑛 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
212211biimpcd 250 . . . . . . . 8 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
213205, 212sylcom 30 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
214213rexlimdvw 3287 . . . . . 6 ((𝜑𝑘𝑍) → (∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
21518, 214mpd 15 . . . . 5 ((𝜑𝑘𝑍) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃))
216215simpld 495 . . . 4 ((𝜑𝑘𝑍) → (𝐺𝑘):(𝑀...𝑘)⟶𝐴)
217 eluzfz2 12903 . . . . 5 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
218199, 217syl 17 . . . 4 ((𝜑𝑘𝑍) → 𝑘 ∈ (𝑀...𝑘))
219216, 218ffvelrnd 6844 . . 3 ((𝜑𝑘𝑍) → ((𝐺𝑘)‘𝑘) ∈ 𝐴)
22043cbvmptv 5160 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) = (𝑘𝑍 ↦ ((𝐺𝑘)‘𝑘))
2211, 219, 220fmptdf 6873 . 2 (𝜑 → (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴)
222215simprd 496 . . . . . 6 ((𝜑𝑘𝑍) → [(𝐺𝑘) / 𝑔]𝜃)
223191, 222sbceq1dd 3775 . . . . 5 ((𝜑𝑘𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
224223ex 413 . . . 4 (𝜑 → (𝑘𝑍[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
2251, 224ralrimi 3213 . . 3 (𝜑 → ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
226 mpteq1 5145 . . . . . 6 ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
227 dfsbcq 3771 . . . . . 6 ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
228206, 226, 2273syl 18 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
229208sbcbidv 3824 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
230228, 229bitrd 280 . . . 4 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
231230cbvralvw 3447 . . 3 (∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
232225, 231sylibr 235 . 2 (𝜑 → ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)
23370mptex 6977 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ∈ V
234 feq1 6488 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓:𝑍𝐴 ↔ (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴))
235 vex 3495 . . . . . . . 8 𝑓 ∈ V
236235resex 5892 . . . . . . 7 (𝑓 ↾ (𝑀...𝑛)) ∈ V
237 sdc.2 . . . . . . 7 (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓𝜒))
238236, 237sbcie 3809 . . . . . 6 ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓𝜒)
239 reseq1 5840 . . . . . . . 8 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
240 fzssuz 12936 . . . . . . . . . 10 (𝑀...𝑛) ⊆ (ℤ𝑀)
241240, 63sseqtrri 4001 . . . . . . . . 9 (𝑀...𝑛) ⊆ 𝑍
242 resmpt 5898 . . . . . . . . 9 ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
243241, 242ax-mp 5 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚))
244239, 243syl6eq 2869 . . . . . . 7 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
245244sbceq1d 3774 . . . . . 6 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
246238, 245syl5bbr 286 . . . . 5 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝜒[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
247246ralbidv 3194 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (∀𝑛𝑍 𝜒 ↔ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
248234, 247anbi12d 630 . . 3 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ((𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒) ↔ ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)))
249233, 248spcev 3604 . 2 (((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
250221, 232, 249syl2anc 584 1 (𝜑 → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wnf 1775  wcel 2105  {cab 2796  wral 3135  wrex 3136  Vcvv 3492  [wsbc 3769  wss 3933  {csn 4557  cmpt 5137  dom cdm 5548  cres 5550   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  m cmap 8395  1c1 10526   + caddc 10528  cz 11969  cuz 12231  ...cfz 12880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12881
This theorem is referenced by:  sdclem1  34899
  Copyright terms: Public domain W3C validator