Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmvlelem3 Structured version   Visualization version   GIF version

Theorem hoidmvlelem3 41331
Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem3.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hoidmvlelem3.x (𝜑𝑋 ∈ Fin)
hoidmvlelem3.y (𝜑𝑌𝑋)
hoidmvlelem3.z (𝜑𝑍 ∈ (𝑋𝑌))
hoidmvlelem3.w 𝑊 = (𝑌 ∪ {𝑍})
hoidmvlelem3.a (𝜑𝐴:𝑊⟶ℝ)
hoidmvlelem3.b (𝜑𝐵:𝑊⟶ℝ)
hoidmvlelem3.lt ((𝜑𝑘𝑊) → (𝐴𝑘) < (𝐵𝑘))
hoidmvlelem3.f 𝐹 = (𝑦𝑌 ↦ 0)
hoidmvlelem3.c (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
hoidmvlelem3.j 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
hoidmvlelem3.d (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
hoidmvlelem3.k 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
hoidmvlelem3.r (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
hoidmvlelem3.h 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
hoidmvlelem3.g 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
hoidmvlelem3.e (𝜑𝐸 ∈ ℝ+)
hoidmvlelem3.u 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
hoidmvlelem3.s (𝜑𝑆𝑈)
hoidmvlelem3.sb (𝜑𝑆 < (𝐵𝑍))
hoidmvlelem3.p 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
hoidmvlelem3.i (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
hoidmvlelem3.i2 (𝜑X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
hoidmvlelem3.o 𝑂 = (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ↦ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
Assertion
Ref Expression
hoidmvlelem3 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Distinct variable groups:   𝐴,𝑎,𝑏,,𝑗,𝑘,𝑥   𝐴,𝑒,𝑓,𝑔,,𝑗,𝑘   𝑧,𝐴,,𝑗   𝐵,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝐵,𝑐,,𝑗,𝑘,𝑥   𝐵,𝑓,𝑔   𝑢,𝐵,,𝑗   𝑧,𝐵   𝐶,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝐶,𝑐   𝑢,𝐶   𝑧,𝐶   𝐷,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝐷,𝑐   𝑢,𝐷   𝑧,𝐷   𝐸,𝑎,𝑏,,𝑘,𝑥,𝑦   𝐸,𝑐   𝑧,𝐸   𝑗,𝐹   𝐺,𝑎,𝑏,,𝑘,𝑥,𝑦   𝐺,𝑐   𝑧,𝐺   𝐻,𝑎,𝑏,𝑗,𝑘   𝑧,𝐻   𝐽,𝑎,𝑏,,𝑗,𝑘,𝑥   𝑔,𝐽   𝐾,𝑎,𝑏,,𝑗,𝑘,𝑥   𝐿,𝑎,𝑏,,𝑗,𝑘,𝑥   𝑒,𝐿,𝑓,𝑔   𝑧,𝐿   𝑗,𝑂,𝑘   𝑃,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝑃,𝑐   𝑆,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝑆,𝑐   𝑢,𝑆   𝑧,𝑆   𝑢,𝑈   𝑊,𝑎,𝑏,𝑗,𝑘,𝑥   𝑊,𝑐   𝑧,𝑊   𝑌,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝑌,𝑐   𝑒,𝑌,𝑓,𝑔   𝑍,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝑍,𝑐   𝑢,𝑍   𝑧,𝑍   𝜑,𝑎,𝑏,,𝑗,𝑘,𝑥,𝑦   𝜑,𝑐
Allowed substitution hints:   𝜑(𝑧,𝑢,𝑒,𝑓,𝑔)   𝐴(𝑦,𝑢,𝑐)   𝐵(𝑒)   𝐶(𝑒,𝑓,𝑔)   𝐷(𝑒,𝑓,𝑔)   𝑃(𝑧,𝑢,𝑒,𝑓,𝑔)   𝑆(𝑒,𝑓,𝑔)   𝑈(𝑥,𝑦,𝑧,𝑒,𝑓,𝑔,,𝑗,𝑘,𝑎,𝑏,𝑐)   𝐸(𝑢,𝑒,𝑓,𝑔,𝑗)   𝐹(𝑥,𝑦,𝑧,𝑢,𝑒,𝑓,𝑔,,𝑘,𝑎,𝑏,𝑐)   𝐺(𝑢,𝑒,𝑓,𝑔,𝑗)   𝐻(𝑥,𝑦,𝑢,𝑒,𝑓,𝑔,,𝑐)   𝐽(𝑦,𝑧,𝑢,𝑒,𝑓,𝑐)   𝐾(𝑦,𝑧,𝑢,𝑒,𝑓,𝑔,𝑐)   𝐿(𝑦,𝑢,𝑐)   𝑂(𝑥,𝑦,𝑧,𝑢,𝑒,𝑓,𝑔,,𝑎,𝑏,𝑐)   𝑊(𝑦,𝑢,𝑒,𝑓,𝑔,)   𝑋(𝑥,𝑦,𝑧,𝑢,𝑒,𝑓,𝑔,,𝑗,𝑘,𝑎,𝑏,𝑐)   𝑌(𝑧,𝑢)   𝑍(𝑒,𝑓,𝑔)

Proof of Theorem hoidmvlelem3
Dummy variables 𝑖 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 11233 . . . . 5 1 ∈ ℕ
21a1i 11 . . . 4 ((𝜑𝑌 = ∅) → 1 ∈ ℕ)
3 0le0 11312 . . . . . 6 0 ≤ 0
43a1i 11 . . . . 5 ((𝜑𝑌 = ∅) → 0 ≤ 0)
5 hoidmvlelem3.g . . . . . . . 8 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
65a1i 11 . . . . . . 7 ((𝜑𝑌 = ∅) → 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
7 fveq2 6332 . . . . . . . . 9 (𝑌 = ∅ → (𝐿𝑌) = (𝐿‘∅))
8 reseq2 5529 . . . . . . . . . 10 (𝑌 = ∅ → (𝐴𝑌) = (𝐴 ↾ ∅))
9 res0 5538 . . . . . . . . . . 11 (𝐴 ↾ ∅) = ∅
109a1i 11 . . . . . . . . . 10 (𝑌 = ∅ → (𝐴 ↾ ∅) = ∅)
118, 10eqtrd 2805 . . . . . . . . 9 (𝑌 = ∅ → (𝐴𝑌) = ∅)
12 reseq2 5529 . . . . . . . . . 10 (𝑌 = ∅ → (𝐵𝑌) = (𝐵 ↾ ∅))
13 res0 5538 . . . . . . . . . . 11 (𝐵 ↾ ∅) = ∅
1413a1i 11 . . . . . . . . . 10 (𝑌 = ∅ → (𝐵 ↾ ∅) = ∅)
1512, 14eqtrd 2805 . . . . . . . . 9 (𝑌 = ∅ → (𝐵𝑌) = ∅)
167, 11, 15oveq123d 6814 . . . . . . . 8 (𝑌 = ∅ → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = (∅(𝐿‘∅)∅))
1716adantl 467 . . . . . . 7 ((𝜑𝑌 = ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = (∅(𝐿‘∅)∅))
18 hoidmvlelem3.l . . . . . . . 8 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
19 f0 6226 . . . . . . . . 9 ∅:∅⟶ℝ
2019a1i 11 . . . . . . . 8 ((𝜑𝑌 = ∅) → ∅:∅⟶ℝ)
2118, 20, 20hoidmv0val 41317 . . . . . . 7 ((𝜑𝑌 = ∅) → (∅(𝐿‘∅)∅) = 0)
226, 17, 213eqtrd 2809 . . . . . 6 ((𝜑𝑌 = ∅) → 𝐺 = 0)
23 nfcvd 2914 . . . . . . . . . . 11 (𝜑𝑗(𝑃‘1))
24 nfv 1995 . . . . . . . . . . 11 𝑗𝜑
25 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑗 = 1) → 𝑗 = 1)
2625fveq2d 6336 . . . . . . . . . . 11 ((𝜑𝑗 = 1) → (𝑃𝑗) = (𝑃‘1))
27 1red 10257 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
28 rge0ssre 12487 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
29 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
301a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℕ)
311elexi 3365 . . . . . . . . . . . . . . 15 1 ∈ V
32 eleq1 2838 . . . . . . . . . . . . . . . . 17 (𝑗 = 1 → (𝑗 ∈ ℕ ↔ 1 ∈ ℕ))
3332anbi2d 614 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑 ∧ 1 ∈ ℕ)))
34 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑗 = 1 → (𝑃𝑗) = (𝑃‘1))
3534eleq1d 2835 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝑃𝑗) ∈ (0[,)+∞) ↔ (𝑃‘1) ∈ (0[,)+∞)))
3633, 35imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝑃‘1) ∈ (0[,)+∞))))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
38 ovexd 6825 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ V)
39 hoidmvlelem3.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4039fvmpt2 6433 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ V) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4137, 38, 40syl2anc 573 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4241adantl 467 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
43 hoidmvlelem3.x . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋 ∈ Fin)
44 hoidmvlelem3.w . . . . . . . . . . . . . . . . . . . . . 22 𝑊 = (𝑌 ∪ {𝑍})
4544a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑊 = (𝑌 ∪ {𝑍}))
46 hoidmvlelem3.y . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌𝑋)
47 hoidmvlelem3.z . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑍 ∈ (𝑋𝑌))
4847eldifad 3735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑍𝑋)
49 snssi 4474 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍𝑋 → {𝑍} ⊆ 𝑋)
5048, 49syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑍} ⊆ 𝑋)
5146, 50unssd 3940 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑌 ∪ {𝑍}) ⊆ 𝑋)
5245, 51eqsstrd 3788 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑊𝑋)
5343, 52ssfid 8339 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊 ∈ Fin)
54 ssun1 3927 . . . . . . . . . . . . . . . . . . . . 21 𝑌 ⊆ (𝑌 ∪ {𝑍})
5544eqcomi 2780 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 ∪ {𝑍}) = 𝑊
5654, 55sseqtri 3786 . . . . . . . . . . . . . . . . . . . 20 𝑌𝑊
5756a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌𝑊)
5853, 57ssfid 8339 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌 ∈ Fin)
5958adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ Fin)
60 iftrue 4231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
6160adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
62 hoidmvlelem3.c . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
6362ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊))
64 elmapi 8031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
6654, 44sseqtr4i 3787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑌𝑊
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → 𝑌𝑊)
6865, 67fssresd 6211 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ)
69 reex 10229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ∈ V
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → ℝ ∈ V)
7153, 57ssexd 4939 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ∈ V)
7271adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ V)
7370, 72elmapd 8023 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ))
7468, 73mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
7574adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
7661, 75eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
77 iffalse 4234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = 𝐹)
7877adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = 𝐹)
79 0red 10243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑌) → 0 ∈ ℝ)
80 hoidmvlelem3.f . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐹 = (𝑦𝑌 ↦ 0)
8179, 80fmptd 6527 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝑌⟶ℝ)
8269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ℝ ∈ V)
8382, 58elmapd 8023 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ (ℝ ↑𝑚 𝑌) ↔ 𝐹:𝑌⟶ℝ))
8481, 83mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ (ℝ ↑𝑚 𝑌))
8584ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹 ∈ (ℝ ↑𝑚 𝑌))
8678, 85eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
8776, 86pm2.61dan 814 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
88 hoidmvlelem3.j . . . . . . . . . . . . . . . . . . . 20 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
8987, 88fmptd 6527 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐽:ℕ⟶(ℝ ↑𝑚 𝑌))
9089ffvelrnda 6502 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) ∈ (ℝ ↑𝑚 𝑌))
91 elmapi 8031 . . . . . . . . . . . . . . . . . 18 ((𝐽𝑗) ∈ (ℝ ↑𝑚 𝑌) → (𝐽𝑗):𝑌⟶ℝ)
9290, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ)
93 iftrue 4231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
9493adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
95 hoidmvlelem3.d . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
9695ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊))
97 elmapi 8031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
9998, 67fssresd 6211 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗) ↾ 𝑌):𝑌⟶ℝ)
10070, 72elmapd 8023 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ ((𝐷𝑗) ↾ 𝑌):𝑌⟶ℝ))
10199, 100mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
102101adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
10394, 102eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
104 iffalse 4234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = 𝐹)
105104adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = 𝐹)
106105, 85eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
107103, 106pm2.61dan 814 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
108 hoidmvlelem3.k . . . . . . . . . . . . . . . . . . . 20 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
109107, 108fmptd 6527 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶(ℝ ↑𝑚 𝑌))
110109ffvelrnda 6502 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) ∈ (ℝ ↑𝑚 𝑌))
111 elmapi 8031 . . . . . . . . . . . . . . . . . 18 ((𝐾𝑗) ∈ (ℝ ↑𝑚 𝑌) → (𝐾𝑗):𝑌⟶ℝ)
112110, 111syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗):𝑌⟶ℝ)
11318, 59, 92, 112hoidmvcl 41316 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ (0[,)+∞))
11442, 113eqeltrd 2850 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞))
11531, 36, 114vtocl 3410 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝑃‘1) ∈ (0[,)+∞))
11629, 30, 115syl2anc 573 . . . . . . . . . . . . 13 (𝜑 → (𝑃‘1) ∈ (0[,)+∞))
11728, 116sseldi 3750 . . . . . . . . . . . 12 (𝜑 → (𝑃‘1) ∈ ℝ)
118117recnd 10270 . . . . . . . . . . 11 (𝜑 → (𝑃‘1) ∈ ℂ)
11923, 24, 26, 27, 118sumsnd 39707 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ {1} (𝑃𝑗) = (𝑃‘1))
120119adantr 466 . . . . . . . . 9 ((𝜑𝑌 = ∅) → Σ𝑗 ∈ {1} (𝑃𝑗) = (𝑃‘1))
121 fveq2 6332 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐽𝑗) = (𝐽‘1))
122 fveq2 6332 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐾𝑗) = (𝐾‘1))
123121, 122oveq12d 6811 . . . . . . . . . . . 12 (𝑗 = 1 → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
124 ovex 6823 . . . . . . . . . . . 12 ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) ∈ V
125123, 39, 124fvmpt 6424 . . . . . . . . . . 11 (1 ∈ ℕ → (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
1261, 125ax-mp 5 . . . . . . . . . 10 (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1))
127126a1i 11 . . . . . . . . 9 ((𝜑𝑌 = ∅) → (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
1287oveqd 6810 . . . . . . . . . . 11 (𝑌 = ∅ → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = ((𝐽‘1)(𝐿‘∅)(𝐾‘1)))
129128adantl 467 . . . . . . . . . 10 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = ((𝐽‘1)(𝐿‘∅)(𝐾‘1)))
130121feq1d 6170 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝐽𝑗):𝑌⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
13133, 130imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝐽‘1):𝑌⟶ℝ)))
13268adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ)
13361feq1d 6170 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ))
134132, 133mpbird 247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
13581ad2antrr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹:𝑌⟶ℝ)
13678feq1d 6170 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ))
137135, 136mpbird 247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
138134, 137pm2.61dan 814 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
139 simpr 471 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
140 fvex 6342 . . . . . . . . . . . . . . . . . . . . 21 (𝐶𝑗) ∈ V
141140resex 5584 . . . . . . . . . . . . . . . . . . . 20 ((𝐶𝑗) ↾ 𝑌) ∈ V
14261, 141syl6eqel 2858 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
14384elexd 3366 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 ∈ V)
144143adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → 𝐹 ∈ V)
145144adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹 ∈ V)
14678, 145eqeltrd 2850 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
147142, 146pm2.61dan 814 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
14888fvmpt2 6433 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
149139, 147, 148syl2anc 573 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
150149feq1d 6170 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐽𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ))
151138, 150mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ)
15231, 131, 151vtocl 3410 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝐽‘1):𝑌⟶ℝ)
15329, 30, 152syl2anc 573 . . . . . . . . . . . . 13 (𝜑 → (𝐽‘1):𝑌⟶ℝ)
154153adantr 466 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → (𝐽‘1):𝑌⟶ℝ)
155 id 22 . . . . . . . . . . . . . . 15 (𝑌 = ∅ → 𝑌 = ∅)
156155eqcomd 2777 . . . . . . . . . . . . . 14 (𝑌 = ∅ → ∅ = 𝑌)
157156feq2d 6171 . . . . . . . . . . . . 13 (𝑌 = ∅ → ((𝐽‘1):∅⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
158157adantl 467 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → ((𝐽‘1):∅⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
159154, 158mpbird 247 . . . . . . . . . . 11 ((𝜑𝑌 = ∅) → (𝐽‘1):∅⟶ℝ)
160122feq1d 6170 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝐾𝑗):𝑌⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
16133, 160imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝐾𝑗):𝑌⟶ℝ) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝐾‘1):𝑌⟶ℝ)))
16231, 161, 112vtocl 3410 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝐾‘1):𝑌⟶ℝ)
16329, 30, 162syl2anc 573 . . . . . . . . . . . . 13 (𝜑 → (𝐾‘1):𝑌⟶ℝ)
164163adantr 466 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → (𝐾‘1):𝑌⟶ℝ)
165156feq2d 6171 . . . . . . . . . . . . 13 (𝑌 = ∅ → ((𝐾‘1):∅⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
166165adantl 467 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → ((𝐾‘1):∅⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
167164, 166mpbird 247 . . . . . . . . . . 11 ((𝜑𝑌 = ∅) → (𝐾‘1):∅⟶ℝ)
16818, 159, 167hoidmv0val 41317 . . . . . . . . . 10 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿‘∅)(𝐾‘1)) = 0)
169129, 168eqtrd 2805 . . . . . . . . 9 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = 0)
170120, 127, 1693eqtrd 2809 . . . . . . . 8 ((𝜑𝑌 = ∅) → Σ𝑗 ∈ {1} (𝑃𝑗) = 0)
171170oveq2d 6809 . . . . . . 7 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) = ((1 + 𝐸) · 0))
172 hoidmvlelem3.e . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ+)
173172rpred 12075 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
17427, 173readdcld 10271 . . . . . . . . . 10 (𝜑 → (1 + 𝐸) ∈ ℝ)
175174recnd 10270 . . . . . . . . 9 (𝜑 → (1 + 𝐸) ∈ ℂ)
176175mul01d 10437 . . . . . . . 8 (𝜑 → ((1 + 𝐸) · 0) = 0)
177176adantr 466 . . . . . . 7 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · 0) = 0)
178 eqidd 2772 . . . . . . 7 ((𝜑𝑌 = ∅) → 0 = 0)
179171, 177, 1783eqtrd 2809 . . . . . 6 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) = 0)
18022, 179breq12d 4799 . . . . 5 ((𝜑𝑌 = ∅) → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) ↔ 0 ≤ 0))
1814, 180mpbird 247 . . . 4 ((𝜑𝑌 = ∅) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)))
182 oveq2 6801 . . . . . . . . 9 (𝑚 = 1 → (1...𝑚) = (1...1))
1831nnzi 11603 . . . . . . . . . . 11 1 ∈ ℤ
184 fzsn 12590 . . . . . . . . . . 11 (1 ∈ ℤ → (1...1) = {1})
185183, 184ax-mp 5 . . . . . . . . . 10 (1...1) = {1}
186185a1i 11 . . . . . . . . 9 (𝑚 = 1 → (1...1) = {1})
187182, 186eqtrd 2805 . . . . . . . 8 (𝑚 = 1 → (1...𝑚) = {1})
188187sumeq1d 14639 . . . . . . 7 (𝑚 = 1 → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) = Σ𝑗 ∈ {1} (𝑃𝑗))
189188oveq2d 6809 . . . . . 6 (𝑚 = 1 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)))
190189breq2d 4798 . . . . 5 (𝑚 = 1 → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) ↔ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗))))
191190rspcev 3460 . . . 4 ((1 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗))) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
1922, 181, 191syl2anc 573 . . 3 ((𝜑𝑌 = ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
193 simpl 468 . . . 4 ((𝜑 ∧ ¬ 𝑌 = ∅) → 𝜑)
194 neqne 2951 . . . . 5 𝑌 = ∅ → 𝑌 ≠ ∅)
195194adantl 467 . . . 4 ((𝜑 ∧ ¬ 𝑌 = ∅) → 𝑌 ≠ ∅)
196 nfv 1995 . . . . . 6 𝑗(𝜑𝑌 ≠ ∅)
197183a1i 11 . . . . . 6 ((𝜑𝑌 ≠ ∅) → 1 ∈ ℤ)
198 nnuz 11925 . . . . . 6 ℕ = (ℤ‘1)
199114adantlr 694 . . . . . 6 (((𝜑𝑌 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞))
200 hoidmvlelem3.a . . . . . . . . . . . 12 (𝜑𝐴:𝑊⟶ℝ)
20166a1i 11 . . . . . . . . . . . 12 (𝜑𝑌𝑊)
202200, 201fssresd 6211 . . . . . . . . . . 11 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
203 hoidmvlelem3.b . . . . . . . . . . . 12 (𝜑𝐵:𝑊⟶ℝ)
204203, 201fssresd 6211 . . . . . . . . . . 11 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
20518, 58, 202, 204hoidmvcl 41316 . . . . . . . . . 10 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
20628, 205sseldi 3750 . . . . . . . . 9 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ ℝ)
2075, 206syl5eqel 2854 . . . . . . . 8 (𝜑𝐺 ∈ ℝ)
208 0red 10243 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
209 1rp 12039 . . . . . . . . . . . . 13 1 ∈ ℝ+
210209a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ+)
211210, 172jca 501 . . . . . . . . . . 11 (𝜑 → (1 ∈ ℝ+𝐸 ∈ ℝ+))
212 rpaddcl 12057 . . . . . . . . . . 11 ((1 ∈ ℝ+𝐸 ∈ ℝ+) → (1 + 𝐸) ∈ ℝ+)
213211, 212syl 17 . . . . . . . . . 10 (𝜑 → (1 + 𝐸) ∈ ℝ+)
214 rpgt0 12047 . . . . . . . . . 10 ((1 + 𝐸) ∈ ℝ+ → 0 < (1 + 𝐸))
215213, 214syl 17 . . . . . . . . 9 (𝜑 → 0 < (1 + 𝐸))
216208, 215gtned 10374 . . . . . . . 8 (𝜑 → (1 + 𝐸) ≠ 0)
217207, 174, 216redivcld 11055 . . . . . . 7 (𝜑 → (𝐺 / (1 + 𝐸)) ∈ ℝ)
218217adantr 466 . . . . . 6 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
219217ltpnfd 12160 . . . . . . . . . 10 (𝜑 → (𝐺 / (1 + 𝐸)) < +∞)
220219adantr 466 . . . . . . . . 9 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < +∞)
221 id 22 . . . . . . . . . . 11 ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞)
222221eqcomd 2777 . . . . . . . . . 10 ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
223222adantl 467 . . . . . . . . 9 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
224220, 223breqtrd 4812 . . . . . . . 8 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
225224adantlr 694 . . . . . . 7 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
226 simpl 468 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝜑𝑌 ≠ ∅))
227 simpr 471 . . . . . . . . . 10 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞)
228 nnex 11228 . . . . . . . . . . . 12 ℕ ∈ V
229228a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ℕ ∈ V)
230 icossicc 12466 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ (0[,]+∞)
231230, 114sseldi 3750 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,]+∞))
232 eqid 2771 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (𝑃𝑗)) = (𝑗 ∈ ℕ ↦ (𝑃𝑗))
233231, 232fmptd 6527 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑃𝑗)):ℕ⟶(0[,]+∞))
234233adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝑗 ∈ ℕ ↦ (𝑃𝑗)):ℕ⟶(0[,]+∞))
235229, 234sge0repnf 41120 . . . . . . . . . 10 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞))
236227, 235mpbird 247 . . . . . . . . 9 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
237236adantlr 694 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
238218adantr 466 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
239207adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ∈ ℝ)
240239adantlr 694 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ∈ ℝ)
241 simpr 471 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
24227, 172ltaddrpd 12108 . . . . . . . . . . . 12 (𝜑 → 1 < (1 + 𝐸))
243242adantr 466 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → 1 < (1 + 𝐸))
24458adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → 𝑌 ∈ Fin)
245 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → 𝑌 ≠ ∅)
246202adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → (𝐴𝑌):𝑌⟶ℝ)
247204adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → (𝐵𝑌):𝑌⟶ℝ)
24818, 244, 245, 246, 247hoidmvn0val 41318 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
2495a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
250 fvres 6348 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌 → ((𝐴𝑌)‘𝑘) = (𝐴𝑘))
251 fvres 6348 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌 → ((𝐵𝑌)‘𝑘) = (𝐵𝑘))
252250, 251oveq12d 6811 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑌 → (((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
253252fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑘𝑌 → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
254253adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
255200adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝐴:𝑊⟶ℝ)
256 elun1 3931 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑌𝑘 ∈ (𝑌 ∪ {𝑍}))
257256, 44syl6eleqr 2861 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌𝑘𝑊)
258257adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝑘𝑊)
259255, 258ffvelrnd 6503 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐴𝑘) ∈ ℝ)
260203adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝐵:𝑊⟶ℝ)
261260, 258ffvelrnd 6503 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐵𝑘) ∈ ℝ)
262 volico 40717 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
263259, 261, 262syl2anc 573 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
264 hoidmvlelem3.lt . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑊) → (𝐴𝑘) < (𝐵𝑘))
265258, 264syldan 579 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐴𝑘) < (𝐵𝑘))
266265iftrued 4233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
267254, 263, 2663eqtrd 2809 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
268267prodeq2dv 14860 . . . . . . . . . . . . . . . 16 (𝜑 → ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)))
269268eqcomd 2777 . . . . . . . . . . . . . . 15 (𝜑 → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
270269adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
271248, 249, 2703eqtr4d 2815 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → 𝐺 = ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)))
272 difrp 12071 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → ((𝐴𝑘) < (𝐵𝑘) ↔ ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+))
273259, 261, 272syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑌) → ((𝐴𝑘) < (𝐵𝑘) ↔ ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+))
274265, 273mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑌) → ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
27558, 274fprodrpcl 14893 . . . . . . . . . . . . . 14 (𝜑 → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
276275adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
277271, 276eqeltrd 2850 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → 𝐺 ∈ ℝ+)
278213adantr 466 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → (1 + 𝐸) ∈ ℝ+)
279277, 278ltdivgt1 40088 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → (1 < (1 + 𝐸) ↔ (𝐺 / (1 + 𝐸)) < 𝐺))
280243, 279mpbid 222 . . . . . . . . . 10 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) < 𝐺)
281280adantr 466 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) < 𝐺)
282 hoidmvlelem3.i2 . . . . . . . . . . . . . . . . . . . . 21 (𝜑X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
283282adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
284 fvexd 6344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑥𝑘) ∈ V)
285 hoidmvlelem3.s . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑆𝑈)
286285elexd 3366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑆 ∈ V)
287284, 286ifcld 4270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
288287ralrimivw 3116 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
289288adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
290 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))
291290fnmpt 6160 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊)
292289, 291syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊)
293 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
294 mptexg 6628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑊 ∈ Fin → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
29553, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
296295adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
297 hoidmvlelem3.o . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑂 = (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ↦ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
298297fvmpt2 6433 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V) → (𝑂𝑥) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
299293, 296, 298syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
300299fneq1d 6121 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥) Fn 𝑊 ↔ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊))
301292, 300mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) Fn 𝑊)
302 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝜑
303 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘𝑥
304 nfixp1 8082 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))
305303, 304nfel 2926 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))
306302, 305nfan 1980 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
307299fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
308307adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
309 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘𝑊) → 𝑘𝑊)
310287adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘𝑊) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
311290fvmpt2 6433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘𝑊 ∧ if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
312309, 310, 311syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘𝑊) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
313312adantlr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
314308, 313eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
315 iftrue 4231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘𝑌 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
316315adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
317 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑥 ∈ V
318317elixp 8069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ↔ (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
319318simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) → ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
320319adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
321 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → 𝑘𝑌)
322 rspa 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
323320, 321, 322syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
324323ad4ant24 1212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
325316, 324eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
326 snidg 4345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
32747, 326syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑍 ∈ {𝑍})
328 elun2 3932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
329327, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
33055a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑌 ∪ {𝑍}) = 𝑊)
331329, 330eleqtrd 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑍𝑊)
332200, 331ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐴𝑍) ∈ ℝ)
333332rexrd 10291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴𝑍) ∈ ℝ*)
334203, 331ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐵𝑍) ∈ ℝ)
335334rexrd 10291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐵𝑍) ∈ ℝ*)
336 iccssxr 12461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ*
337 hoidmvlelem3.u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
338 ssrab2 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
339337, 338eqsstri 3784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
340339, 285sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
341336, 340sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑆 ∈ ℝ*)
342 iccgelb 12435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑆)
343333, 335, 340, 342syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴𝑍) ≤ 𝑆)
344 hoidmvlelem3.sb . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑆 < (𝐵𝑍))
345333, 335, 341, 343, 344elicod 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
346345ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → 𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
347 iffalse 4234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑌 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = 𝑆)
348347adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = 𝑆)
34944eleq2i 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘𝑊𝑘 ∈ (𝑌 ∪ {𝑍}))
350349biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘𝑊𝑘 ∈ (𝑌 ∪ {𝑍}))
351350adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 ∈ (𝑌 ∪ {𝑍}))
352 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → ¬ 𝑘𝑌)
353 elunnel1 3905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘 ∈ (𝑌 ∪ {𝑍}) ∧ ¬ 𝑘𝑌) → 𝑘 ∈ {𝑍})
354351, 352, 353syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 ∈ {𝑍})
355 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
356354, 355syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 = 𝑍)
357 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
358 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
359357, 358oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
360356, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
361360adantll 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
362348, 361eleq12d 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → (if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)) ↔ 𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍))))
363346, 362mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
364363adantllr 698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
365325, 364pm2.61dan 814 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
366314, 365eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
367366ex 397 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 → ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
368306, 367ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
369301, 368jca 501 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
370 fvex 6342 . . . . . . . . . . . . . . . . . . . . . 22 (𝑂𝑥) ∈ V
371370elixp 8069 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂𝑥) ∈ X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ↔ ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
372369, 371sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) ∈ X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)))
373283, 372sseldd 3753 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) ∈ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
374 eliun 4658 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑥) ∈ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
375373, 374sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
376 ixpfn 8068 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) → 𝑥 Fn 𝑌)
377376adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥 Fn 𝑌)
378377ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑥 Fn 𝑌)
379 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 𝑗 ∈ ℕ
380306, 379nfan 1980 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ)
381 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘(𝑂𝑥)
382 nfixp1 8082 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
383381, 382nfel 2926 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘(𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
384380, 383nfan 1980 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
3853073adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
386287adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
387258, 386, 311syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘𝑌) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
3883873adant2 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
3893153ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
390385, 388, 3893eqtrrd 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) = ((𝑂𝑥)‘𝑘))
391390ad5ant125 1464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) = ((𝑂𝑥)‘𝑘))
392 simpl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
393370elixp 8069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
394392, 393sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
395394simprd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
396257adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → 𝑘𝑊)
397 rspa 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
398395, 396, 397syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
399398adantll 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
400391, 399eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
40129ad3antrrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝜑)
40237ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑗 ∈ ℕ)
403299fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥)‘𝑍) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍))
404 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
405 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 = 𝑍 → (𝑘𝑌𝑍𝑌))
406 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 = 𝑍 → (𝑥𝑘) = (𝑥𝑍))
407405, 406ifbieq1d 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 = 𝑍 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
408407adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 = 𝑍) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
409 fvexd 6344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (𝑥𝑍) ∈ V)
410409, 286ifcld 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → if(𝑍𝑌, (𝑥𝑍), 𝑆) ∈ V)
411404, 408, 331, 410fvmptd 6430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
412411adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
41347eldifbd 3736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ¬ 𝑍𝑌)
414413iffalsed 4236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(𝑍𝑌, (𝑥𝑍), 𝑆) = 𝑆)
415414adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → if(𝑍𝑌, (𝑥𝑍), 𝑆) = 𝑆)
416403, 412, 4153eqtrrd 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑆 = ((𝑂𝑥)‘𝑍))
417416ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑆 = ((𝑂𝑥)‘𝑍))
418401, 331syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑍𝑊)
419393simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
420419adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
421 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝑍 → ((𝑂𝑥)‘𝑘) = ((𝑂𝑥)‘𝑍))
422 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
423 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
424422, 423oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
425421, 424eleq12d 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑍 → (((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
426425rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑍𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
427418, 420, 426syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
428417, 427eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
4291493adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
430603ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
431429, 430eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐽𝑗) = ((𝐶𝑗) ↾ 𝑌))
432431fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
433401, 402, 428, 432syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
434433adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
435 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑌 → (((𝐶𝑗) ↾ 𝑌)‘𝑘) = ((𝐶𝑗)‘𝑘))
436435adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐶𝑗) ↾ 𝑌)‘𝑘) = ((𝐶𝑗)‘𝑘))
437434, 436eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐽𝑗)‘𝑘) = ((𝐶𝑗)‘𝑘))
438107elexd 3366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ V)
439108fvmpt2 6433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
440139, 438, 439syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
4414403adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
442933ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
443441, 442eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐾𝑗) = ((𝐷𝑗) ↾ 𝑌))
444443fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
445401, 402, 428, 444syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
446445adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
447 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑌 → (((𝐷𝑗) ↾ 𝑌)‘𝑘) = ((𝐷𝑗)‘𝑘))
448447adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐷𝑗) ↾ 𝑌)‘𝑘) = ((𝐷𝑗)‘𝑘))
449446, 448eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐾𝑗)‘𝑘) = ((𝐷𝑗)‘𝑘))
450437, 449oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
451450eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
452400, 451eleqtrd 2852 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
453452ex 397 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑌 → (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
454384, 453ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
455378, 454jca 501 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
456317elixp 8069 . . . . . . . . . . . . . . . . . . . . 21 (𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
457455, 456sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
458457ex 397 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) → ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
459458reximdva 3165 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
460375, 459mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
461 eliun 4658 . . . . . . . . . . . . . . . . 17 (𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
462460, 461sylibr 224 . . . . . . . . . . . . . . . 16 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
463462ralrimiva 3115 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥X 𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
464 dfss3 3741 . . . . . . . . . . . . . . 15 (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ ∀𝑥X 𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
465463, 464sylibr 224 . . . . . . . . . . . . . 14 (𝜑X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
466 ovexd 6825 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ ↑𝑚 𝑌) ∈ V)
467228a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℕ ∈ V)
468466, 467elmapd 8023 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ↔ 𝐾:ℕ⟶(ℝ ↑𝑚 𝑌)))
469109, 468mpbird 247 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ))
470466, 467elmapd 8023 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ↔ 𝐽:ℕ⟶(ℝ ↑𝑚 𝑌)))
47189, 470mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ))
47282, 71elmapd 8023 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ (𝐵𝑌):𝑌⟶ℝ))
473204, 472mpbird 247 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌))
47482, 71elmapd 8023 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ (𝐴𝑌):𝑌⟶ℝ))
475202, 474mpbird 247 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌))
476 hoidmvlelem3.i . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
477 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 = (𝐴𝑌) → (𝑒𝑘) = ((𝐴𝑌)‘𝑘))
478477adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → (𝑒𝑘) = ((𝐴𝑌)‘𝑘))
479250adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → ((𝐴𝑌)‘𝑘) = (𝐴𝑘))
480478, 479eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → (𝑒𝑘) = (𝐴𝑘))
481480oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → ((𝑒𝑘)[,)(𝑓𝑘)) = ((𝐴𝑘)[,)(𝑓𝑘)))
482481ixpeq2dva 8077 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = (𝐴𝑌) → X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) = X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)))
483482sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐴𝑌) → (X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
484 oveq1 6800 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = (𝐴𝑌) → (𝑒(𝐿𝑌)𝑓) = ((𝐴𝑌)(𝐿𝑌)𝑓))
485484breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐴𝑌) → ((𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
486483, 485imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐴𝑌) → ((X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
487486ralbidv 3135 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐴𝑌) → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
488487ralbidv 3135 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝐴𝑌) → (∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
489488ralbidv 3135 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝐴𝑌) → (∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
490489rspcva 3458 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌) ∧ ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
491475, 476, 490syl2anc 573 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
492 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (𝐵𝑌) → (𝑓𝑘) = ((𝐵𝑌)‘𝑘))
493492adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → (𝑓𝑘) = ((𝐵𝑌)‘𝑘))
494251adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → ((𝐵𝑌)‘𝑘) = (𝐵𝑘))
495493, 494eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → (𝑓𝑘) = (𝐵𝑘))
496495oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → ((𝐴𝑘)[,)(𝑓𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
497496ixpeq2dva 8077 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝐵𝑌) → X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) = X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
498497sseq1d 3781 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝐵𝑌) → (X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
499 oveq2 6801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝐵𝑌) → ((𝐴𝑌)(𝐿𝑌)𝑓) = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
500499breq1d 4796 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝐵𝑌) → (((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
501498, 500imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝐵𝑌) → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
502501ralbidv 3135 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝐵𝑌) → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
503502ralbidv 3135 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐵𝑌) → (∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
504503rspcva 3458 . . . . . . . . . . . . . . . . 17 (((𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌) ∧ ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
505473, 491, 504syl2anc 573 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
506 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = 𝐽 → (𝑔𝑗) = (𝐽𝑗))
507506fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝐽 → ((𝑔𝑗)‘𝑘) = ((𝐽𝑗)‘𝑘))
508507oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝐽 → (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
509508ixpeq2dv 8078 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝐽X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
510509iuneq2d 4681 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝐽 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
511510sseq2d 3782 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝐽 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
512506oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝐽 → ((𝑔𝑗)(𝐿𝑌)(𝑗)) = ((𝐽𝑗)(𝐿𝑌)(𝑗)))
513512mpteq2dv 4879 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝐽 → (𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))
514513fveq2d 6336 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝐽 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))
515514breq2d 4798 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝐽 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
516511, 515imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝐽 → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))))
517516ralbidv 3135 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝐽 → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))))
518517rspcva 3458 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ∧ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
519471, 505, 518syl2anc 573 . . . . . . . . . . . . . . 15 (𝜑 → ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
520 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝐾 → (𝑗) = (𝐾𝑗))
521520fveq1d 6334 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝐾 → ((𝑗)‘𝑘) = ((𝐾𝑗)‘𝑘))
522521oveq2d 6809 . . . . . . . . . . . . . . . . . . . 20 ( = 𝐾 → (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
523522ixpeq2dv 8078 . . . . . . . . . . . . . . . . . . 19 ( = 𝐾X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
524523iuneq2d 4681 . . . . . . . . . . . . . . . . . 18 ( = 𝐾 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
525524sseq2d 3782 . . . . . . . . . . . . . . . . 17 ( = 𝐾 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
526520oveq2d 6809 . . . . . . . . . . . . . . . . . . . 20 ( = 𝐾 → ((𝐽𝑗)(𝐿𝑌)(𝑗)) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
527526mpteq2dv 4879 . . . . . . . . . . . . . . . . . . 19 ( = 𝐾 → (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))
528527fveq2d 6336 . . . . . . . . . . . . . . . . . 18 ( = 𝐾 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
529528breq2d 4798 . . . . . . . . . . . . . . . . 17 ( = 𝐾 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
530525, 529imbi12d 333 . . . . . . . . . . . . . . . 16 ( = 𝐾 → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))))
531530rspcva 3458 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ∧ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))) → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
532469, 519, 531syl2anc 573 . . . . . . . . . . . . . 14 (𝜑 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
533465, 532mpd 15 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
534 idd 24 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
535533, 534mpd 15 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
536535adantr 466 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
53741adantl 467 . . . . . . . . . . . . . 14 (((𝜑𝑌 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
538537mpteq2dva 4878 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → (𝑗 ∈ ℕ ↦ (𝑃𝑗)) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))
539538fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
540249, 539breq12d 4799 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → (𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
541536, 540mpbird 247 . . . . . . . . . 10 ((𝜑𝑌 ≠ ∅) → 𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
542541adantr 466 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
543238, 240, 241, 281, 542ltletrd 10399 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
544226, 237, 543syl2anc 573 . . . . . . 7 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
545225, 544pm2.61dan 814 . . . . . 6 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
546196, 197, 198, 199, 218, 545sge0uzfsumgt 41178 . . . . 5 ((𝜑𝑌 ≠ ∅) → ∃𝑚 ∈ ℕ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
547217adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
548 fzfid 12980 . . . . . . . . . . . . 13 (𝜑 → (1...𝑚) ∈ Fin)
549 simpl 468 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑚)) → 𝜑)
550 elfznn 12577 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℕ)
551550adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑚)) → 𝑗 ∈ ℕ)
55228, 114sseldi 3750 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ ℝ)
553549, 551, 552syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑚)) → (𝑃𝑗) ∈ ℝ)
554548, 553fsumrecl 14673 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ∈ ℝ)
555554adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ∈ ℝ)
556 simpr 471 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
557547, 555, 556ltled 10387 . . . . . . . . . 10 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) ≤ Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
558207adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ∈ ℝ)
559213adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (1 + 𝐸) ∈ ℝ+)
560558, 555, 559ledivmuld 12128 . . . . . . . . . 10 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ((𝐺 / (1 + 𝐸)) ≤ Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ↔ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
561557, 560mpbid 222 . . . . . . . . 9 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
562561ex 397 . . . . . . . 8 (𝜑 → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
563562adantr 466 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
564563adantlr 694 . . . . . 6 (((𝜑𝑌 ≠ ∅) ∧ 𝑚 ∈ ℕ) → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
565564reximdva 3165 . . . . 5 ((𝜑𝑌 ≠ ∅) → (∃𝑚 ∈ ℕ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
566546, 565mpd 15 . . . 4 ((𝜑𝑌 ≠ ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
567193, 195, 566syl2anc 573 . . 3 ((𝜑 ∧ ¬ 𝑌 = ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
568192, 567pm2.61dan 814 . 2 (𝜑 → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
569433ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑋 ∈ Fin)
570463ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑌𝑋)
571473ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑍 ∈ (𝑋𝑌))
5722003ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐴:𝑊⟶ℝ)
5732033ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐵:𝑊⟶ℝ)
574623ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
575 eqid 2771 . . . . 5 (𝑦𝑌 ↦ 0) = (𝑦𝑌 ↦ 0)
576 eqid 2771 . . . . 5 (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0))) = (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
577953ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
578 eqid 2771 . . . . 5 (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0))) = (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
579 fveq2 6332 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝐶𝑖) = (𝐶𝑗))
580 fveq2 6332 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝐷𝑖) = (𝐷𝑗))
581579, 580oveq12d 6811 . . . . . . . . 9 (𝑖 = 𝑗 → ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)) = ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
582581cbvmptv 4884 . . . . . . . 8 (𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
583582fveq2i 6335 . . . . . . 7 ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗))))
584 hoidmvlelem3.r . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
585583, 584syl5eqel 2854 . . . . . 6 (𝜑 → (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) ∈ ℝ)
5865853ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) ∈ ℝ)
587 hoidmvlelem3.h . . . . . 6 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
588 eleq1w 2833 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗𝑌𝑖𝑌))
589 fveq2 6332 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑐𝑗) = (𝑐𝑖))
590589breq1d 4796 . . . . . . . . . . 11 (𝑗 = 𝑖 → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐𝑖) ≤ 𝑥))
591590, 589ifbieq1d 4248 . . . . . . . . . 10 (𝑗 = 𝑖 → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥))
592588, 589, 591ifbieq12d 4252 . . . . . . . . 9 (𝑗 = 𝑖 → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))
593592cbvmptv 4884 . . . . . . . 8 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))
594593mpteq2i 4875 . . . . . . 7 (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥))))
595594mpteq2i 4875 . . . . . 6 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))))
596587, 595eqtri 2793 . . . . 5 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))))
5971723ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐸 ∈ ℝ+)
598 fveq2 6332 . . . . . . . . . . . 12 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
599 fveq2 6332 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
600599fveq2d 6336 . . . . . . . . . . . 12 (𝑗 = 𝑖 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑧)‘(𝐷𝑖)))
601598, 600oveq12d 6811 . . . . . . . . . . 11 (𝑗 = 𝑖 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))
602601cbvmptv 4884 . . . . . . . . . 10 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))
603602fveq2i 6335 . . . . . . . . 9 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖)))))
604603oveq2i 6804 . . . . . . . 8 ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))
605604breq2i 4794 . . . . . . 7 ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖)))))))
606605rabbii 3335 . . . . . 6 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))}
607337, 606eqtri 2793 . . . . 5 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))}
6082853ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑆𝑈)
6093443ad2ant1 1127 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑆 < (𝐵𝑍))
610 eqid 2771 . . . . 5 (𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖))) = (𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
611 simp2 1131 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑚 ∈ ℕ)
612 id 22 . . . . . . . 8 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
613 fveq2 6332 . . . . . . . . . . 11 (𝑗 = 𝑖 → (𝑃𝑗) = (𝑃𝑖))
614613cbvsumv 14634 . . . . . . . . . 10 Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) = Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)
615614oveq2i 6804 . . . . . . . . 9 ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖))
616615a1i 11 . . . . . . . 8 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
617612, 616breqtrd 4812 . . . . . . 7 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
6186173ad2ant3 1129 . . . . . 6 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
619 simpl 468 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑚)) → 𝜑)
620 elfznn 12577 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ)
621620adantl 467 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ)
622 eleq1w 2833 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ))
623 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐽𝑗) = (𝐽𝑖))
624 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐾𝑗) = (𝐾𝑖))
625623, 624oveq12d 6811 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
626613, 625eqeq12d 2786 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ↔ (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖))))
627622, 626imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝑗 ∈ ℕ → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))) ↔ (𝑖 ∈ ℕ → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))))
628627, 41chvarv 2425 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
629628adantl 467 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
630622anbi2d 614 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑖 ∈ ℕ)))
631598fveq1d 6334 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
632599fveq1d 6334 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
633631, 632oveq12d 6811 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
634633eleq2d 2836 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
635598reseq1d 5533 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((𝐶𝑗) ↾ 𝑌) = ((𝐶𝑖) ↾ 𝑌))
636634, 635ifbieq1d 4248 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
637623, 636eqeq12d 2786 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ↔ (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)))
638630, 637imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹)) ↔ ((𝜑𝑖 ∈ ℕ) → (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))))
639638, 149chvarv 2425 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
640599reseq1d 5533 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((𝐷𝑗) ↾ 𝑌) = ((𝐷𝑖) ↾ 𝑌))
641634, 640ifbieq1d 4248 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
642624, 641eqeq12d 2786 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ↔ (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
643630, 642imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹)) ↔ ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))))
644643, 440chvarv 2425 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
645639, 644oveq12d 6811 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
646629, 645eqtrd 2805 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
647 simpr 471 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
648 ovexd 6825 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) ∈ V)
649610fvmpt2 6433 . . . . . . . . . . . . 13 ((𝑖 ∈ ℕ ∧ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) ∈ V) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
650647, 648, 649syl2anc 573 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
651 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (𝐶𝑖) ∈ V
652651resex 5584 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑖) ↾ 𝑌) ∈ V
653652a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐶𝑖) ↾ 𝑌) ∈ V)
65480, 143syl5eqelr 2855 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑦𝑌 ↦ 0) ∈ V)
655653, 654ifcld 4270 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
656655adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
657576fvmpt2 6433 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
658647, 656, 657syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
65980eqcomi 2780 . . . . . . . . . . . . . . . 16 (𝑦𝑌 ↦ 0) = 𝐹
660 ifeq2 4230 . . . . . . . . . . . . . . . 16 ((𝑦𝑌 ↦ 0) = 𝐹 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
661659, 660ax-mp 5 . . . . . . . . . . . . . . 15 if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)
662661a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
663658, 662eqtrd 2805 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
664 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (𝐷𝑖) ∈ V
665664resex 5584 . . . . . . . . . . . . . . . . . 18 ((𝐷𝑖) ↾ 𝑌) ∈ V
666665a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷𝑖) ↾ 𝑌) ∈ V)
667666, 654ifcld 4270 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
668667adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
669578fvmpt2 6433 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
670647, 668, 669syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
671 biid 251 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
672671, 659ifbieq2i 4249 . . . . . . . . . . . . . . 15 if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)
673672a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
674670, 673eqtrd 2805 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
675663, 674oveq12d 6811 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
676650, 675eqtrd 2805 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
677646, 676eqtr4d 2808 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
678619, 621, 677syl2anc 573 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑚)) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
6796783ad2antl1 1200 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) ∧ 𝑖 ∈ (1...𝑚)) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
680679sumeq2dv 14641 . . . . . . 7 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → Σ𝑖 ∈ (1...𝑚)(𝑃𝑖) = Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
681680oveq2d 6809 . . . . . 6 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖)))
682618, 681breqtrd 4812 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖)))
683 fveq2 6332 . . . . . . . 8 (𝑗 = → (𝐷𝑗) = (𝐷))
684683fveq1d 6334 . . . . . . 7 (𝑗 = → ((𝐷𝑗)‘𝑍) = ((𝐷)‘𝑍))
685684cbvmptv 4884 . . . . . 6 (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ( ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷)‘𝑍))
686685rneqi 5490 . . . . 5 ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ran ( ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷)‘𝑍))
687 fveq2 6332 . . . . . . . . . . . 12 ( = 𝑖 → (𝐶) = (𝐶𝑖))
688687fveq1d 6334 . . . . . . . . . . 11 ( = 𝑖 → ((𝐶)‘𝑍) = ((𝐶𝑖)‘𝑍))
689 fveq2 6332 . . . . . . . . . . . 12 ( = 𝑖 → (𝐷) = (𝐷𝑖))
690689fveq1d 6334 . . . . . . . . . . 11 ( = 𝑖 → ((𝐷)‘𝑍) = ((𝐷𝑖)‘𝑍))
691688, 690oveq12d 6811 . . . . . . . . . 10 ( = 𝑖 → (((𝐶)‘𝑍)[,)((𝐷)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
692691eleq2d 2836 . . . . . . . . 9 ( = 𝑖 → (𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
693692cbvrabv 3349 . . . . . . . 8 { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} = {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))}
694693mpteq1i 4873 . . . . . . 7 (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))
695694rneqi 5490 . . . . . 6 ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))
696695uneq2i 3915 . . . . 5 ({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))) = ({(𝐵𝑍)} ∪ ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)))
697 eqid 2771 . . . . 5 inf(({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))), ℝ, < ) = inf(({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))), ℝ, < )
69818, 569, 570, 571, 44, 572, 573, 574, 575, 576, 577, 578, 586, 596, 5, 597, 607, 608, 609, 610, 611, 682, 686, 696, 697hoidmvlelem2 41330 . . . 4 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → ∃𝑢𝑈 𝑆 < 𝑢)
6996983exp 1112 . . 3 (𝜑 → (𝑚 ∈ ℕ → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢)))
700699rexlimdv 3178 . 2 (𝜑 → (∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢))
701568, 700mpd 15 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cdif 3720  cun 3721  wss 3723  c0 4063  ifcif 4225  {csn 4316   ciun 4654   class class class wbr 4786  cmpt 4863  ran crn 5250  cres 5251   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  cmpt2 6795  𝑚 cmap 8009  Xcixp 8062  Fincfn 8109  infcinf 8503  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  +∞cpnf 10273  *cxr 10275   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  cz 11579  +crp 12035  [,)cico 12382  [,]cicc 12383  ...cfz 12533  Σcsu 14624  cprod 14842  volcvol 23451  Σ^csumge0 41096
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-inf2 8702  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  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  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-rmo 3069  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-int 4612  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-se 5209  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-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-rlim 14428  df-sum 14625  df-prod 14843  df-rest 16291  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971  df-cmp 21411  df-ovol 23452  df-vol 23453  df-sumge0 41097
This theorem is referenced by:  hoidmvlelem4  41332
  Copyright terms: Public domain W3C validator