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

Theorem sdclem2 32708
 Description: Lemma for sdc 32710. (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 6267 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐽)
4 sdc.10 . . . . . . . . 9 𝐽 = {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)}
54eleq2i 2680 . . . . . . . 8 ((𝐺𝑘) ∈ 𝐽 ↔ (𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)})
6 nfcv 2751 . . . . . . . . . 10 𝑔𝑍
7 nfv 1830 . . . . . . . . . . 11 𝑔(𝐺𝑘):(𝑀...𝑛)⟶𝐴
8 nfsbc1v 3422 . . . . . . . . . . 11 𝑔[(𝐺𝑘) / 𝑔]𝜓
97, 8nfan 1816 . . . . . . . . . 10 𝑔((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
106, 9nfrex 2990 . . . . . . . . 9 𝑔𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)
11 fvex 6113 . . . . . . . . 9 (𝐺𝑘) ∈ V
12 feq1 5939 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑛)⟶𝐴))
13 sbceq1a 3413 . . . . . . . . . . 11 (𝑔 = (𝐺𝑘) → (𝜓[(𝐺𝑘) / 𝑔]𝜓))
1412, 13anbi12d 743 . . . . . . . . . 10 (𝑔 = (𝐺𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1514rexbidv 3034 . . . . . . . . 9 (𝑔 = (𝐺𝑘) → (∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓) ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓)))
1610, 11, 15elabf 3318 . . . . . . . 8 ((𝐺𝑘) ∈ {𝑔 ∣ ∃𝑛𝑍 (𝑔:(𝑀...𝑛)⟶𝐴𝜓)} ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
175, 16bitri 263 . . . . . . 7 ((𝐺𝑘) ∈ 𝐽 ↔ ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
183, 17sylib 207 . . . . . 6 ((𝜑𝑘𝑍) → ∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓))
19 fdm 5964 . . . . . . . . . 10 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺𝑘) = (𝑀...𝑛))
2019adantr 480 . . . . . . . . 9 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → dom (𝐺𝑘) = (𝑀...𝑛))
21 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝐺𝑥) = (𝐺𝑀))
22 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀))
2322mpteq1d 4666 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
2421, 23eqeq12d 2625 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑀 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
2524imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑀 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))))
26 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
27 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤))
2827mpteq1d 4666 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
2926, 28eqeq12d 2625 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
3029imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))))
31 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝐺𝑥) = (𝐺‘(𝑤 + 1)))
32 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1)))
3332mpteq1d 4666 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
3431, 33eqeq12d 2625 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑤 + 1) → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
3534imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
36 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝐺𝑥) = (𝐺𝑘))
37 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘))
3837mpteq1d 4666 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
3936, 38eqeq12d 2625 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → ((𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚)) ↔ (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
4039imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → ((𝜑 → (𝐺𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺𝑚)‘𝑚))) ↔ (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))))
41 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
42 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘𝑚 = 𝑘)
4341, 42fveq12d 6109 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑘 → ((𝐺𝑚)‘𝑚) = ((𝐺𝑘)‘𝑘))
44 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))
45 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘)‘𝑘) ∈ V
4643, 44, 45fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
4746adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘) = ((𝐺𝑘)‘𝑘))
48 elfz1eq 12223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
4948adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀)
5049fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (𝑀...𝑀)) → (𝐺𝑘) = (𝐺𝑀))
5150fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑘)‘𝑘) = ((𝐺𝑀)‘𝑘))
5247, 51eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (𝑀...𝑀)) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
5352ex 449 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
541, 53ralrimi 2940 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘))
55 sdc.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺𝑀):(𝑀...𝑀)⟶𝐴)
56 ffn 5958 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑀):(𝑀...𝑀)⟶𝐴 → (𝐺𝑀) Fn (𝑀...𝑀))
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑀) Fn (𝑀...𝑀))
58 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑚)‘𝑚) ∈ V
5958, 44fnmpti 5935 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)
60 eqfnfv 6219 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6157, 59, 60sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))‘𝑘)))
6254, 61mpbird 246 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚)))
6362a1i 11 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → (𝜑 → (𝐺𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺𝑚)‘𝑚))))
64 sdc.1 . . . . . . . . . . . . . . . . . . . 20 𝑍 = (ℤ𝑀)
6564eleq2i 2680 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍𝑤 ∈ (ℤ𝑀))
662ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → (𝐺𝑤) ∈ 𝐽)
67 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → 𝑤𝑍)
68 3simpa 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
6968reximi 2994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
7069ss2abi 3637 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))}
71 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℤ𝑀) ∈ V
7264, 71eqeltri 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑍 ∈ V
73 nfv 1830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘 𝑤𝑍
741, 73nfan 1816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑘(𝜑𝑤𝑍)
75 sdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝐴𝑉)
7675adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑤𝑍) → 𝐴𝑉)
77 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → :(𝑀...(𝑘 + 1))⟶𝐴)
78 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...(𝑘 + 1)) ∈ V
79 elmapg 7757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐴𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → ( ∈ (𝐴𝑚 (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
8078, 79mpan2 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴𝑉 → ( ∈ (𝐴𝑚 (𝑀...(𝑘 + 1))) ↔ :(𝑀...(𝑘 + 1))⟶𝐴))
8177, 80syl5ibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐴𝑉 → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) → ∈ (𝐴𝑚 (𝑀...(𝑘 + 1)))))
8281abssdv 3639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴𝑉 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))))
8376, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))))
84 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐴𝑚 (𝑀...(𝑘 + 1))) ∈ V
85 ssexg 4732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({ ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ⊆ (𝐴𝑚 (𝑀...(𝑘 + 1))) ∧ (𝐴𝑚 (𝑀...(𝑘 + 1))) ∈ V) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8683, 84, 85sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑤𝑍) → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
8786a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑍) → (𝑘𝑍 → { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V))
8874, 87ralrimi 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑍) → ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
89 abrexex2g 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ V ∧ ∀𝑘𝑍 { ∣ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
9072, 88, 89sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V)
91 ssexg 4732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ∈ V) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
9270, 90, 91sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑍) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)
93 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝐺𝑤) → (𝑥 = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ( ↾ (𝑀...𝑘))))
94933anbi2d 1396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝐺𝑤) → ((:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9594rexbidv 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝐺𝑤) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)))
9695abbidv 2728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
9796eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐺𝑤) → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V))
98 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐺𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺𝑤)))
9998, 96eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝑍𝑥𝐽 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1041033com12 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐽𝑤𝑍 ∧ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
1051043exp 1256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴𝑥 = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
106101, 105vtoclga 3245 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) ∈ 𝐽 → (𝑤𝑍 → ({ ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})))
10766, 67, 92, 106syl3c 64 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) = { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)) ∧ 𝜎)})
108107, 70syl6eqss 3618 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝑤𝐹(𝐺𝑤)) ⊆ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
109 sdc.15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺𝑤)))
110108, 109sseldd 3569 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))})
111 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(𝑤 + 1)) ∈ V
112 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → (:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴))
113 reseq1 5311 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( = (𝐺‘(𝑤 + 1)) → ( ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))
114113eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( = (𝐺‘(𝑤 + 1)) → ((𝐺𝑤) = ( ↾ (𝑀...𝑘)) ↔ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
115112, 114anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . 24 ( = (𝐺‘(𝑤 + 1)) → ((:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
116115rexbidv 3034 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝐺‘(𝑤 + 1)) → (∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘))) ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))))
117111, 116elab 3319 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺‘(𝑤 + 1)) ∈ { ∣ ∃𝑘𝑍 (:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ( ↾ (𝑀...𝑘)))} ↔ ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
118110, 117sylib 207 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → ∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))
119 nfv 1830 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
120 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)
121 fzssp1 12255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))
122 fssres 5983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
123120, 121, 122sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴)
124 fdm 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴 → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
125123, 124syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘))
126 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
12758, 126fnmpti 5935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)
128 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
129128fneq1d 5895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...𝑤)))
130127, 129mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤))
131 fndm 5904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
132130, 131syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤))
133125, 132eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤))
134 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘𝑍)
135134, 64syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ𝑀))
136 fzopth 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
137135, 136syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀𝑘 = 𝑤)))
138133, 137mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀 = 𝑀𝑘 = 𝑤))
139138simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑘 = 𝑤)
140139oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1))
141140oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)))
142 elfzp1 12261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
143135, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1))))
144133reseq2d 5317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)))
145 fzssp1 12255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1))
146 resmpt 5369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))
148144, 147syl6req 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
149128, 148eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘)))
150149fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥))
151 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥))
152 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
153151, 152eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
154150, 153syl5ibcom 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
155140eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1)))
156139, 135eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ𝑀))
157 peano2uz 11617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (ℤ𝑀))
158 eluzfz2 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (ℤ𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1)))
159 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → (𝐺𝑚) = (𝐺‘(𝑤 + 1)))
160 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1))
161159, 160fveq12d 6109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 = (𝑤 + 1) → ((𝐺𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
162 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))
163 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V
164161, 162, 163fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
165156, 157, 158, 1644syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
166165eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
167 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)))
168 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1)))
169167, 168eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘(𝑤 + 1))))
170166, 169syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
171155, 170sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
172154, 171jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
173143, 172sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥)))
174173ralrimiv 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))
175 ffn 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
176175ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)))
17758, 162fnmpti 5935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))
178 eqfnfv2 6220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
179176, 177, 178sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))‘𝑥))))
180141, 174, 179mpbir2and 959 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))
181180expr 641 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
182 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))))
183182imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
184181, 183syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤𝑍) ∧ 𝑘𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
185184expimpd 627 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑍) ∧ 𝑘𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
186185ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑍) → (𝑘𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))))
18774, 119, 186rexlimd 3008 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑍) → (∃𝑘𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
188118, 187mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑍) → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚))))
189188expcom 450 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑍 → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
19065, 189sylbir 224 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (ℤ𝑀) → (𝜑 → ((𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
191190a2d 29 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (ℤ𝑀) → ((𝜑 → (𝐺𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺𝑚)‘𝑚)))))
19225, 30, 35, 40, 63, 191uzind4 11622 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
193192, 64eleq2s 2706 . . . . . . . . . . . . . . 15 (𝑘𝑍 → (𝜑 → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚))))
194193impcom 445 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
195194dmeqd 5248 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
196 dmmptg 5549 . . . . . . . . . . . . . 14 (∀𝑚 ∈ (𝑀...𝑘)((𝐺𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘))
19758a1i 11 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝑀...𝑘) → ((𝐺𝑚)‘𝑚) ∈ V)
198196, 197mprg 2910 . . . . . . . . . . . . 13 dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) = (𝑀...𝑘)
199195, 198syl6eq 2660 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → dom (𝐺𝑘) = (𝑀...𝑘))
200199eqeq1d 2612 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛)))
201 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑘𝑍)
202201, 64syl6eleq 2698 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ (ℤ𝑀))
203 fzopth 12249 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
204202, 203syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
205200, 204bitrd 267 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀𝑘 = 𝑛)))
206 simpr 476 . . . . . . . . . 10 ((𝑀 = 𝑀𝑘 = 𝑛) → 𝑘 = 𝑛)
207205, 206syl6bi 242 . . . . . . . . 9 ((𝜑𝑘𝑍) → (dom (𝐺𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛))
20820, 207syl5 33 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛))
209 oveq2 6557 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
210209feq2d 5944 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐺𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺𝑘):(𝑀...𝑘)⟶𝐴))
211 sdc.4 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝜓𝜃))
212211sbcbidv 3457 . . . . . . . . . . 11 (𝑛 = 𝑘 → ([(𝐺𝑘) / 𝑔]𝜓[(𝐺𝑘) / 𝑔]𝜃))
213210, 212anbi12d 743 . . . . . . . . . 10 (𝑛 = 𝑘 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
214213equcoms 1934 . . . . . . . . 9 (𝑘 = 𝑛 → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) ↔ ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
215214biimpcd 238 . . . . . . . 8 (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
216208, 215sylcom 30 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
217216rexlimdvw 3016 . . . . . 6 ((𝜑𝑘𝑍) → (∃𝑛𝑍 ((𝐺𝑘):(𝑀...𝑛)⟶𝐴[(𝐺𝑘) / 𝑔]𝜓) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃)))
21818, 217mpd 15 . . . . 5 ((𝜑𝑘𝑍) → ((𝐺𝑘):(𝑀...𝑘)⟶𝐴[(𝐺𝑘) / 𝑔]𝜃))
219218simpld 474 . . . 4 ((𝜑𝑘𝑍) → (𝐺𝑘):(𝑀...𝑘)⟶𝐴)
220 eluzfz2 12220 . . . . 5 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
221202, 220syl 17 . . . 4 ((𝜑𝑘𝑍) → 𝑘 ∈ (𝑀...𝑘))
222219, 221ffvelrnd 6268 . . 3 ((𝜑𝑘𝑍) → ((𝐺𝑘)‘𝑘) ∈ 𝐴)
22343cbvmptv 4678 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) = (𝑘𝑍 ↦ ((𝐺𝑘)‘𝑘))
2241, 222, 223fmptdf 6294 . 2 (𝜑 → (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴)
225218simprd 478 . . . . . 6 ((𝜑𝑘𝑍) → [(𝐺𝑘) / 𝑔]𝜃)
226194, 225sbceq1dd 3408 . . . . 5 ((𝜑𝑘𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
227226ex 449 . . . 4 (𝜑 → (𝑘𝑍[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
2281, 227ralrimi 2940 . . 3 (𝜑 → ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
229 mpteq1 4665 . . . . . 6 ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)))
230 dfsbcq 3404 . . . . . 6 ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
231209, 229, 2303syl 18 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
232211sbcbidv 3457 . . . . 5 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
233231, 232bitrd 267 . . . 4 (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃))
234233cbvralv 3147 . . 3 (∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜃)
235228, 234sylibr 223 . 2 (𝜑 → ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)
23672mptex 6390 . . 3 (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ∈ V
237 feq1 5939 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓:𝑍𝐴 ↔ (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴))
238 vex 3176 . . . . . . . 8 𝑓 ∈ V
239238resex 5363 . . . . . . 7 (𝑓 ↾ (𝑀...𝑛)) ∈ V
240 sdc.2 . . . . . . 7 (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓𝜒))
241239, 240sbcie 3437 . . . . . 6 ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓𝜒)
242 reseq1 5311 . . . . . . . 8 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)))
243 fzssuz 12253 . . . . . . . . . 10 (𝑀...𝑛) ⊆ (ℤ𝑀)
244243, 64sseqtr4i 3601 . . . . . . . . 9 (𝑀...𝑛) ⊆ 𝑍
245 resmpt 5369 . . . . . . . . 9 ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
246244, 245ax-mp 5 . . . . . . . 8 ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚))
247242, 246syl6eq 2660 . . . . . . 7 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)))
248247sbceq1d 3407 . . . . . 6 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
249241, 248syl5bbr 273 . . . . 5 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (𝜒[(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
250249ralbidv 2969 . . . 4 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → (∀𝑛𝑍 𝜒 ↔ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓))
251237, 250anbi12d 743 . . 3 (𝑓 = (𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)) → ((𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒) ↔ ((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓)))
252236, 251spcev 3273 . 2 (((𝑚𝑍 ↦ ((𝐺𝑚)‘𝑚)):𝑍𝐴 ∧ ∀𝑛𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
253224, 235, 252syl2anc 691 1 (𝜑 → ∃𝑓(𝑓:𝑍𝐴 ∧ ∀𝑛𝑍 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  Vcvv 3173  [wsbc 3402   ⊆ wss 3540  {csn 4125   ↦ cmpt 4643  dom cdm 5038   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑𝑚 cmap 7744  1c1 9816   + caddc 9818  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198 This theorem is referenced by:  sdclem1  32709
 Copyright terms: Public domain W3C validator