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

Theorem hspmbllem2 41162
Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hspmbllem2.h 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
hspmbllem2.x (𝜑𝑋 ∈ Fin)
hspmbllem2.k (𝜑𝐾𝑋)
hspmbllem2.y (𝜑𝑌 ∈ ℝ)
hspmbllem2.e (𝜑𝐸 ∈ ℝ+)
hspmbllem2.c (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
hspmbllem2.d (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
hspmbllem2.a (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
hspmbllem2.g (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
hspmbllem2.r (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
hspmbllem2.i (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
hspmbllem2.f (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
hspmbllem2.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hspmbllem2.t 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
hspmbllem2.s 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
Assertion
Ref Expression
hspmbllem2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
Distinct variable groups:   𝐴,𝑗,𝑘   𝐶,𝑎,𝑏,𝑐,,𝑘,𝑙   𝐷,𝑎,𝑏,𝑐,,𝑗,𝑘,𝑙   𝑗,𝐻,𝑘   𝐾,𝑎,𝑏,𝑐,,𝑗,𝑘,𝑙,𝑥,𝑦   𝑆,𝑎,𝑏,𝑘,𝑙   𝑇,𝑎,𝑏,𝑘,𝑙   𝑋,𝑎,𝑏,𝑐,,𝑗,𝑘,𝑙,𝑥,𝑦   𝑌,𝑎,𝑏,𝑐,,𝑗,𝑘,𝑙,𝑥,𝑦   𝜑,𝑎,𝑏,𝑐,,𝑗,𝑘,𝑙,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦,,𝑎,𝑏,𝑐,𝑙)   𝐶(𝑥,𝑦,𝑗)   𝐷(𝑥,𝑦)   𝑆(𝑥,𝑦,,𝑗,𝑐)   𝑇(𝑥,𝑦,,𝑗,𝑐)   𝐸(𝑥,𝑦,,𝑗,𝑘,𝑎,𝑏,𝑐,𝑙)   𝐻(𝑥,𝑦,,𝑎,𝑏,𝑐,𝑙)   𝐿(𝑥,𝑦,,𝑗,𝑘,𝑎,𝑏,𝑐,𝑙)

Proof of Theorem hspmbllem2
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 hspmbllem2.i . . 3 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
2 hspmbllem2.f . . 3 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
31, 2readdcld 10107 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (𝜑𝐸 ∈ ℝ+)
65rpred 11910 . . . 4 (𝜑𝐸 ∈ ℝ)
74, 6readdcld 10107 . . 3 (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8 nfv 1883 . . . 4 𝑗𝜑
9 nnex 11064 . . . . 5 ℕ ∈ V
109a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
11 icossicc 12298 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
12 hspmbllem2.l . . . . . 6 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
13 hspmbllem2.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
1413adantr 480 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15 hspmbllem2.c . . . . . . . 8 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
1615ffvelrnda 6399 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
17 elmapi 7921 . . . . . . 7 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
1816, 17syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
19 hspmbllem2.d . . . . . . . 8 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
2019ffvelrnda 6399 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
21 elmapi 7921 . . . . . . 7 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
2220, 21syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
2312, 14, 18, 22hoidmvcl 41117 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
2411, 23sseldi 3634 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 40960 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (𝜑𝐾𝑋)
27 ne0i 3954 . . . . . . . . 9 (𝐾𝑋𝑋 ≠ ∅)
2826, 27syl 17 . . . . . . . 8 (𝜑𝑋 ≠ ∅)
2928adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
3012, 14, 29, 18, 22hoidmvn0val 41119 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
3130mpteq2dva 4777 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))))
3231fveq2d 6233 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))))
33 hspmbllem2.g . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
3432, 33eqbrtrd 4707 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
357, 25, 34ge0lere 40077 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
3837adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
3936, 38, 14, 22hsphoif 41111 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
4012, 14, 18, 39hoidmvcl 41117 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,)+∞))
4111, 40sseldi 3634 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 40960 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ (0[,]+∞))
43 oveq2 6698 . . . . . . . . . . 11 (𝑥 = 𝑦 → (ℝ ↑𝑚 𝑥) = (ℝ ↑𝑚 𝑦))
44 eqeq1 2655 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45 prodeq1 14683 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
4644, 45ifbieq2d 4144 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
4743, 43, 46mpt2eq123dv 6759 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4847cbvmptv 4783 . . . . . . . . 9 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4912, 48eqtri 2673 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
50 diffi 8233 . . . . . . . . . . 11 (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52 snfi 8079 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (𝜑 → {𝐾} ∈ Fin)
54 unfi 8268 . . . . . . . . . 10 (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 694 . . . . . . . . 9 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5655adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57 snidg 4239 . . . . . . . . . . . 12 (𝐾𝑋𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝐾})
59 elun2 3814 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61 neldifsnd 4355 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
6260, 61eldifd 3618 . . . . . . . . 9 (𝜑𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
6362adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64 eqid 2651 . . . . . . . 8 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65 eqid 2651 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
66 uncom 3790 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
6826snssd 4372 . . . . . . . . . . . . 13 (𝜑 → {𝐾} ⊆ 𝑋)
69 undif 4082 . . . . . . . . . . . . 13 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7068, 69sylib 208 . . . . . . . . . . . 12 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7167, 70eqtrd 2685 . . . . . . . . . . 11 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7271adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7372feq2d 6069 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶𝑗):𝑋⟶ℝ))
7418, 73mpbird 247 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7572feq2d 6069 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷𝑗):𝑋⟶ℝ))
7622, 75mpbird 247 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 41121 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)))
7871fveq2d 6233 . . . . . . . . . 10 (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
79 eqidd 2652 . . . . . . . . . 10 (𝜑 → (𝐶𝑗) = (𝐶𝑗))
8036a1i 11 . . . . . . . . . . . . 13 (𝜑𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8171oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑𝑚 𝑋))
8271mpteq1d 4771 . . . . . . . . . . . . . . . 16 (𝜑 → ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))
8381, 82mpteq12dv 4766 . . . . . . . . . . . . . . 15 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8483eqcomd 2657 . . . . . . . . . . . . . 14 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8584mpteq2dv 4778 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8680, 85eqtr2d 2686 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = 𝑇)
8786fveq1d 6231 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌) = (𝑇𝑌))
8887fveq1d 6231 . . . . . . . . . 10 (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗)) = ((𝑇𝑌)‘(𝐷𝑗)))
8978, 79, 88oveq123d 6711 . . . . . . . . 9 (𝜑 → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9089adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9178adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
9291oveqd 6707 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) = ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
9390, 92breq12d 4698 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) ↔ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))))
9477, 93mpbid 222 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
958, 10, 41, 24, 94sge0lempt 40945 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
9635, 42, 95ge0lere 40077 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
9897, 38, 14, 18hoidifhspf 41153 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
9912, 14, 98, 22hoidmvcl 41117 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
100 eqid 2651 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
10199, 100fmptd 6425 . . . . . . 7 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
10211a1i 11 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
103101, 102fssd 6095 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
10410, 103sge0cl 40916 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
10511, 99sseldi 3634 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
10626adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐾𝑋)
10712, 14, 18, 22, 106, 97, 38hoidifhspdmvle 41155 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
1088, 10, 105, 24, 107sge0lempt 40945 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
10935, 104, 108ge0lere 40077 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
11037adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
11113adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
112 eleq1 2718 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
113112anbi2d 740 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑙 ∈ ℕ)))
114 fveq2 6229 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
115114feq1d 6068 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝐷𝑗):𝑋⟶ℝ ↔ (𝐷𝑙):𝑋⟶ℝ))
116113, 115imbi12d 333 . . . . . . . . . 10 (𝑗 = 𝑙 → (((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ) ↔ ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)))
117116, 22chvarv 2299 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)
11836, 110, 111, 117hsphoif 41111 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ)
119 reex 10065 . . . . . . . . . . . 12 ℝ ∈ V
120119a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ V)
121120, 13jca 553 . . . . . . . . . 10 (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122121adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
123 elmapg 7912 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
124122, 123syl 17 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
125118, 124mpbird 247 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋))
126 eqid 2651 . . . . . . 7 (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))
127125, 126fmptd 6425 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
128 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
129 elinel1 3832 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
130129adantl 481 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
131 hspmbllem2.a . . . . . . . . . . . . . 14 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
132131sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
133 eliun 4556 . . . . . . . . . . . . 13 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
134132, 133sylib 208 . . . . . . . . . . . 12 ((𝜑𝑓𝐴) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
135128, 130, 134syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
136128adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
137 elinel2 3833 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
138137adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
139138adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
140 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
141 ixpfn 7956 . . . . . . . . . . . . . . . . 17 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
142141adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
143 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑘((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
144 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑘𝑓
145 nfixp1 7970 . . . . . . . . . . . . . . . . . . 19 𝑘X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
146144, 145nfel 2806 . . . . . . . . . . . . . . . . . 18 𝑘 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
147143, 146nfan 1868 . . . . . . . . . . . . . . . . 17 𝑘(((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
148183adant3 1101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐶𝑗):𝑋⟶ℝ)
149 simp3 1083 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑘𝑋)
150148, 149ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
151150rexrd 10127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
152151ad5ant135 1354 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
153393adant3 1101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
154153, 149ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ)
155154rexrd 10127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
156155ad5ant135 1354 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
157 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
158 ioossre 12273 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)𝑌) ⊆ ℝ
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
160157, 159eqsstrd 3672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
161 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
162 ssid 3657 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → ℝ ⊆ ℝ)
164161, 163eqsstrd 3672 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
165160, 164pm2.61i 176 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
166 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
167 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
168167, 13, 26, 37hspval 41144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169168adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170166, 169eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
171170adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
172 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑘𝑋)
173 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
174173elixp 7957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
175174biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
176175simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
177176adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → 𝑘𝑋)
179 rspa 2959 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180177, 178, 179syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
181171, 172, 180syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
182165, 181sseldi 3634 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
183182rexrd 10127 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
184183ad4ant14 1317 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
185151ad4ant124 1321 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
186223adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐷𝑗):𝑋⟶ℝ)
187186, 149ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ)
188187rexrd 10127 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
189188ad4ant124 1321 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
190173elixp 7957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
191190biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
192191simprd 478 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
193192adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
194 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → 𝑘𝑋)
195 rspa 2959 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
196193, 194, 195syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
197196adantll 750 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
198 icogelb 12263 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
199185, 189, 197, 198syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
200199ad5ant1345 1356 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
201 icoltub 40050 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
202185, 189, 197, 201syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
203202ad5ant1345 1356 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
204203ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
205 simpll 805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
206 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
207205, 206jca 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
2082073ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝜑𝑗 ∈ ℕ))
209 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
210 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) ≤ 𝑌)
211 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝐾))
212211breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
213212biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) ≤ 𝑌)
214213iftrued 4127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝐾))
215211eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
216215adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
217214, 216eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
2182173adant1 1099 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
219 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌 → ((𝑐) ≤ 𝑦 ↔ (𝑐) ≤ 𝑌))
220 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌𝑦 = 𝑌)
221219, 220ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌 → if((𝑐) ≤ 𝑦, (𝑐), 𝑦) = if((𝑐) ≤ 𝑌, (𝑐), 𝑌))
222221ifeq2d 4138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑌 → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)) = if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))
223222mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑌 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))))
224223mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
225224adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑦 = 𝑌) → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
226 ovex 6718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑𝑚 𝑋) ∈ V
227226mptex 6527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V)
22980, 225, 37, 228fvmptd 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
230229adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
231 fveq1 6228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → (𝑐) = ((𝐷𝑗)‘))
232231breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (𝐷𝑗) → ((𝑐) ≤ 𝑌 ↔ ((𝐷𝑗)‘) ≤ 𝑌))
233232, 231ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → if((𝑐) ≤ 𝑌, (𝑐), 𝑌) = if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))
234231, 233ifeq12d 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (𝐷𝑗) → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)) = if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))
235234mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (𝐷𝑗) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
236235adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷𝑗)) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
237 mptexg 6525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
23813, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
239238adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
240230, 236, 20, 239fvmptd 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
241240fveq1d 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
2422413adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
243 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝜑)
244 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝑘 = 𝐾)
245243, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝐾𝑋)
246244, 245eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝑘𝑋)
247 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
248 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ( ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
249 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ((𝐷𝑗)‘) = ((𝐷𝑗)‘𝑘))
250249breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = 𝑘 → (((𝐷𝑗)‘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝑘) ≤ 𝑌))
251250, 249ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌) = if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌))
252248, 249, 251ifbieq12d 4146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑘 → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
253252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
254 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → 𝑘𝑋)
255 fvexd 6241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝐷𝑗)‘𝑘) ∈ V)
256 ifexg 4190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐷𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
257255, 37, 256syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
258 ifexg 4190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐷𝑗)‘𝑘) ∈ V ∧ if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
259255, 257, 258syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
260259adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
261247, 253, 254, 260fvmptd 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘𝑋) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
262243, 246, 261syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
263 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
264212, 211ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
265263, 211, 264ifbieq12d 4146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
266265adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
267262, 266eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
2682673adant2 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
269 neldifsnd 4355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
270269iffalsed 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
2712703ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
272242, 268, 2713eqtrrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2732723expa 1284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2742733adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
275218, 274eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
276208, 209, 210, 275syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
277276ad5ant145 1355 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
278204, 277breqtrd 4711 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
279 mnfxr 10134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
280279a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → -∞ ∈ ℝ*)
28137rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑌 ∈ ℝ*)
282281adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑌 ∈ ℝ*)
2832823ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
2841813adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
2851573ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
286284, 285eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
287 iooltub 40053 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ*𝑌 ∈ ℝ* ∧ (𝑓𝑘) ∈ (-∞(,)𝑌)) → (𝑓𝑘) < 𝑌)
288280, 283, 286, 287syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
2892883adant1r 1359 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
290289ad4ant123 1319 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < 𝑌)
291 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌)
292212notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
293292adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
294291, 293mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌)
295294iffalsed 4130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = 𝑌)
296 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
297295, 296eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
298297adantll 750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
299273adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
300299adantlllr 39513 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
301300adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
302298, 301eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
303290, 302breqtrd 4711 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
304303ad5ant1345 1356 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
305278, 304pm2.61dan 849 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
306203adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
3072403adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
308252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3092603adant2 1100 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
310307, 308, 149, 309fvmptd 6327 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3113103expa 1284 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
312311adantllr 755 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
313312ad4ant13 1315 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
314 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘𝑋)
315 neqne 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘 = 𝐾𝑘𝐾)
316 nelsn 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘𝐾 → ¬ 𝑘 ∈ {𝐾})
317315, 316syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
318317adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
319314, 318eldifd 3618 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
320319iftrued 4127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
321320adantll 750 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
322313, 321eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
323306, 322breqtrd 4711 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
324305, 323pm2.61dan 849 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
325152, 156, 184, 200, 324elicod 12262 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
326325ex 449 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
327147, 326ralrimi 2986 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
328142, 327jca 553 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
329173elixp 7957 . . . . . . . . . . . . . . 15 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
330328, 329sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
331330ex 449 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
332136, 139, 140, 331syl21anc 1365 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
333332reximdva 3046 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
334135, 333mpd 15 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
335 eliun 4556 . . . . . . . . . 10 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
336334, 335sylibr 224 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
337336ralrimiva 2995 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
338 dfss3 3625 . . . . . . . 8 ((𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
339337, 338sylibr 224 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
340 eqidd 2652 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))))
341 fveq2 6229 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
342341fveq2d 6233 . . . . . . . . . . . . 13 (𝑙 = 𝑗 → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
343342adantl 481 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
344 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
345 fvexd 6241 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝑇𝑌)‘(𝐷𝑗)) ∈ V)
346340, 343, 344, 345fvmptd 6327 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗) = ((𝑇𝑌)‘(𝐷𝑗)))
347346fveq1d 6231 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
348347oveq2d 6706 . . . . . . . . 9 (𝑗 ∈ ℕ → (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
349348ixpeq2dv 7966 . . . . . . . 8 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
350349iuneq2i 4571 . . . . . . 7 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
351339, 350syl6sseqr 3685 . . . . . 6 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)))
35213, 15, 127, 351, 12ovnlecvr2 41145 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))))
353346oveq2d 6706 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
354353mpteq2ia 4773 . . . . . . 7 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
355354fveq2i 6232 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗)))))
356355a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
357352, 356breqtrd 4711 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
35815ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋))
359 elmapi 7921 . . . . . . . . . 10 ((𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑙):𝑋⟶ℝ)
360358, 359syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙):𝑋⟶ℝ)
36197, 110, 111, 360hoidifhspf 41153 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ)
362 elmapg 7912 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
363121, 362syl 17 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
364363adantr 480 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
365361, 364mpbird 247 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋))
366 eqid 2651 . . . . . . 7 (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))
367365, 366fmptd 6425 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
368 simpl 472 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
369 eldifi 3765 . . . . . . . . . . . 12 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
370369adantl 481 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
371368, 370, 134syl2anc 694 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
372141adantl 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
373 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑘((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
374373, 146nfan 1868 . . . . . . . . . . . . . . . 16 𝑘(((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
375983adant3 1101 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
376375, 149ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ)
377376rexrd 10127 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
378377ad5ant135 1354 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
379189adantl3r 801 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
3801503expa 1284 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
3811883expa 1284 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
382 icossre 12292 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ*) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
383380, 381, 382syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
384383adantlr 751 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
385384, 197sseldd 3637 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
386385rexrd 10127 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
387386ad5ant1345 1356 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
388383adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑌 ∈ ℝ)
389143adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
39097, 388, 389, 148, 149hoidifhspval3 41154 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
391390ad5ant134 1353 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
392 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
393392adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
394391, 393eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
395394adantllr 755 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
396 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
397396adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
398199adantl3r 801 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
399398ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
400397, 399eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
401 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . . 23 𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
402401adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
403 simpl1 1084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))))
404 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝑘))
405 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝐾 → (𝑓𝑘) = (𝑓𝐾))
406405breq2d 4697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑌 ≤ (𝑓𝑘) ↔ 𝑌 ≤ (𝑓𝐾)))
407406notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
408407adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
409404, 408mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
4104093ad2antl3 1245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
411405eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑓𝐾) = (𝑓𝑘))
4124113ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) = (𝑓𝑘))
413371adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
414 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
415414ad4ant13 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝜑𝑗 ∈ ℕ))
416 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
417254ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑘𝑋)
418415, 416, 417, 385syl21anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) ∈ ℝ)
419418ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
420419rexlimdva 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
421420adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
422413, 421mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
4234223adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
424412, 423eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) ∈ ℝ)
425424adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) ∈ ℝ)
426403, 368, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑌 ∈ ℝ)
427425, 426ltnled 10222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ((𝑓𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
428410, 427mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) < 𝑌)
429372, 371r19.29a 3107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 Fn 𝑋)
430429adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → 𝑓 Fn 𝑋)
431279a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ*)
432281ad4antr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
433422ad4ant13 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
434433mnfltd 11996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓𝑘))
435405adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) = (𝑓𝐾))
436 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝐾) < 𝑌)
437435, 436eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
438437ad4ant24 1327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
439431, 432, 433, 434, 438eliood 40038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
440157eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441440adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
442439, 441eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
443422ad4ant13 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
444161eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
445444adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
446443, 445eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
447442, 446pm2.61dan 849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
448447ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
449430, 448jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
450403, 428, 449syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
451450, 174sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
452168eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
453452ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
4544533ad2antl1 1243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
455451, 454eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
456 eldifn 3766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
457456adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
4584573ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
459458adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
460455, 459condan 852 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
461460ad5ant145 1355 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
462461adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → 𝑌 ≤ (𝑓𝑘))
463402, 462eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
464400, 463pm2.61dan 849 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
465395, 464eqbrtrd 4707 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
466390ad5ant124 1351 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
467 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
468467adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
469466, 468eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = ((𝐶𝑗)‘𝑘))
470199adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
471469, 470eqbrtrd 4707 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
472471adantl4r 802 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
473465, 472pm2.61dan 849 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
474202adantl3r 801 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
475378, 379, 387, 473, 474elicod 12262 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
476475ex 449 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
477374, 476ralrimi 2986 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
478372, 477jca 553 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
479173elixp 7957 . . . . . . . . . . . . . 14 (𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
480478, 479sylibr 224 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
481 eqidd 2652 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))))
482 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑗 → (𝐶𝑙) = (𝐶𝑗))
483482fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
484483adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
485 fvexd 6241 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((𝑆𝑌)‘(𝐶𝑗)) ∈ V)
486481, 484, 344, 485fvmptd 6327 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗) = ((𝑆𝑌)‘(𝐶𝑗)))
487486fveq1d 6231 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘) = (((𝑆𝑌)‘(𝐶𝑗))‘𝑘))
488487oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
489488ixpeq2dv 7966 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
490489ad2antlr 763 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
491490eleq2d 2716 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
492480, 491mpbird 247 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
493492ex 449 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
494493reximdva 3046 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
495371, 494mpd 15 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
496 eliun 4556 . . . . . . . . 9 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
497495, 496sylibr 224 . . . . . . . 8 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
498497ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
499 dfss3 3625 . . . . . . 7 ((𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
500498, 499sylibr 224 . . . . . 6 (𝜑 → (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
50113, 367, 19, 500, 12ovnlecvr2 41145 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))))
502486oveq1d 6705 . . . . . . . 8 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
503502mpteq2ia 4773 . . . . . . 7 (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
504503fveq2i 6232 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
505504a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
506501, 505breqtrd 4711 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
5071, 2, 96, 109, 357, 506leadd12dd 39845 . . 3 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50814, 106, 38, 18, 22, 12, 36, 97hspmbllem1 41161 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
509508mpteq2dva 4777 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
510509fveq2d 6233 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
5118, 10, 41, 105sge0xadd 40970 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
51296, 109rexaddd 12103 . . . 4 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
513510, 511, 5123eqtrrd 2690 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
514507, 513breqtrd 4711 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
5153, 35, 7, 514, 34letrd 10232 1 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  ifcif 4119  {csn 4210   ciun 4552   class class class wbr 4685  cmpt 4762   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  𝑚 cmap 7899  Xcixp 7950  Fincfn 7997  cr 9973  0cc0 9974   + caddc 9977  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112  cle 10113  cn 11058  +crp 11870   +𝑒 cxad 11982  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  cprod 14679  volcvol 23278  Σ^csumge0 40897  voln*covoln 41071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-prod 14680  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280  df-sumge0 40898  df-ovoln 41072
This theorem is referenced by:  hspmbllem3  41163
  Copyright terms: Public domain W3C validator