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 39487
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 10908 . . . . 5 1 ∈ ℕ
21a1i 11 . . . 4 ((𝜑𝑌 = ∅) → 1 ∈ ℕ)
3 0le0 10987 . . . . . 6 0 ≤ 0
43a1i 11 . . . . 5 ((𝜑𝑌 = ∅) → 0 ≤ 0)
5 hoidmvlelem3.g . . . . . . . 8 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
65a1i 11 . . . . . . 7 ((𝜑𝑌 = ∅) → 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
7 fveq2 6103 . . . . . . . . 9 (𝑌 = ∅ → (𝐿𝑌) = (𝐿‘∅))
8 reseq2 5312 . . . . . . . . . 10 (𝑌 = ∅ → (𝐴𝑌) = (𝐴 ↾ ∅))
9 res0 5321 . . . . . . . . . . 11 (𝐴 ↾ ∅) = ∅
109a1i 11 . . . . . . . . . 10 (𝑌 = ∅ → (𝐴 ↾ ∅) = ∅)
118, 10eqtrd 2644 . . . . . . . . 9 (𝑌 = ∅ → (𝐴𝑌) = ∅)
12 reseq2 5312 . . . . . . . . . 10 (𝑌 = ∅ → (𝐵𝑌) = (𝐵 ↾ ∅))
13 res0 5321 . . . . . . . . . . 11 (𝐵 ↾ ∅) = ∅
1413a1i 11 . . . . . . . . . 10 (𝑌 = ∅ → (𝐵 ↾ ∅) = ∅)
1512, 14eqtrd 2644 . . . . . . . . 9 (𝑌 = ∅ → (𝐵𝑌) = ∅)
167, 11, 15oveq123d 6570 . . . . . . . 8 (𝑌 = ∅ → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = (∅(𝐿‘∅)∅))
1716adantl 481 . . . . . . 7 ((𝜑𝑌 = ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = (∅(𝐿‘∅)∅))
18 hoidmvlelem3.l . . . . . . . 8 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
19 f0 5999 . . . . . . . . 9 ∅:∅⟶ℝ
2019a1i 11 . . . . . . . 8 ((𝜑𝑌 = ∅) → ∅:∅⟶ℝ)
2118, 20, 20hoidmv0val 39473 . . . . . . 7 ((𝜑𝑌 = ∅) → (∅(𝐿‘∅)∅) = 0)
226, 17, 213eqtrd 2648 . . . . . 6 ((𝜑𝑌 = ∅) → 𝐺 = 0)
23 nfcvd 2752 . . . . . . . . . . 11 (𝜑𝑗(𝑃‘1))
24 nfv 1830 . . . . . . . . . . 11 𝑗𝜑
25 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑗 = 1) → 𝑗 = 1)
2625fveq2d 6107 . . . . . . . . . . 11 ((𝜑𝑗 = 1) → (𝑃𝑗) = (𝑃‘1))
27 1red 9934 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
28 rge0ssre 12151 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
29 id 22 . . . . . . . . . . . . . 14 (𝜑𝜑)
301a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℕ)
311elexi 3186 . . . . . . . . . . . . . . 15 1 ∈ V
32 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑗 = 1 → (𝑗 ∈ ℕ ↔ 1 ∈ ℕ))
3332anbi2d 736 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑 ∧ 1 ∈ ℕ)))
34 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑗 = 1 → (𝑃𝑗) = (𝑃‘1))
3534eleq1d 2672 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝑃𝑗) ∈ (0[,)+∞) ↔ (𝑃‘1) ∈ (0[,)+∞)))
3633, 35imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝑃‘1) ∈ (0[,)+∞))))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
38 ovex 6577 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ V
3938a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ V)
40 hoidmvlelem3.p . . . . . . . . . . . . . . . . . . 19 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4140fvmpt2 6200 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ V) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4237, 39, 41syl2anc 691 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
4342adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
44 hoidmvlelem3.x . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋 ∈ Fin)
45 hoidmvlelem3.w . . . . . . . . . . . . . . . . . . . . . 22 𝑊 = (𝑌 ∪ {𝑍})
4645a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑊 = (𝑌 ∪ {𝑍}))
47 hoidmvlelem3.y . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌𝑋)
48 hoidmvlelem3.z . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑍 ∈ (𝑋𝑌))
4948eldifad 3552 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑍𝑋)
50 snssi 4280 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍𝑋 → {𝑍} ⊆ 𝑋)
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑍} ⊆ 𝑋)
5247, 51unssd 3751 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑌 ∪ {𝑍}) ⊆ 𝑋)
5346, 52eqsstrd 3602 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑊𝑋)
5444, 53ssfid 8068 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑊 ∈ Fin)
55 ssun1 3738 . . . . . . . . . . . . . . . . . . . . 21 𝑌 ⊆ (𝑌 ∪ {𝑍})
5645eqcomi 2619 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 ∪ {𝑍}) = 𝑊
5755, 56sseqtri 3600 . . . . . . . . . . . . . . . . . . . 20 𝑌𝑊
5857a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌𝑊)
5954, 58ssfid 8068 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌 ∈ Fin)
6059adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ Fin)
61 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
6261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
63 hoidmvlelem3.c . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
6463ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊))
65 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
6755, 45sseqtr4i 3601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑌𝑊
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → 𝑌𝑊)
6966, 68fssresd 5984 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ)
70 reex 9906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ∈ V
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → ℝ ∈ V)
7254, 58ssexd 4733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑌 ∈ V)
7372adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ V)
7471, 73elmapd 7758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ))
7569, 74mpbird 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
7675adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐶𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
7762, 76eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
78 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = 𝐹)
7978adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = 𝐹)
80 0red 9920 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑌) → 0 ∈ ℝ)
81 hoidmvlelem3.f . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐹 = (𝑦𝑌 ↦ 0)
8280, 81fmptd 6292 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝑌⟶ℝ)
8370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ℝ ∈ V)
8483, 59elmapd 7758 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ∈ (ℝ ↑𝑚 𝑌) ↔ 𝐹:𝑌⟶ℝ))
8582, 84mpbird 246 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹 ∈ (ℝ ↑𝑚 𝑌))
8685ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹 ∈ (ℝ ↑𝑚 𝑌))
8779, 86eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
8877, 87pm2.61dan 828 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
89 hoidmvlelem3.j . . . . . . . . . . . . . . . . . . . 20 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
9088, 89fmptd 6292 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐽:ℕ⟶(ℝ ↑𝑚 𝑌))
9190ffvelrnda 6267 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) ∈ (ℝ ↑𝑚 𝑌))
92 elmapi 7765 . . . . . . . . . . . . . . . . . 18 ((𝐽𝑗) ∈ (ℝ ↑𝑚 𝑌) → (𝐽𝑗):𝑌⟶ℝ)
9391, 92syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ)
94 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
9594adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
96 hoidmvlelem3.d . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
9796ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊))
98 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
10099, 68fssresd 5984 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗) ↾ 𝑌):𝑌⟶ℝ)
10171, 73elmapd 7758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ ((𝐷𝑗) ↾ 𝑌):𝑌⟶ℝ))
102100, 101mpbird 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
103102adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐷𝑗) ↾ 𝑌) ∈ (ℝ ↑𝑚 𝑌))
10495, 103eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
105 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = 𝐹)
106105adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = 𝐹)
107106, 86eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
108104, 107pm2.61dan 828 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ (ℝ ↑𝑚 𝑌))
109 hoidmvlelem3.k . . . . . . . . . . . . . . . . . . . 20 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
110108, 109fmptd 6292 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶(ℝ ↑𝑚 𝑌))
111110ffvelrnda 6267 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) ∈ (ℝ ↑𝑚 𝑌))
112 elmapi 7765 . . . . . . . . . . . . . . . . . 18 ((𝐾𝑗) ∈ (ℝ ↑𝑚 𝑌) → (𝐾𝑗):𝑌⟶ℝ)
113111, 112syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗):𝑌⟶ℝ)
11418, 60, 93, 113hoidmvcl 39472 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ∈ (0[,)+∞))
11543, 114eqeltrd 2688 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞))
11631, 36, 115vtocl 3232 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝑃‘1) ∈ (0[,)+∞))
11729, 30, 116syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝑃‘1) ∈ (0[,)+∞))
11828, 117sseldi 3566 . . . . . . . . . . . 12 (𝜑 → (𝑃‘1) ∈ ℝ)
119118recnd 9947 . . . . . . . . . . 11 (𝜑 → (𝑃‘1) ∈ ℂ)
12023, 24, 26, 27, 119sumsnd 38208 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ {1} (𝑃𝑗) = (𝑃‘1))
121120adantr 480 . . . . . . . . 9 ((𝜑𝑌 = ∅) → Σ𝑗 ∈ {1} (𝑃𝑗) = (𝑃‘1))
122 fveq2 6103 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐽𝑗) = (𝐽‘1))
123 fveq2 6103 . . . . . . . . . . . . 13 (𝑗 = 1 → (𝐾𝑗) = (𝐾‘1))
124122, 123oveq12d 6567 . . . . . . . . . . . 12 (𝑗 = 1 → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
125 ovex 6577 . . . . . . . . . . . 12 ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) ∈ V
126124, 40, 125fvmpt 6191 . . . . . . . . . . 11 (1 ∈ ℕ → (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
1271, 126ax-mp 5 . . . . . . . . . 10 (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1))
128127a1i 11 . . . . . . . . 9 ((𝜑𝑌 = ∅) → (𝑃‘1) = ((𝐽‘1)(𝐿𝑌)(𝐾‘1)))
1297oveqd 6566 . . . . . . . . . . 11 (𝑌 = ∅ → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = ((𝐽‘1)(𝐿‘∅)(𝐾‘1)))
130129adantl 481 . . . . . . . . . 10 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = ((𝐽‘1)(𝐿‘∅)(𝐾‘1)))
131122feq1d 5943 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝐽𝑗):𝑌⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
13233, 131imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝐽‘1):𝑌⟶ℝ)))
13369adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ)
13462feq1d 5943 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐶𝑗) ↾ 𝑌):𝑌⟶ℝ))
135133, 134mpbird 246 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
13682ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹:𝑌⟶ℝ)
13779feq1d 5943 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ))
138136, 137mpbird 246 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
139135, 138pm2.61dan 828 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
140 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
141 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 (𝐶𝑗) ∈ V
142141resex 5363 . . . . . . . . . . . . . . . . . . . 20 ((𝐶𝑗) ↾ 𝑌) ∈ V
14362, 142syl6eqel 2696 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
14485elexd 3187 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 ∈ V)
145144adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → 𝐹 ∈ V)
146145adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝐹 ∈ V)
14779, 146eqeltrd 2688 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
148143, 147pm2.61dan 828 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V)
14989fvmpt2 6200 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
150140, 148, 149syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
151150feq1d 5943 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐽𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ))
152139, 151mpbird 246 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐽𝑗):𝑌⟶ℝ)
15331, 132, 152vtocl 3232 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝐽‘1):𝑌⟶ℝ)
15429, 30, 153syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝐽‘1):𝑌⟶ℝ)
155154adantr 480 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → (𝐽‘1):𝑌⟶ℝ)
156 id 22 . . . . . . . . . . . . . . 15 (𝑌 = ∅ → 𝑌 = ∅)
157156eqcomd 2616 . . . . . . . . . . . . . 14 (𝑌 = ∅ → ∅ = 𝑌)
158157feq2d 5944 . . . . . . . . . . . . 13 (𝑌 = ∅ → ((𝐽‘1):∅⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
159158adantl 481 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → ((𝐽‘1):∅⟶ℝ ↔ (𝐽‘1):𝑌⟶ℝ))
160155, 159mpbird 246 . . . . . . . . . . 11 ((𝜑𝑌 = ∅) → (𝐽‘1):∅⟶ℝ)
161123feq1d 5943 . . . . . . . . . . . . . . . 16 (𝑗 = 1 → ((𝐾𝑗):𝑌⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
16233, 161imbi12d 333 . . . . . . . . . . . . . . 15 (𝑗 = 1 → (((𝜑𝑗 ∈ ℕ) → (𝐾𝑗):𝑌⟶ℝ) ↔ ((𝜑 ∧ 1 ∈ ℕ) → (𝐾‘1):𝑌⟶ℝ)))
16331, 162, 113vtocl 3232 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 ∈ ℕ) → (𝐾‘1):𝑌⟶ℝ)
16429, 30, 163syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝐾‘1):𝑌⟶ℝ)
165164adantr 480 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → (𝐾‘1):𝑌⟶ℝ)
166157feq2d 5944 . . . . . . . . . . . . 13 (𝑌 = ∅ → ((𝐾‘1):∅⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
167166adantl 481 . . . . . . . . . . . 12 ((𝜑𝑌 = ∅) → ((𝐾‘1):∅⟶ℝ ↔ (𝐾‘1):𝑌⟶ℝ))
168165, 167mpbird 246 . . . . . . . . . . 11 ((𝜑𝑌 = ∅) → (𝐾‘1):∅⟶ℝ)
16918, 160, 168hoidmv0val 39473 . . . . . . . . . 10 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿‘∅)(𝐾‘1)) = 0)
170130, 169eqtrd 2644 . . . . . . . . 9 ((𝜑𝑌 = ∅) → ((𝐽‘1)(𝐿𝑌)(𝐾‘1)) = 0)
171121, 128, 1703eqtrd 2648 . . . . . . . 8 ((𝜑𝑌 = ∅) → Σ𝑗 ∈ {1} (𝑃𝑗) = 0)
172171oveq2d 6565 . . . . . . 7 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) = ((1 + 𝐸) · 0))
173 hoidmvlelem3.e . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ+)
174173rpred 11748 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
17527, 174readdcld 9948 . . . . . . . . . 10 (𝜑 → (1 + 𝐸) ∈ ℝ)
176175recnd 9947 . . . . . . . . 9 (𝜑 → (1 + 𝐸) ∈ ℂ)
177176mul01d 10114 . . . . . . . 8 (𝜑 → ((1 + 𝐸) · 0) = 0)
178177adantr 480 . . . . . . 7 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · 0) = 0)
179 eqidd 2611 . . . . . . 7 ((𝜑𝑌 = ∅) → 0 = 0)
180172, 178, 1793eqtrd 2648 . . . . . 6 ((𝜑𝑌 = ∅) → ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) = 0)
18122, 180breq12d 4596 . . . . 5 ((𝜑𝑌 = ∅) → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)) ↔ 0 ≤ 0))
1824, 181mpbird 246 . . . 4 ((𝜑𝑌 = ∅) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)))
183 oveq2 6557 . . . . . . . . 9 (𝑚 = 1 → (1...𝑚) = (1...1))
1841nnzi 11278 . . . . . . . . . . 11 1 ∈ ℤ
185 fzsn 12254 . . . . . . . . . . 11 (1 ∈ ℤ → (1...1) = {1})
186184, 185ax-mp 5 . . . . . . . . . 10 (1...1) = {1}
187186a1i 11 . . . . . . . . 9 (𝑚 = 1 → (1...1) = {1})
188183, 187eqtrd 2644 . . . . . . . 8 (𝑚 = 1 → (1...𝑚) = {1})
189188sumeq1d 14279 . . . . . . 7 (𝑚 = 1 → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) = Σ𝑗 ∈ {1} (𝑃𝑗))
190189oveq2d 6565 . . . . . 6 (𝑚 = 1 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗)))
191190breq2d 4595 . . . . 5 (𝑚 = 1 → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) ↔ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗))))
192191rspcev 3282 . . . 4 ((1 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ {1} (𝑃𝑗))) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
1932, 182, 192syl2anc 691 . . 3 ((𝜑𝑌 = ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
194 simpl 472 . . . 4 ((𝜑 ∧ ¬ 𝑌 = ∅) → 𝜑)
195 neqne 2790 . . . . 5 𝑌 = ∅ → 𝑌 ≠ ∅)
196195adantl 481 . . . 4 ((𝜑 ∧ ¬ 𝑌 = ∅) → 𝑌 ≠ ∅)
197 nfv 1830 . . . . . 6 𝑗(𝜑𝑌 ≠ ∅)
198184a1i 11 . . . . . 6 ((𝜑𝑌 ≠ ∅) → 1 ∈ ℤ)
199 nnuz 11599 . . . . . 6 ℕ = (ℤ‘1)
200115adantlr 747 . . . . . 6 (((𝜑𝑌 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,)+∞))
201 hoidmvlelem3.a . . . . . . . . . . . 12 (𝜑𝐴:𝑊⟶ℝ)
20267a1i 11 . . . . . . . . . . . 12 (𝜑𝑌𝑊)
203201, 202fssresd 5984 . . . . . . . . . . 11 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
204 hoidmvlelem3.b . . . . . . . . . . . 12 (𝜑𝐵:𝑊⟶ℝ)
205204, 202fssresd 5984 . . . . . . . . . . 11 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
20618, 59, 203, 205hoidmvcl 39472 . . . . . . . . . 10 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
20728, 206sseldi 3566 . . . . . . . . 9 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ ℝ)
2085, 207syl5eqel 2692 . . . . . . . 8 (𝜑𝐺 ∈ ℝ)
209 0red 9920 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
210 1rp 11712 . . . . . . . . . . . . 13 1 ∈ ℝ+
211210a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ+)
212211, 173jca 553 . . . . . . . . . . 11 (𝜑 → (1 ∈ ℝ+𝐸 ∈ ℝ+))
213 rpaddcl 11730 . . . . . . . . . . 11 ((1 ∈ ℝ+𝐸 ∈ ℝ+) → (1 + 𝐸) ∈ ℝ+)
214212, 213syl 17 . . . . . . . . . 10 (𝜑 → (1 + 𝐸) ∈ ℝ+)
215 rpgt0 11720 . . . . . . . . . 10 ((1 + 𝐸) ∈ ℝ+ → 0 < (1 + 𝐸))
216214, 215syl 17 . . . . . . . . 9 (𝜑 → 0 < (1 + 𝐸))
217209, 216gtned 10051 . . . . . . . 8 (𝜑 → (1 + 𝐸) ≠ 0)
218208, 175, 217redivcld 10732 . . . . . . 7 (𝜑 → (𝐺 / (1 + 𝐸)) ∈ ℝ)
219218adantr 480 . . . . . 6 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
220218ltpnfd 11831 . . . . . . . . . 10 (𝜑 → (𝐺 / (1 + 𝐸)) < +∞)
221220adantr 480 . . . . . . . . 9 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < +∞)
222 id 22 . . . . . . . . . . 11 ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞)
223222eqcomd 2616 . . . . . . . . . 10 ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
224223adantl 481 . . . . . . . . 9 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
225221, 224breqtrd 4609 . . . . . . . 8 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
226225adantlr 747 . . . . . . 7 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
227 simpl 472 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝜑𝑌 ≠ ∅))
228 simpr 476 . . . . . . . . . 10 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞)
229 nnex 10903 . . . . . . . . . . . 12 ℕ ∈ V
230229a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ℕ ∈ V)
231 icossicc 12131 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ (0[,]+∞)
232231, 115sseldi 3566 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ (0[,]+∞))
233 eqid 2610 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (𝑃𝑗)) = (𝑗 ∈ ℕ ↦ (𝑃𝑗))
234232, 233fmptd 6292 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑃𝑗)):ℕ⟶(0[,]+∞))
235234adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝑗 ∈ ℕ ↦ (𝑃𝑗)):ℕ⟶(0[,]+∞))
236230, 235sge0repnf 39279 . . . . . . . . . 10 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞))
237228, 236mpbird 246 . . . . . . . . 9 ((𝜑 ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
238237adantlr 747 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
239219adantr 480 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
240208adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ∈ ℝ)
241240adantlr 747 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ∈ ℝ)
242 simpr 476 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ)
24327, 173ltaddrpd 11781 . . . . . . . . . . . 12 (𝜑 → 1 < (1 + 𝐸))
244243adantr 480 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → 1 < (1 + 𝐸))
24559adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → 𝑌 ∈ Fin)
246 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → 𝑌 ≠ ∅)
247203adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → (𝐴𝑌):𝑌⟶ℝ)
248205adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ ∅) → (𝐵𝑌):𝑌⟶ℝ)
24918, 245, 246, 247, 248hoidmvn0val 39474 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
2505a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
251 fvres 6117 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌 → ((𝐴𝑌)‘𝑘) = (𝐴𝑘))
252 fvres 6117 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌 → ((𝐵𝑌)‘𝑘) = (𝐵𝑘))
253251, 252oveq12d 6567 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑌 → (((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
254253fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑘𝑌 → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
255254adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
256201adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝐴:𝑊⟶ℝ)
257 elun1 3742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑌𝑘 ∈ (𝑌 ∪ {𝑍}))
258257, 45syl6eleqr 2699 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑌𝑘𝑊)
259258adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝑘𝑊)
260256, 259ffvelrnd 6268 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐴𝑘) ∈ ℝ)
261204adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑌) → 𝐵:𝑊⟶ℝ)
262261, 259ffvelrnd 6268 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐵𝑘) ∈ ℝ)
263 volico 38876 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
264260, 262, 263syl2anc 691 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
265 hoidmvlelem3.lt . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑊) → (𝐴𝑘) < (𝐵𝑘))
266259, 265syldan 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑌) → (𝐴𝑘) < (𝐵𝑘))
267266iftrued 4044 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑌) → if((𝐴𝑘) < (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
268255, 264, 2673eqtrd 2648 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑌) → (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
269268prodeq2dv 14492 . . . . . . . . . . . . . . . 16 (𝜑 → ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))) = ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)))
270269eqcomd 2616 . . . . . . . . . . . . . . 15 (𝜑 → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
271270adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ ∅) → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑌 (vol‘(((𝐴𝑌)‘𝑘)[,)((𝐵𝑌)‘𝑘))))
272249, 250, 2713eqtr4d 2654 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → 𝐺 = ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)))
273 difrp 11744 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → ((𝐴𝑘) < (𝐵𝑘) ↔ ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+))
274260, 262, 273syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑌) → ((𝐴𝑘) < (𝐵𝑘) ↔ ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+))
275266, 274mpbid 221 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑌) → ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
27659, 275fprodrpcl 14525 . . . . . . . . . . . . . 14 (𝜑 → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
277276adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → ∏𝑘𝑌 ((𝐵𝑘) − (𝐴𝑘)) ∈ ℝ+)
278272, 277eqeltrd 2688 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → 𝐺 ∈ ℝ+)
279214adantr 480 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → (1 + 𝐸) ∈ ℝ+)
280278, 279ltdivgt1 38513 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → (1 < (1 + 𝐸) ↔ (𝐺 / (1 + 𝐸)) < 𝐺))
281244, 280mpbid 221 . . . . . . . . . 10 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) < 𝐺)
282281adantr 480 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) < 𝐺)
283 hoidmvlelem3.i2 . . . . . . . . . . . . . . . . . . . . 21 (𝜑X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
284283adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
285 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑘) ∈ V
286285a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑥𝑘) ∈ V)
287 hoidmvlelem3.s . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑆𝑈)
288287elexd 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑆 ∈ V)
289286, 288ifcld 4081 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
290289ralrimivw 2950 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
292 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))
293292fnmpt 5933 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑘𝑊 if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊)
294291, 293syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊)
295 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
296 mptexg 6389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑊 ∈ Fin → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
29754, 296syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
298297adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V)
299 hoidmvlelem3.o . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑂 = (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ↦ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
300299fvmpt2 6200 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) ∈ V) → (𝑂𝑥) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
301295, 298, 300syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
302301fneq1d 5895 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥) Fn 𝑊 ↔ (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) Fn 𝑊))
303294, 302mpbird 246 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) Fn 𝑊)
304 nfv 1830 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝜑
305 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘𝑥
306 nfixp1 7814 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))
307305, 306nfel 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))
308304, 307nfan 1816 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
309301fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
310309adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
311 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘𝑊) → 𝑘𝑊)
312289adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘𝑊) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
313292fvmpt2 6200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘𝑊 ∧ if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
314311, 312, 313syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘𝑊) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
315314adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
316310, 315eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
317 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘𝑌 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
318317adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
319 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑥 ∈ V
320319elixp 7801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ↔ (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
321320simprbi 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) → ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
322321adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
323 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → 𝑘𝑌)
324 rspa 2914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑘𝑌 (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
325322, 323, 324syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
326325ad4ant24 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
327318, 326eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
328 snidg 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
32948, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑍 ∈ {𝑍})
330 elun2 3743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
331329, 330syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
33256a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑌 ∪ {𝑍}) = 𝑊)
333331, 332eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑍𝑊)
334201, 333ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐴𝑍) ∈ ℝ)
335334rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴𝑍) ∈ ℝ*)
336204, 333ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐵𝑍) ∈ ℝ)
337336rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐵𝑍) ∈ ℝ*)
338 iccssxr 12127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ*
339 hoidmvlelem3.u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
340 ssrab2 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
341339, 340eqsstri 3598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
342341, 287sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
343338, 342sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑆 ∈ ℝ*)
344 iccgelb 12101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑆)
345335, 337, 342, 344syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴𝑍) ≤ 𝑆)
346 hoidmvlelem3.sb . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑆 < (𝐵𝑍))
347335, 337, 343, 345, 346elicod 12095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
348347ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → 𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
349 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑌 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = 𝑆)
350349adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = 𝑆)
35145eleq2i 2680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘𝑊𝑘 ∈ (𝑌 ∪ {𝑍}))
352351biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘𝑊𝑘 ∈ (𝑌 ∪ {𝑍}))
353352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 ∈ (𝑌 ∪ {𝑍}))
354 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → ¬ 𝑘𝑌)
355 elunnel1 3716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘 ∈ (𝑌 ∪ {𝑍}) ∧ ¬ 𝑘𝑌) → 𝑘 ∈ {𝑍})
356353, 354, 355syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 ∈ {𝑍})
357 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
358356, 357syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → 𝑘 = 𝑍)
359 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
360 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
361359, 360oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
362358, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘𝑊 ∧ ¬ 𝑘𝑌) → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
363362adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
364350, 363eleq12d 2682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → (if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)) ↔ 𝑆 ∈ ((𝐴𝑍)[,)(𝐵𝑍))))
365348, 364mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
366365adantllr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) ∧ ¬ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
367327, 366pm2.61dan 828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
368316, 367eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
369368ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑘𝑊 → ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
370308, 369ralrimi 2940 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
371303, 370jca 553 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
372 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (𝑂𝑥) ∈ V
373372elixp 7801 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂𝑥) ∈ X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)) ↔ ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))))
374371, 373sylibr 223 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) ∈ X𝑘𝑊 ((𝐴𝑘)[,)(𝐵𝑘)))
375284, 374sseldd 3569 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑂𝑥) ∈ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
376 eliun 4460 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑥) ∈ 𝑗 ∈ ℕ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
377375, 376sylib 207 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
378 ixpfn 7800 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) → 𝑥 Fn 𝑌)
379378adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥 Fn 𝑌)
380379ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑥 Fn 𝑌)
381 nfv 1830 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 𝑗 ∈ ℕ
382308, 381nfan 1816 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ)
383 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘(𝑂𝑥)
384 nfixp1 7814 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
385383, 384nfel 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘(𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
386382, 385nfan 1816 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
3873093adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘))
388289adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) ∈ V)
389259, 388, 313syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘𝑌) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
3903893adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑘) = if(𝑘𝑌, (𝑥𝑘), 𝑆))
3913173ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = (𝑥𝑘))
392387, 390, 3913eqtrrd 2649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ∧ 𝑘𝑌) → (𝑥𝑘) = ((𝑂𝑥)‘𝑘))
393392ad5ant125 1304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) = ((𝑂𝑥)‘𝑘))
394 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
395372elixp 7801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
396394, 395sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥) Fn 𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
397396simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
398258adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → 𝑘𝑊)
399 rspa 2914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑊) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
400397, 398, 399syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
401400adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
402393, 401eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
40329ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝜑)
40437ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑗 ∈ ℕ)
405301fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑂𝑥)‘𝑍) = ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍))
406 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)) = (𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆)))
407 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 = 𝑍 → (𝑘𝑌𝑍𝑌))
408 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 = 𝑍 → (𝑥𝑘) = (𝑥𝑍))
409407, 408ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 = 𝑍 → if(𝑘𝑌, (𝑥𝑘), 𝑆) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
410409adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 = 𝑍) → if(𝑘𝑌, (𝑥𝑘), 𝑆) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
411 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥𝑍) ∈ V
412411a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (𝑥𝑍) ∈ V)
413412, 288ifcld 4081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → if(𝑍𝑌, (𝑥𝑍), 𝑆) ∈ V)
414406, 410, 333, 413fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
415414adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ((𝑘𝑊 ↦ if(𝑘𝑌, (𝑥𝑘), 𝑆))‘𝑍) = if(𝑍𝑌, (𝑥𝑍), 𝑆))
41648eldifbd 3553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ¬ 𝑍𝑌)
417416iffalsed 4047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(𝑍𝑌, (𝑥𝑍), 𝑆) = 𝑆)
418417adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → if(𝑍𝑌, (𝑥𝑍), 𝑆) = 𝑆)
419405, 415, 4183eqtrrd 2649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑆 = ((𝑂𝑥)‘𝑍))
420419ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑆 = ((𝑂𝑥)‘𝑍))
421403, 333syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑍𝑊)
422395simprbi 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
423422adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
424 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝑍 → ((𝑂𝑥)‘𝑘) = ((𝑂𝑥)‘𝑍))
425 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
426 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
427425, 426oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
428424, 427eleq12d 2682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝑍 → (((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
429428rspcva 3280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑍𝑊 ∧ ∀𝑘𝑊 ((𝑂𝑥)‘𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
430421, 423, 429syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝑂𝑥)‘𝑍) ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
431420, 430eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
4321503adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹))
433613ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = ((𝐶𝑗) ↾ 𝑌))
434432, 433eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐽𝑗) = ((𝐶𝑗) ↾ 𝑌))
435434fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
436403, 404, 431, 435syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
437436adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐽𝑗)‘𝑘) = (((𝐶𝑗) ↾ 𝑌)‘𝑘))
438 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑌 → (((𝐶𝑗) ↾ 𝑌)‘𝑘) = ((𝐶𝑗)‘𝑘))
439438adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐶𝑗) ↾ 𝑌)‘𝑘) = ((𝐶𝑗)‘𝑘))
440437, 439eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐽𝑗)‘𝑘) = ((𝐶𝑗)‘𝑘))
441108elexd 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ V)
442109fvmpt2 6200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
443140, 441, 442syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
4444433adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹))
445943ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = ((𝐷𝑗) ↾ 𝑌))
446444, 445eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝐾𝑗) = ((𝐷𝑗) ↾ 𝑌))
447446fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
448403, 404, 431, 447syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
449448adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐾𝑗)‘𝑘) = (((𝐷𝑗) ↾ 𝑌)‘𝑘))
450 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑌 → (((𝐷𝑗) ↾ 𝑌)‘𝑘) = ((𝐷𝑗)‘𝑘))
451450adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐷𝑗) ↾ 𝑌)‘𝑘) = ((𝐷𝑗)‘𝑘))
452449, 451eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → ((𝐾𝑗)‘𝑘) = ((𝐷𝑗)‘𝑘))
453440, 452oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
454453eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
455402, 454eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑌) → (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
456455ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑌 → (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
457386, 456ralrimi 2940 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
458380, 457jca 553 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
459319elixp 7801 . . . . . . . . . . . . . . . . . . . . 21 (𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ (𝑥 Fn 𝑌 ∧ ∀𝑘𝑌 (𝑥𝑘) ∈ (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
460458, 459sylibr 223 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) ∧ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
461460ex 449 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) ∧ 𝑗 ∈ ℕ) → ((𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
462461reximdva 3000 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → (∃𝑗 ∈ ℕ (𝑂𝑥) ∈ X𝑘𝑊 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
463377, 462mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
464 eliun 4460 . . . . . . . . . . . . . . . . 17 (𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑥X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
465463, 464sylibr 223 . . . . . . . . . . . . . . . 16 ((𝜑𝑥X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))) → 𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
466465ralrimiva 2949 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥X 𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
467 dfss3 3558 . . . . . . . . . . . . . . 15 (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) ↔ ∀𝑥X 𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘))𝑥 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
468466, 467sylibr 223 . . . . . . . . . . . . . 14 (𝜑X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
469 ovex 6577 . . . . . . . . . . . . . . . . . 18 (ℝ ↑𝑚 𝑌) ∈ V
470469a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ ↑𝑚 𝑌) ∈ V)
471229a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℕ ∈ V)
472470, 471elmapd 7758 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ↔ 𝐾:ℕ⟶(ℝ ↑𝑚 𝑌)))
473110, 472mpbird 246 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ))
474470, 471elmapd 7758 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ↔ 𝐽:ℕ⟶(ℝ ↑𝑚 𝑌)))
47590, 474mpbird 246 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ))
47683, 72elmapd 7758 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ (𝐵𝑌):𝑌⟶ℝ))
477205, 476mpbird 246 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌))
47883, 72elmapd 7758 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌) ↔ (𝐴𝑌):𝑌⟶ℝ))
479203, 478mpbird 246 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌))
480 hoidmvlelem3.i . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
481 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 = (𝐴𝑌) → (𝑒𝑘) = ((𝐴𝑌)‘𝑘))
482481adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → (𝑒𝑘) = ((𝐴𝑌)‘𝑘))
483251adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → ((𝐴𝑌)‘𝑘) = (𝐴𝑘))
484482, 483eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → (𝑒𝑘) = (𝐴𝑘))
485484oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑒 = (𝐴𝑌) ∧ 𝑘𝑌) → ((𝑒𝑘)[,)(𝑓𝑘)) = ((𝐴𝑘)[,)(𝑓𝑘)))
486485ixpeq2dva 7809 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = (𝐴𝑌) → X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) = X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)))
487486sseq1d 3595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐴𝑌) → (X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
488 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = (𝐴𝑌) → (𝑒(𝐿𝑌)𝑓) = ((𝐴𝑌)(𝐿𝑌)𝑓))
489488breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐴𝑌) → ((𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
490487, 489imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐴𝑌) → ((X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
491490ralbidv 2969 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐴𝑌) → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
492491ralbidv 2969 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝐴𝑌) → (∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
493492ralbidv 2969 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝐴𝑌) → (∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
494493rspcva 3280 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑌) ∈ (ℝ ↑𝑚 𝑌) ∧ ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝑒𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → (𝑒(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
495479, 480, 494syl2anc 691 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
496 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (𝐵𝑌) → (𝑓𝑘) = ((𝐵𝑌)‘𝑘))
497496adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → (𝑓𝑘) = ((𝐵𝑌)‘𝑘))
498252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → ((𝐵𝑌)‘𝑘) = (𝐵𝑘))
499497, 498eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → (𝑓𝑘) = (𝐵𝑘))
500499oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 = (𝐵𝑌) ∧ 𝑘𝑌) → ((𝐴𝑘)[,)(𝑓𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
501500ixpeq2dva 7809 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝐵𝑌) → X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) = X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)))
502501sseq1d 3595 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝐵𝑌) → (X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
503 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝐵𝑌) → ((𝐴𝑌)(𝐿𝑌)𝑓) = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)))
504503breq1d 4593 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝐵𝑌) → (((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
505502, 504imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝐵𝑌) → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
506505ralbidv 2969 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝐵𝑌) → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
507506ralbidv 2969 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝐵𝑌) → (∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))))
508507rspcva 3280 . . . . . . . . . . . . . . . . 17 (((𝐵𝑌) ∈ (ℝ ↑𝑚 𝑌) ∧ ∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝑓𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
509477, 495, 508syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))))
510 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = 𝐽 → (𝑔𝑗) = (𝐽𝑗))
511510fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝐽 → ((𝑔𝑗)‘𝑘) = ((𝐽𝑗)‘𝑘))
512511oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝐽 → (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
513512ixpeq2dv 7810 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝐽X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
514513iuneq2d 4483 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝐽 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)))
515514sseq2d 3596 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝐽 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘))))
516510oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝐽 → ((𝑔𝑗)(𝐿𝑌)(𝑗)) = ((𝐽𝑗)(𝐿𝑌)(𝑗)))
517516mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝐽 → (𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))
518517fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝐽 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))
519518breq2d 4595 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝐽 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
520515, 519imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝐽 → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))))
521520ralbidv 2969 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝐽 → (∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗))))) ↔ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))))
522521rspcva 3280 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ∧ ∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝑔𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔𝑗)(𝐿𝑌)(𝑗)))))) → ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
523475, 509, 522syl2anc 691 . . . . . . . . . . . . . . 15 (𝜑 → ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))))
524 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝐾 → (𝑗) = (𝐾𝑗))
525524fveq1d 6105 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝐾 → ((𝑗)‘𝑘) = ((𝐾𝑗)‘𝑘))
526525oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 ( = 𝐾 → (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
527526ixpeq2dv 7810 . . . . . . . . . . . . . . . . . . 19 ( = 𝐾X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
528527iuneq2d 4483 . . . . . . . . . . . . . . . . . 18 ( = 𝐾 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)))
529528sseq2d 3596 . . . . . . . . . . . . . . . . 17 ( = 𝐾 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) ↔ X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘))))
530524oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 ( = 𝐾 → ((𝐽𝑗)(𝐿𝑌)(𝑗)) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
531530mpteq2dv 4673 . . . . . . . . . . . . . . . . . . 19 ( = 𝐾 → (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))
532531fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ( = 𝐾 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
533532breq2d 4595 . . . . . . . . . . . . . . . . 17 ( = 𝐾 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
534529, 533imbi12d 333 . . . . . . . . . . . . . . . 16 ( = 𝐾 → ((X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗))))) ↔ (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))))
535534rspcva 3280 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ) ∧ ∀ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝑗)))))) → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
536473, 523, 535syl2anc 691 . . . . . . . . . . . . . 14 (𝜑 → (X𝑘𝑌 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑌 (((𝐽𝑗)‘𝑘)[,)((𝐾𝑗)‘𝑘)) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
537468, 536mpd 15 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
538 idd 24 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
539537, 538mpd 15 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
540539adantr 480 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
54142adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑌 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))
542541mpteq2dva 4672 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ ∅) → (𝑗 ∈ ℕ ↦ (𝑃𝑗)) = (𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))
543542fveq2d 6107 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ ∅) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)))))
544250, 543breq12d 4596 . . . . . . . . . . 11 ((𝜑𝑌 ≠ ∅) → (𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ↔ ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))))))
545540, 544mpbird 246 . . . . . . . . . 10 ((𝜑𝑌 ≠ ∅) → 𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
546545adantr 480 . . . . . . . . 9 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → 𝐺 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
547239, 241, 242, 282, 546ltletrd 10076 . . . . . . . 8 (((𝜑𝑌 ≠ ∅) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) ∈ ℝ) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
548227, 238, 547syl2anc 691 . . . . . . 7 (((𝜑𝑌 ≠ ∅) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))) = +∞) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
549226, 548pm2.61dan 828 . . . . . 6 ((𝜑𝑌 ≠ ∅) → (𝐺 / (1 + 𝐸)) < (Σ^‘(𝑗 ∈ ℕ ↦ (𝑃𝑗))))
550197, 198, 199, 200, 219, 549sge0uzfsumgt 39337 . . . . 5 ((𝜑𝑌 ≠ ∅) → ∃𝑚 ∈ ℕ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
551218adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) ∈ ℝ)
552 fzfid 12634 . . . . . . . . . . . . 13 (𝜑 → (1...𝑚) ∈ Fin)
553 simpl 472 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑚)) → 𝜑)
554 elfznn 12241 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℕ)
555554adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑚)) → 𝑗 ∈ ℕ)
55628, 115sseldi 3566 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (𝑃𝑗) ∈ ℝ)
557553, 555, 556syl2anc 691 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑚)) → (𝑃𝑗) ∈ ℝ)
558552, 557fsumrecl 14312 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ∈ ℝ)
559558adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ∈ ℝ)
560 simpr 476 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
561551, 559, 560ltled 10064 . . . . . . . . . 10 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (𝐺 / (1 + 𝐸)) ≤ Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))
562208adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ∈ ℝ)
563214adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → (1 + 𝐸) ∈ ℝ+)
564562, 559, 563ledivmuld 11801 . . . . . . . . . 10 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ((𝐺 / (1 + 𝐸)) ≤ Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) ↔ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
565561, 564mpbid 221 . . . . . . . . 9 ((𝜑 ∧ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
566565ex 449 . . . . . . . 8 (𝜑 → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
567566adantr 480 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
568567adantlr 747 . . . . . 6 (((𝜑𝑌 ≠ ∅) ∧ 𝑚 ∈ ℕ) → ((𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
569568reximdva 3000 . . . . 5 ((𝜑𝑌 ≠ ∅) → (∃𝑚 ∈ ℕ (𝐺 / (1 + 𝐸)) < Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))))
570550, 569mpd 15 . . . 4 ((𝜑𝑌 ≠ ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
571194, 196, 570syl2anc 691 . . 3 ((𝜑 ∧ ¬ 𝑌 = ∅) → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
572193, 571pm2.61dan 828 . 2 (𝜑 → ∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
573443ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑋 ∈ Fin)
574473ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑌𝑋)
575483ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑍 ∈ (𝑋𝑌))
5762013ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐴:𝑊⟶ℝ)
5772043ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐵:𝑊⟶ℝ)
578633ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
579 eqid 2610 . . . . 5 (𝑦𝑌 ↦ 0) = (𝑦𝑌 ↦ 0)
580 eqid 2610 . . . . 5 (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0))) = (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
581963ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
582 eqid 2610 . . . . 5 (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0))) = (𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
583 fveq2 6103 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝐶𝑖) = (𝐶𝑗))
584 fveq2 6103 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝐷𝑖) = (𝐷𝑗))
585583, 584oveq12d 6567 . . . . . . . . 9 (𝑖 = 𝑗 → ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)) = ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
586585cbvmptv 4678 . . . . . . . 8 (𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
587586fveq2i 6106 . . . . . . 7 ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗))))
588 hoidmvlelem3.r . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
589587, 588syl5eqel 2692 . . . . . 6 (𝜑 → (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) ∈ ℝ)
5905893ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)(𝐷𝑖)))) ∈ ℝ)
591 hoidmvlelem3.h . . . . . 6 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
592 eleq1 2676 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗𝑌𝑖𝑌))
593 fveq2 6103 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑐𝑗) = (𝑐𝑖))
594593breq1d 4593 . . . . . . . . . . 11 (𝑗 = 𝑖 → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐𝑖) ≤ 𝑥))
595594, 593ifbieq1d 4059 . . . . . . . . . 10 (𝑗 = 𝑖 → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥))
596592, 593, 595ifbieq12d 4063 . . . . . . . . 9 (𝑗 = 𝑖 → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))
597596cbvmptv 4678 . . . . . . . 8 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))
598597mpteq2i 4669 . . . . . . 7 (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥))))
599598mpteq2i 4669 . . . . . 6 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))))
600591, 599eqtri 2632 . . . . 5 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑖𝑊 ↦ if(𝑖𝑌, (𝑐𝑖), if((𝑐𝑖) ≤ 𝑥, (𝑐𝑖), 𝑥)))))
6011733ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐸 ∈ ℝ+)
602 fveq2 6103 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
603 fveq2 6103 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
604603fveq2d 6107 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑧)‘(𝐷𝑖)))
605602, 604oveq12d 6567 . . . . . . . . . . . 12 (𝑗 = 𝑖 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))
606605cbvmptv 4678 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))
607606fveq2i 6106 . . . . . . . . . 10 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖)))))
608607oveq2i 6560 . . . . . . . . 9 ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))
609608breq2i 4591 . . . . . . . 8 ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖)))))))
610609a1i 11 . . . . . . 7 (𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))))
611610rabbiia 3161 . . . . . 6 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))}
612339, 611eqtri 2632 . . . . 5 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶𝑖)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑖))))))}
6132873ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑆𝑈)
6143463ad2ant1 1075 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑆 < (𝐵𝑍))
615 eqid 2610 . . . . 5 (𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖))) = (𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
616 simp2 1055 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝑚 ∈ ℕ)
617 id 22 . . . . . . . 8 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)))
618 fveq2 6103 . . . . . . . . . . 11 (𝑗 = 𝑖 → (𝑃𝑗) = (𝑃𝑖))
619618cbvsumv 14274 . . . . . . . . . 10 Σ𝑗 ∈ (1...𝑚)(𝑃𝑗) = Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)
620619oveq2i 6560 . . . . . . . . 9 ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖))
621620a1i 11 . . . . . . . 8 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
622617, 621breqtrd 4609 . . . . . . 7 (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
6236223ad2ant3 1077 . . . . . 6 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)))
624 simpl 472 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑚)) → 𝜑)
625 elfznn 12241 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ)
626625adantl 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ)
627 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ))
628 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐽𝑗) = (𝐽𝑖))
629 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐾𝑗) = (𝐾𝑖))
630628, 629oveq12d 6567 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
631618, 630eqeq12d 2625 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗)) ↔ (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖))))
632627, 631imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝑗 ∈ ℕ → (𝑃𝑗) = ((𝐽𝑗)(𝐿𝑌)(𝐾𝑗))) ↔ (𝑖 ∈ ℕ → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))))
633632, 42chvarv 2251 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
634633adantl 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)))
635627anbi2d 736 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑖 ∈ ℕ)))
636602fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
637603fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
638636, 637oveq12d 6567 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
639638eleq2d 2673 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
640602reseq1d 5316 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((𝐶𝑗) ↾ 𝑌) = ((𝐶𝑖) ↾ 𝑌))
641639, 640ifbieq1d 4059 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
642628, 641eqeq12d 2625 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹) ↔ (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)))
643635, 642imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ ℕ) → (𝐽𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐶𝑗) ↾ 𝑌), 𝐹)) ↔ ((𝜑𝑖 ∈ ℕ) → (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))))
644643, 150chvarv 2251 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝐽𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
645603reseq1d 5316 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((𝐷𝑗) ↾ 𝑌) = ((𝐷𝑖) ↾ 𝑌))
646639, 645ifbieq1d 4059 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
647629, 646eqeq12d 2625 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹) ↔ (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
648635, 647imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ ℕ) → (𝐾𝑗) = if(𝑆 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)), ((𝐷𝑗) ↾ 𝑌), 𝐹)) ↔ ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))))
649648, 443chvarv 2251 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
650644, 649oveq12d 6567 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝐽𝑖)(𝐿𝑌)(𝐾𝑖)) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
651634, 650eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
652 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
653 ovex 6577 . . . . . . . . . . . . . 14 (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) ∈ V
654653a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) ∈ V)
655615fvmpt2 6200 . . . . . . . . . . . . 13 ((𝑖 ∈ ℕ ∧ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) ∈ V) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
656652, 654, 655syl2anc 691 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))
657 fvex 6113 . . . . . . . . . . . . . . . . . . 19 (𝐶𝑖) ∈ V
658657resex 5363 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑖) ↾ 𝑌) ∈ V
659658a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐶𝑖) ↾ 𝑌) ∈ V)
66081, 144syl5eqelr 2693 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑦𝑌 ↦ 0) ∈ V)
661659, 660ifcld 4081 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
662661adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
663580fvmpt2 6200 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
664652, 662, 663syl2anc 691 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
66581eqcomi 2619 . . . . . . . . . . . . . . . 16 (𝑦𝑌 ↦ 0) = 𝐹
666 ifeq2 4041 . . . . . . . . . . . . . . . 16 ((𝑦𝑌 ↦ 0) = 𝐹 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
667665, 666ax-mp 5 . . . . . . . . . . . . . . 15 if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)
668667a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
669664, 668eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹))
670 fvex 6113 . . . . . . . . . . . . . . . . . . 19 (𝐷𝑖) ∈ V
671670resex 5363 . . . . . . . . . . . . . . . . . 18 ((𝐷𝑖) ↾ 𝑌) ∈ V
672671a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷𝑖) ↾ 𝑌) ∈ V)
673672, 660ifcld 4081 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
674673adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V)
675582fvmpt2 6200 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) ∈ V) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
676652, 674, 675syl2anc 691 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))
677 biid 250 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
678677, 665ifbieq2i 4060 . . . . . . . . . . . . . . 15 if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)
679678a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
680676, 679eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖) = if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹))
681669, 680oveq12d 6567 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
682656, 681eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖) = (if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), 𝐹)(𝐿𝑌)if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), 𝐹)))
683651, 682eqtr4d 2647 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
684624, 626, 683syl2anc 691 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑚)) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
6856843ad2antl1 1216 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) ∧ 𝑖 ∈ (1...𝑚)) → (𝑃𝑖) = ((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
686685sumeq2dv 14281 . . . . . . 7 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → Σ𝑖 ∈ (1...𝑚)(𝑃𝑖) = Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖))
687686oveq2d 6565 . . . . . 6 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)(𝑃𝑖)) = ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖)))
688623, 687breqtrd 4609 . . . . 5 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → 𝐺 ≤ ((1 + 𝐸) · Σ𝑖 ∈ (1...𝑚)((𝑖 ∈ ℕ ↦ (((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐶𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)(𝐿𝑌)((𝑖 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)), ((𝐷𝑖) ↾ 𝑌), (𝑦𝑌 ↦ 0)))‘𝑖)))‘𝑖)))
689 fveq2 6103 . . . . . . . 8 (𝑗 = → (𝐷𝑗) = (𝐷))
690689fveq1d 6105 . . . . . . 7 (𝑗 = → ((𝐷𝑗)‘𝑍) = ((𝐷)‘𝑍))
691690cbvmptv 4678 . . . . . 6 (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ( ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷)‘𝑍))
692691rneqi 5273 . . . . 5 ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ran ( ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷)‘𝑍))
693 fveq2 6103 . . . . . . . . . . . 12 ( = 𝑖 → (𝐶) = (𝐶𝑖))
694693fveq1d 6105 . . . . . . . . . . 11 ( = 𝑖 → ((𝐶)‘𝑍) = ((𝐶𝑖)‘𝑍))
695 fveq2 6103 . . . . . . . . . . . 12 ( = 𝑖 → (𝐷) = (𝐷𝑖))
696695fveq1d 6105 . . . . . . . . . . 11 ( = 𝑖 → ((𝐷)‘𝑍) = ((𝐷𝑖)‘𝑍))
697694, 696oveq12d 6567 . . . . . . . . . 10 ( = 𝑖 → (((𝐶)‘𝑍)[,)((𝐷)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
698697eleq2d 2673 . . . . . . . . 9 ( = 𝑖 → (𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍)) ↔ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
699698cbvrabv 3172 . . . . . . . 8 { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} = {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))}
700699mpteq1i 4667 . . . . . . 7 (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))
701700rneqi 5273 . . . . . 6 ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)) = ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))
702701uneq2i 3726 . . . . 5 ({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))) = ({(𝐵𝑍)} ∪ ran (𝑗 ∈ {𝑖 ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍)))
703 eqid 2610 . . . . 5 inf(({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))), ℝ, < ) = inf(({(𝐵𝑍)} ∪ ran (𝑗 ∈ { ∈ (1...𝑚) ∣ 𝑆 ∈ (((𝐶)‘𝑍)[,)((𝐷)‘𝑍))} ↦ ((𝐷𝑗)‘𝑍))), ℝ, < )
70418, 573, 574, 575, 45, 576, 577, 578, 579, 580, 581, 582, 590, 600, 5, 601, 612, 613, 614, 615, 616, 688, 692, 702, 703hoidmvlelem2 39486 . . . 4 ((𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗))) → ∃𝑢𝑈 𝑆 < 𝑢)
7057043exp 1256 . . 3 (𝜑 → (𝑚 ∈ ℕ → (𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢)))
706705rexlimdv 3012 . 2 (𝜑 → (∃𝑚 ∈ ℕ 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑚)(𝑃𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢))
707572, 706mpd 15 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  cdif 3537  cun 3538  wss 3540  c0 3874  ifcif 4036  {csn 4125   ciun 4455   class class class wbr 4583  cmpt 4643  ran crn 5039  cres 5040   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cmpt2 6551  𝑚 cmap 7744  Xcixp 7794  Fincfn 7841  infcinf 8230  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  *cxr 9952   < clt 9953  cle 9954  cmin 10145   / cdiv 10563  cn 10897  cz 11254  +crp 11708  [,)cico 12048  [,]cicc 12049  ...cfz 12197  Σcsu 14264  cprod 14474  volcvol 23039  Σ^csumge0 39255
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-inf2 8421  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  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  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-rmo 2904  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-int 4411  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-se 4998  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-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-sumge0 39256
This theorem is referenced by:  hoidmvlelem4  39488
  Copyright terms: Public domain W3C validator