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 33870
Description: Lemma for sdc 33872. (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 6502 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐽)
4 sdc.10 . . . . . . . . 9 𝐽 = {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)}
54eleq2i 2842 . . . . . . . 8 ((𝐺𝑘) ∈ 𝐽 ↔ (𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)})
6 nfcv 2913 . . . . . . . . . 10 𝑔𝑍
7 nfv 1995 . . . . . . . . . . 11 𝑔(𝐺𝑘):(𝑀...𝑛)⟶𝐴
8 nfsbc1v 3607 . . . . . . . . . . 11 𝑔[(𝐺𝑘) / 𝑔]𝜓
97, 8nfan 1980 . . . . . . . . . 10 𝑔((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
106, 9nfrex 3155 . . . . . . . . 9 𝑔𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
11 fvex 6342 . . . . . . . . 9 (𝐺𝑘) ∈ V
12 feq1 6166 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑛)⟶𝐴))
13 sbceq1a 3598 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝜓[(𝐺𝑘) / 𝑔]𝜓))
1412, 13anbi12d 616 . . . . . . . . . 10 (𝑔 = (𝐺𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1514rexbidv 3200 . . . . . . . . 9 (𝑔 = (𝐺𝑘) → (∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1610, 11, 15elabf 3500 . . . . . . . 8 ((𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)} ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
175, 16bitri 264 . . . . . . 7 ((𝐺𝑘) ∈ 𝐽 ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
183, 17sylib 208 . . . . . 6 ((𝜑𝑘𝑍) → ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
19 fdm 6191 . . . . . . . . . 10 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺𝑘) = (𝑀...𝑛))
2019adantr 466 . . . . . . . . 9 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → dom (𝐺𝑘) = (𝑀...𝑛))
21 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝐺𝑥) = (𝐺𝑀))
22 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
2322mpteq1d 4872 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
2421, 23eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑀 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
2524imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑀 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))))
26 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
27 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
2827mpteq1d 4872 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
2926, 28eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
3029imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))))
31 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝐺𝑥) = (𝐺‘(𝑤 + 1)))
32 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
3332mpteq1d 4872 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
3431, 33eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑤 + 1) → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
3534imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
36 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝐺𝑥) = (𝐺𝑘))
37 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
3837mpteq1d 4872 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
3936, 38eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
4039imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))))
41 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
42 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘𝑚 = 𝑘)
4341, 42fveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝐺𝑚)‘𝑚) = ((𝐺𝑘)‘𝑘))
44 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))
45 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘)‘𝑘) ∈ V
4643, 44, 45fvmpt 6424 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
4746adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
48 elfz1eq 12559 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
4948adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
5049fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (𝑀...𝑀)) → (𝐺𝑘) = (𝐺𝑀))
5150fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑘)‘𝑘) = ((𝐺𝑀)‘𝑘))
5247, 51eqtr2d 2806 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
5352ex 397 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
541, 53ralrimi 3106 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
55 sdc.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺𝑀):(𝑀...𝑀)⟶𝐴)
56 ffn 6185 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑀):(𝑀...𝑀)⟶𝐴 → (𝐺𝑀) Fn (𝑀...𝑀))
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑀) Fn (𝑀...𝑀))
58 fvex 6342 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑚)‘𝑚) ∈ V
5958, 44fnmpti 6162 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)
60 eqfnfv 6454 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6157, 59, 60sylancl 574 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6254, 61mpbird 247 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
6362a1i 11 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
64 sdc.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
6564eleq2i 2842 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍𝑤 ∈ (ℤ𝑀))
662ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → (𝐺𝑤) ∈ 𝐽)
67 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → 𝑤𝑍)
68 3simpa 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6968reximi 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
7069ss2abi 3823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))}
71 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℤ𝑀) ∈ V
7264, 71eqeltri 2846 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑍 ∈ V
73 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘 𝑤𝑍
741, 73nfan 1980 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑘(𝜑𝑤𝑍)
75 sdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐴𝑉)
7675adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑤𝑍) → 𝐴𝑉)
77 simpl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → :(𝑀...(𝑘 + 1))⟶𝐴)
78 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...(𝑘 + 1)) ∈ V
79 elmapg 8022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐴𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → ( ∈ (𝐴𝑚 (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
8078, 79mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴𝑉 → ( ∈ (𝐴𝑚 (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
8177, 80syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴𝑉 → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → ∈ (𝐴𝑚 (𝑀...(𝑘 + 1)))))
8281abssdv 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴𝑉 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))))
8376, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))))
84 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴𝑚 (𝑀...(𝑘 + 1))) ∈ V
85 ssexg 4938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({ ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))) ∧ (𝐴𝑚 (𝑀...(𝑘 + 1))) ∈ V) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8683, 84, 85sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8786a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑍) → (𝑘𝑍 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V))
8874, 87ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑍) → ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
89 abrexex2g 7291 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ V ∧ ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
9072, 88, 89sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
91 ssexg 4938 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
9270, 90, 91sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
93 eqeq1 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝐺𝑤) → (𝑥 = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
94933anbi2d 1552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝐺𝑤) → ((:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9594rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝐺𝑤) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9695abbidv 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
9796eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
98 oveq2 6801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺𝑤)))
9998, 96eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ((𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))
10097, 99imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐺𝑤) → (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
101100imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐺𝑤) → ((𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)}))))
102 sdc.11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐹 = (𝑤𝑍, 𝑥𝐽 ↦ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
103102ovmpt4g 6930 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝑍𝑥𝐽 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1041033com12 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐽𝑤𝑍 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1051043exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
106101, 105vtoclga 3423 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) ∈ 𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10766, 67, 92, 106syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
108107, 70syl6eqss 3804 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
109 sdc.15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺𝑤)))
110108, 109sseldd 3753 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
111 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑤 + 1)) ∈ V
112 feq1 6166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → (:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
113 reseq1 5528 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = (𝐺‘(𝑤 + 1)) → ( ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
114113eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → ((𝐺𝑤) = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
115112, 114anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = (𝐺‘(𝑤 + 1)) → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
116115rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝐺‘(𝑤 + 1)) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
117111, 116elab 3501 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
118110, 117sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
119 nfv 1995 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
120 simprl 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
121 fzssp1 12591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
122 fssres 6210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
123120, 121, 122sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
124 fdm 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴 → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
125123, 124syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
126 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
12758, 126fnmpti 6162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)
128 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
129128fneq1d 6121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)))
130127, 129mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
131 fndm 6130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
132130, 131syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
133125, 132eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
134 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘𝑍)
135134, 64syl6eleq 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ𝑀))
136 fzopth 12585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
137135, 136syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
138133, 137mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀 = 𝑀𝑘 = 𝑤))
139138simprd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 = 𝑤)
140139oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
141140oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
142 elfzp1 12598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
143135, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
144133reseq2d 5534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
145 fzssp1 12591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
146 resmpt 5590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
148144, 147syl6req 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
149128, 148eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
150149fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
151 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
152 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
153151, 152eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
154150, 153syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
155140eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
156139, 135eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ𝑀))
157 peano2uz 11943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (ℤ𝑀))
158 eluzfz2 12556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
159 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → (𝐺𝑚) = (𝐺‘(𝑤 + 1)))
160 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
161159, 160fveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 = (𝑤 + 1) → ((𝐺𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))
163 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
164161, 162, 163fvmpt 6424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
165156, 157, 158, 1644syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
166165eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
167 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
168 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
169167, 168eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1))))
170166, 169syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
171155, 170sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
172154, 171jaod 848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
173143, 172sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
174173ralrimiv 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
175 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
176175ad2antrl 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
17758, 162fnmpti 6162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
178 eqfnfv2 6455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
179176, 177, 178sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
180141, 174, 179mpbir2and 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
181180expr 444 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
182 eqeq1 2775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
183182imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
184181, 183syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
185184expimpd 441 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑍) ∧ 𝑘𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
186185ex 397 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝑘𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))))
18774, 119, 186rexlimd 3174 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → (∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
188118, 187mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑍) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
189188expcom 398 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍 → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
19065, 189sylbir 225 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (ℤ𝑀) → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
191190a2d 29 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (ℤ𝑀) → ((𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
19225, 30, 35, 40, 63, 191uzind4 11948 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
193192, 64eleq2s 2868 . . . . . . . . . . . . . . 15 (𝑘𝑍 → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
194193impcom 394 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
195194dmeqd 5464 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
196 dmmptg 5776 . . . . . . . . . . . . . 14 (∀𝑚 ∈ (𝑀...𝑘)((𝐺𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘))
19758a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝑀...𝑘) → ((𝐺𝑚)‘𝑚) ∈ V)
198196, 197mprg 3075 . . . . . . . . . . . . 13 dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘)
199195, 198syl6eq 2821 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = (𝑀...𝑘))
200199eqeq1d 2773 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
201 simpr 471 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑘𝑍)
202201, 64syl6eleq 2860 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
203 fzopth 12585 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
204202, 203syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
205200, 204bitrd 268 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
206 simpr 471 . . . . . . . . . 10 ((𝑀 = 𝑀𝑘 = 𝑛) → 𝑘 = 𝑛)
207205, 206syl6bi 243 . . . . . . . . 9 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
20820, 207syl5 34 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
209 oveq2 6801 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
210209feq2d 6171 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑘)⟶𝐴))
211 sdc.4 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝜓𝜃))
212211sbcbidv 3642 . . . . . . . . . . 11 (𝑛 = 𝑘 → ([(𝐺𝑘) / 𝑔]𝜓[(𝐺𝑘) / 𝑔]𝜃))
213210, 212anbi12d 616 . . . . . . . . . 10 (𝑛 = 𝑘 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
214213equcoms 2105 . . . . . . . . 9 (𝑘 = 𝑛 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
215214biimpcd 239 . . . . . . . 8 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
216208, 215sylcom 30 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
217216rexlimdvw 3182 . . . . . 6 ((𝜑𝑘𝑍) → (∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
21818, 217mpd 15 . . . . 5 ((𝜑𝑘𝑍) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃))
219218simpld 482 . . . 4 ((𝜑𝑘𝑍) → (𝐺𝑘):(𝑀...𝑘)⟶𝐴)
220 eluzfz2 12556 . . . . 5 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
221202, 220syl 17 . . . 4 ((𝜑𝑘𝑍) → 𝑘 ∈ (𝑀...𝑘))
222219, 221ffvelrnd 6503 . . 3 ((𝜑𝑘𝑍) → ((𝐺𝑘)‘𝑘) ∈ 𝐴)
22343cbvmptv 4884 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) = (𝑘𝑍 ↦ ((𝐺𝑘)‘𝑘))
2241, 222, 223fmptdf 6529 . 2 (𝜑 → (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴)
225218simprd 483 . . . . . 6 ((𝜑𝑘𝑍) → [(𝐺𝑘) / 𝑔]𝜃)
226194, 225sbceq1dd 3593 . . . . 5 ((𝜑𝑘𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
227226ex 397 . . . 4 (𝜑 → (𝑘𝑍[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
2281, 227ralrimi 3106 . . 3 (𝜑 → ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
229 mpteq1 4871 . . . . . 6 ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
230 dfsbcq 3589 . . . . . 6 ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
231209, 229, 2303syl 18 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
232211sbcbidv 3642 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
233231, 232bitrd 268 . . . 4 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
234233cbvralv 3320 . . 3 (∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
235228, 234sylibr 224 . 2 (𝜑 → ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)
23672mptex 6630 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ∈ V
237 feq1 6166 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓:𝑍𝐴 ↔ (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴))
238 vex 3354 . . . . . . . 8 𝑓 ∈ V
239238resex 5584 . . . . . . 7 (𝑓 ↾ (𝑀...𝑛)) ∈ V
240 sdc.2 . . . . . . 7 (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓𝜒))
241239, 240sbcie 3622 . . . . . 6 ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓𝜒)
242 reseq1 5528 . . . . . . . 8 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
243 fzssuz 12589 . . . . . . . . . 10 (𝑀...𝑛) ⊆ (ℤ𝑀)
244243, 64sseqtr4i 3787 . . . . . . . . 9 (𝑀...𝑛) ⊆ 𝑍
245 resmpt 5590 . . . . . . . . 9 ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
246244, 245ax-mp 5 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚))
247242, 246syl6eq 2821 . . . . . . 7 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
248247sbceq1d 3592 . . . . . 6 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
249241, 248syl5bbr 274 . . . . 5 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝜒[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
250249ralbidv 3135 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (∀𝑛𝑍 𝜒 ↔ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
251237, 250anbi12d 616 . . 3 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ((𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒) ↔ ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)))
252236, 251spcev 3451 . 2 (((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
253224, 235, 252syl2anc 573 1 (𝜑 → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 836  w3a 1071   = wceq 1631  wex 1852  wnf 1856  wcel 2145  {cab 2757  wral 3061  wrex 3062  Vcvv 3351  [wsbc 3587  wss 3723  {csn 4316  cmpt 4863  dom cdm 5249  cres 5251   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  cmpt2 6795  𝑚 cmap 8009  1c1 10139   + caddc 10141  cz 11579  cuz 11888  ...cfz 12533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534
This theorem is referenced by:  sdclem1  33871
  Copyright terms: Public domain W3C validator