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

Theorem hspmbllem2 43259
 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 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑋))
hspmbllem2.d (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑋))
hspmbllem2.a (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
hspmbllem2.g (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
hspmbllem2.r (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
hspmbllem2.i (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
hspmbllem2.f (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∈ ℝ)
hspmbllem2.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hspmbllem2.t 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
hspmbllem2.s 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ 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 10663 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (𝜑𝐸 ∈ ℝ+)
65rpred 12423 . . . 4 (𝜑𝐸 ∈ ℝ)
74, 6readdcld 10663 . . 3 (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8 nfv 1915 . . . 4 𝑗𝜑
9 nnex 11635 . . . . 5 ℕ ∈ V
109a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
11 icossicc 12818 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
12 hspmbllem2.l . . . . . 6 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
13 hspmbllem2.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
1413adantr 484 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15 hspmbllem2.c . . . . . . . 8 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑋))
1615ffvelrnda 6832 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑m 𝑋))
17 elmapi 8415 . . . . . . 7 ((𝐶𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
1816, 17syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
19 hspmbllem2.d . . . . . . . 8 (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑋))
2019ffvelrnda 6832 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑m 𝑋))
21 elmapi 8415 . . . . . . 7 ((𝐷𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
2220, 21syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
2312, 14, 18, 22hoidmvcl 43214 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
2411, 23sseldi 3916 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 43057 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (𝜑𝐾𝑋)
27 ne0i 4253 . . . . . . . . 9 (𝐾𝑋𝑋 ≠ ∅)
2826, 27syl 17 . . . . . . . 8 (𝜑𝑋 ≠ ∅)
2928adantr 484 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
3012, 14, 29, 18, 22hoidmvn0val 43216 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
3130mpteq2dva 5128 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))))
3231fveq2d 6653 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))))
33 hspmbllem2.g . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
3432, 33eqbrtrd 5055 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
357, 25, 34ge0lere 42162 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
3837adantr 484 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
3936, 38, 14, 22hsphoif 43208 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
4012, 14, 18, 39hoidmvcl 43214 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,)+∞))
4111, 40sseldi 3916 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 43057 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ (0[,]+∞))
43 oveq2 7147 . . . . . . . . . . 11 (𝑥 = 𝑦 → (ℝ ↑m 𝑥) = (ℝ ↑m 𝑦))
44 eqeq1 2805 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45 prodeq1 15259 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
4644, 45ifbieq2d 4453 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
4743, 43, 46mpoeq123dv 7212 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4847cbvmptv 5136 . . . . . . . . 9 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4912, 48eqtri 2824 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
50 diffi 8738 . . . . . . . . . . 11 (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52 snfi 8581 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (𝜑 → {𝐾} ∈ Fin)
54 unfi 8773 . . . . . . . . . 10 (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5655adantr 484 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57 snidg 4562 . . . . . . . . . . . 12 (𝐾𝑋𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝐾})
59 elun2 4107 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61 neldifsnd 4689 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
6260, 61eldifd 3895 . . . . . . . . 9 (𝜑𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
6362adantr 484 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64 eqid 2801 . . . . . . . 8 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65 eqid 2801 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
66 uncom 4083 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
6826snssd 4705 . . . . . . . . . . . . 13 (𝜑 → {𝐾} ⊆ 𝑋)
69 undif 4391 . . . . . . . . . . . . 13 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7068, 69sylib 221 . . . . . . . . . . . 12 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7167, 70eqtrd 2836 . . . . . . . . . . 11 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7271adantr 484 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7372feq2d 6477 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶𝑗):𝑋⟶ℝ))
7418, 73mpbird 260 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7572feq2d 6477 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷𝑗):𝑋⟶ℝ))
7622, 75mpbird 260 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 43218 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)))
7871fveq2d 6653 . . . . . . . . . 10 (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
79 eqidd 2802 . . . . . . . . . 10 (𝜑 → (𝐶𝑗) = (𝐶𝑗))
8036a1i 11 . . . . . . . . . . . . 13 (𝜑𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8171oveq2d 7155 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑m 𝑋))
8271mpteq1d 5122 . . . . . . . . . . . . . . . 16 (𝜑 → ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))
8381, 82mpteq12dv 5118 . . . . . . . . . . . . . . 15 (𝜑 → (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8483eqcomd 2807 . . . . . . . . . . . . . 14 (𝜑 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8584mpteq2dv 5129 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8680, 85eqtr2d 2837 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = 𝑇)
8786fveq1d 6651 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌) = (𝑇𝑌))
8887fveq1d 6651 . . . . . . . . . 10 (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗)) = ((𝑇𝑌)‘(𝐷𝑗)))
8978, 79, 88oveq123d 7160 . . . . . . . . 9 (𝜑 → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9089adantr 484 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9178adantr 484 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
9291oveqd 7156 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) = ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
9390, 92breq12d 5046 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) ↔ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))))
9477, 93mpbid 235 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
958, 10, 41, 24, 94sge0lempt 43042 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
9635, 42, 95ge0lere 42162 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
9897, 38, 14, 18hoidifhspf 43250 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
9912, 14, 98, 22hoidmvcl 43214 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
10099fmpttd 6860 . . . . . . 7 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
10111a1i 11 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102100, 101fssd 6506 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
10310, 102sge0cl 43013 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
10411, 99sseldi 3916 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
10526adantr 484 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐾𝑋)
10612, 14, 18, 22, 105, 97, 38hoidifhspdmvle 43252 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
1078, 10, 104, 24, 106sge0lempt 43042 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
10835, 103, 107ge0lere 42162 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
10937adantr 484 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
11013adantr 484 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111 eleq1w 2875 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112111anbi2d 631 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑙 ∈ ℕ)))
113 fveq2 6649 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
114113feq1d 6476 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝐷𝑗):𝑋⟶ℝ ↔ (𝐷𝑙):𝑋⟶ℝ))
115112, 114imbi12d 348 . . . . . . . . . 10 (𝑗 = 𝑙 → (((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ) ↔ ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)))
116115, 22chvarvv 2005 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)
11736, 109, 110, 116hsphoif 43208 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ)
118 reex 10621 . . . . . . . . . . . 12 ℝ ∈ V
119118a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ V)
120119, 13jca 515 . . . . . . . . . 10 (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121120adantr 484 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122 elmapg 8406 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
123121, 122syl 17 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
124117, 123mpbird 260 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋))
125124fmpttd 6860 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))):ℕ⟶(ℝ ↑m 𝑋))
126 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
127 elinel1 4125 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
128127adantl 485 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
129 hspmbllem2.a . . . . . . . . . . . . . 14 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
130129sselda 3918 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
131 eliun 4888 . . . . . . . . . . . . 13 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
132130, 131sylib 221 . . . . . . . . . . . 12 ((𝜑𝑓𝐴) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
133126, 128, 132syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
134 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135 elinel2 4126 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
136135adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
137136adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
138 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139 ixpfn 8454 . . . . . . . . . . . . . . . . 17 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140139adantl 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑘((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142 nfcv 2958 . . . . . . . . . . . . . . . . . . 19 𝑘𝑓
143 nfixp1 8469 . . . . . . . . . . . . . . . . . . 19 𝑘X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
144142, 143nfel 2972 . . . . . . . . . . . . . . . . . 18 𝑘 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
145141, 144nfan 1900 . . . . . . . . . . . . . . . . 17 𝑘(((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
146183adant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐶𝑗):𝑋⟶ℝ)
147 simp3 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑘𝑋)
148146, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
149148rexrd 10684 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
150149ad5ant135 1365 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
151393adant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
152151, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ)
153152rexrd 10684 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
154153ad5ant135 1365 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
155 iftrue 4434 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156 ioossre 12790 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)𝑌) ⊆ ℝ
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158155, 157eqsstrd 3956 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159 iffalse 4437 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160 ssid 3940 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162159, 161eqsstrd 3956 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163158, 162pm2.61i 185 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
165 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166165, 13, 26, 37hspval 43241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167166adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168164, 167eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169168adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑘𝑋)
171 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
172171elixp 8455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173172biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174173simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175174adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → 𝑘𝑋)
177 rspa 3174 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178175, 176, 177syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179169, 170, 178syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180163, 179sseldi 3916 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
181180rexrd 10684 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
182181ad4ant14 751 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
183149ad4ant124 1170 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
184223adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐷𝑗):𝑋⟶ℝ)
185184, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ)
186185rexrd 10684 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
187186ad4ant124 1170 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
188171elixp 8455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
189188biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
190189simprd 499 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
191190adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
192 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → 𝑘𝑋)
193 rspa 3174 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
194191, 192, 193syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
195194adantll 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
196 icogelb 12780 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
197183, 187, 195, 196syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
198197adantl3r 749 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
199 icoltub 42138 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
200183, 187, 195, 199syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
201200adantl3r 749 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
202201ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
203 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205203, 204jca 515 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
2062053ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝜑𝑗 ∈ ℕ))
207 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208 simp3 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) ≤ 𝑌)
209 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝐾))
210209breq1d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
211210biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) ≤ 𝑌)
212211iftrued 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝐾))
213209eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
214213adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
215212, 214eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
2162153adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
217 breq2 5037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌 → ((𝑐) ≤ 𝑦 ↔ (𝑐) ≤ 𝑌))
218 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌𝑦 = 𝑌)
219217, 218ifbieq2d 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑌 → if((𝑐) ≤ 𝑦, (𝑐), 𝑦) = if((𝑐) ≤ 𝑌, (𝑐), 𝑌))
220219ifeq2d 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑌 → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)) = if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))
221220mpteq2dv 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑌 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))))
222221mpteq2dv 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
223 ovex 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑m 𝑋) ∈ V
224223mptex 6967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V
225224a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V)
22636, 222, 37, 225fvmptd3 6772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
227226adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
228 fveq1 6648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → (𝑐) = ((𝐷𝑗)‘))
229228breq1d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (𝐷𝑗) → ((𝑐) ≤ 𝑌 ↔ ((𝐷𝑗)‘) ≤ 𝑌))
230229, 228ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → if((𝑐) ≤ 𝑌, (𝑐), 𝑌) = if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))
231228, 230ifeq12d 4448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (𝐷𝑗) → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)) = if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))
232231mpteq2dv 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (𝐷𝑗) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
233232adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷𝑗)) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
234 mptexg 6965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
23513, 234syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
236235adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
237227, 233, 20, 236fvmptd 6756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
238237fveq1d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
2392383adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
240 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝜑)
241 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝑘 = 𝐾)
242240, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝐾𝑋)
243241, 242eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝑘𝑋)
244 eqidd 2802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
245 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ( ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ((𝐷𝑗)‘) = ((𝐷𝑗)‘𝑘))
247246breq1d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = 𝑘 → (((𝐷𝑗)‘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝑘) ≤ 𝑌))
248247, 246ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌) = if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌))
249245, 246, 248ifbieq12d 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑘 → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
250249adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
251 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → 𝑘𝑋)
252 fvexd 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝐷𝑗)‘𝑘) ∈ V)
253 ifexg 4475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐷𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
254252, 37, 253syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
255 ifexg 4475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐷𝑗)‘𝑘) ∈ V ∧ if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
256252, 254, 255syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
257256adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
258244, 250, 251, 257fvmptd 6756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘𝑋) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
259240, 243, 258syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
260 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
261210, 209ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
262260, 209, 261ifbieq12d 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
263262adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
264259, 263eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
2652643adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
266 neldifsnd 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
267266iffalsed 4439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
2682673ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
269239, 265, 2683eqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2702693expa 1115 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2712703adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
272216, 271eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
273206, 207, 208, 272syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
274273ad5ant145 1366 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
275202, 274breqtrd 5059 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
276 mnfxr 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
277276a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → -∞ ∈ ℝ*)
27837rexrd 10684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑌 ∈ ℝ*)
279278adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑌 ∈ ℝ*)
2802793ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
2811793adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
2821553ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
283281, 282eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
284 iooltub 42140 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ*𝑌 ∈ ℝ* ∧ (𝑓𝑘) ∈ (-∞(,)𝑌)) → (𝑓𝑘) < 𝑌)
285277, 280, 283, 284syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
2862853adant1r 1174 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
287286ad4ant123 1169 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < 𝑌)
288 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌)
289210notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
290289adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
291288, 290mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌)
292291iffalsed 4439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = 𝑌)
293 eqidd 2802 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
294292, 293eqtr2d 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
295294adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
296270adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
297296adantl3r 749 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
298297adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
299295, 298eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
300287, 299breqtrd 5059 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
301300adantl3r 749 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
302275, 301pm2.61dan 812 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
303201adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
3042373adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
305249adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3062573adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
307304, 305, 147, 306fvmptd 6756 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3083073expa 1115 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
309308adantllr 718 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
310309ad4ant13 750 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
311 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘𝑋)
312 neqne 2998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘 = 𝐾𝑘𝐾)
313 nelsn 4568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘𝐾 → ¬ 𝑘 ∈ {𝐾})
314312, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
315314adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
316311, 315eldifd 3895 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
317316iftrued 4436 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
318317adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
319310, 318eqtr2d 2837 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
320303, 319breqtrd 5059 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
321302, 320pm2.61dan 812 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
322150, 154, 182, 198, 321elicod 12779 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
323322ex 416 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
324145, 323ralrimi 3183 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
325140, 324jca 515 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
326171elixp 8455 . . . . . . . . . . . . . . 15 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
327325, 326sylibr 237 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
328327ex 416 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
329134, 137, 138, 328syl21anc 836 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
330329reximdva 3236 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
331133, 330mpd 15 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
332 eliun 4888 . . . . . . . . . 10 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
333331, 332sylibr 237 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
334333ralrimiva 3152 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
335 dfss3 3906 . . . . . . . 8 ((𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
336334, 335sylibr 237 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
337 eqidd 2802 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))))
338 2fveq3 6654 . . . . . . . . . . . . 13 (𝑙 = 𝑗 → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
339338adantl 485 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
340 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
341 fvexd 6664 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝑇𝑌)‘(𝐷𝑗)) ∈ V)
342337, 339, 340, 341fvmptd 6756 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗) = ((𝑇𝑌)‘(𝐷𝑗)))
343342fveq1d 6651 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
344343oveq2d 7155 . . . . . . . . 9 (𝑗 ∈ ℕ → (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
345344ixpeq2dv 8464 . . . . . . . 8 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
346345iuneq2i 4905 . . . . . . 7 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
347336, 346sseqtrrdi 3969 . . . . . 6 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)))
34813, 15, 125, 347, 12ovnlecvr2 43242 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))))
349342oveq2d 7155 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
350349mpteq2ia 5124 . . . . . . 7 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
351350fveq2i 6652 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗)))))
352351a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
353348, 352breqtrd 5059 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
35415ffvelrnda 6832 . . . . . . . . . 10 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙) ∈ (ℝ ↑m 𝑋))
355 elmapi 8415 . . . . . . . . . 10 ((𝐶𝑙) ∈ (ℝ ↑m 𝑋) → (𝐶𝑙):𝑋⟶ℝ)
356354, 355syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙):𝑋⟶ℝ)
35797, 109, 110, 356hoidifhspf 43250 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ)
358 elmapg 8406 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
359120, 358syl 17 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
360359adantr 484 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
361357, 360mpbird 260 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋))
362361fmpttd 6860 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))):ℕ⟶(ℝ ↑m 𝑋))
363 simpl 486 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
364 eldifi 4057 . . . . . . . . . . . 12 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
365364adantl 485 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
366363, 365, 132syl2anc 587 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
367139adantl 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
368 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑘((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
369368, 144nfan 1900 . . . . . . . . . . . . . . . 16 𝑘(((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
370983adant3 1129 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
371370, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ)
372371rexrd 10684 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
373372ad5ant135 1365 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
374187adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
3751483expa 1115 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
3761863expa 1115 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
377 icossre 12810 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ*) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
378375, 376, 377syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
379378adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
380379, 195sseldd 3919 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
381380rexrd 10684 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
382381adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
383383adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑌 ∈ ℝ)
384143adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
38597, 383, 384, 146, 147hoidifhspval3 43251 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
386385ad5ant134 1364 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
387 iftrue 4434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
388387adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
389386, 388eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
390389adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
391 iftrue 4434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
392391adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
393197adantl3r 749 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
394393ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
395392, 394eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
396 iffalse 4437 . . . . . . . . . . . . . . . . . . . . . . 23 𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
397396adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
398 simpl1 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))))
399 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝑘))
400 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝐾 → (𝑓𝑘) = (𝑓𝐾))
401400breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑌 ≤ (𝑓𝑘) ↔ 𝑌 ≤ (𝑓𝐾)))
402401notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
403402adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
404399, 403mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
4054043ad2antl3 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
406400eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑓𝐾) = (𝑓𝑘))
4074063ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) = (𝑓𝑘))
408366adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
409 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
410409ad4ant13 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝜑𝑗 ∈ ℕ))
411 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
412251ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑘𝑋)
413410, 411, 412, 380syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) ∈ ℝ)
414413rexlimdva2 3249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
415414adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
416408, 415mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
4174163adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
418407, 417eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) ∈ ℝ)
419418adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) ∈ ℝ)
420398, 363, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑌 ∈ ℝ)
421419, 420ltnled 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ((𝑓𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
422405, 421mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) < 𝑌)
423367, 366r19.29a 3251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 Fn 𝑋)
424423adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → 𝑓 Fn 𝑋)
425276a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ*)
426278ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
427416ad4ant13 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
428427mnfltd 12511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓𝑘))
429400adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) = (𝑓𝐾))
430 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝐾) < 𝑌)
431429, 430eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
432431ad4ant24 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
433425, 426, 427, 428, 432eliood 42128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
434155eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435434adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
436433, 435eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437416ad4ant13 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
438159eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439438adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440437, 439eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441436, 440pm2.61dan 812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
442441ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
443424, 442jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
444398, 422, 443syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
445444, 172sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
446166eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
447446ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
4484473ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
449445, 448eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
450 eldifn 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
451450adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
4524513ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
453452adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
454449, 453condan 817 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
455454ad5ant145 1366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
456455adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → 𝑌 ≤ (𝑓𝑘))
457397, 456eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
458395, 457pm2.61dan 812 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
459390, 458eqbrtrd 5055 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
460385ad5ant124 1362 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
461 iffalse 4437 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
462461adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
463460, 462eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = ((𝐶𝑗)‘𝑘))
464197adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
465463, 464eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
466465adantl4r 754 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
467459, 466pm2.61dan 812 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
468200adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
469373, 374, 382, 467, 468elicod 12779 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
470469ex 416 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
471369, 470ralrimi 3183 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
472367, 471jca 515 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
473171elixp 8455 . . . . . . . . . . . . . 14 (𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
474472, 473sylibr 237 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
475 eqidd 2802 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))))
476 2fveq3 6654 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
477476adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
478 fvexd 6664 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((𝑆𝑌)‘(𝐶𝑗)) ∈ V)
479475, 477, 340, 478fvmptd 6756 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗) = ((𝑆𝑌)‘(𝐶𝑗)))
480479fveq1d 6651 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘) = (((𝑆𝑌)‘(𝐶𝑗))‘𝑘))
481480oveq1d 7154 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
482481ixpeq2dv 8464 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
483482ad2antlr 726 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
484483eleq2d 2878 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
485474, 484mpbird 260 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
486485ex 416 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
487486reximdva 3236 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
488366, 487mpd 15 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
489 eliun 4888 . . . . . . . . 9 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
490488, 489sylibr 237 . . . . . . . 8 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
491490ralrimiva 3152 . . . . . . 7 (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
492 dfss3 3906 . . . . . . 7 ((𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
493491, 492sylibr 237 . . . . . 6 (𝜑 → (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
49413, 362, 19, 493, 12ovnlecvr2 43242 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))))
495479oveq1d 7154 . . . . . . . 8 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
496495mpteq2ia 5124 . . . . . . 7 (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
497496fveq2i 6652 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
498497a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
499494, 498breqtrd 5059 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
5001, 2, 96, 108, 353, 499leadd12dd 41941 . . 3 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50114, 105, 38, 18, 22, 12, 36, 97hspmbllem1 43258 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
502501mpteq2dva 5128 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
503502fveq2d 6653 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
5048, 10, 41, 104sge0xadd 43067 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50596, 108rexaddd 12619 . . . 4 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
506503, 504, 5053eqtrrd 2841 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
507500, 506breqtrd 5059 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
5083, 35, 7, 507, 34letrd 10790 1 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ∖ cdif 3881   ∪ cun 3882   ∩ cin 3883   ⊆ wss 3884  ∅c0 4246  ifcif 4428  {csn 4528  ∪ ciun 4884   class class class wbr 5033   ↦ cmpt 5113   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141   ↑m cmap 8393  Xcixp 8448  Fincfn 8496  ℝcr 10529  0cc0 10530   + caddc 10533  +∞cpnf 10665  -∞cmnf 10666  ℝ*cxr 10667   < clt 10668   ≤ cle 10669  ℕcn 11629  ℝ+crp 12381   +𝑒 cxad 12497  (,)cioo 12730  [,)cico 12732  [,]cicc 12733  ∏cprod 15255  volcvol 24071  Σ^csumge0 42994  voln*covoln 43168 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-rlim 14842  df-sum 15039  df-prod 15256  df-rest 16692  df-topgen 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21503  df-topon 21520  df-bases 21555  df-cmp 21996  df-ovol 24072  df-vol 24073  df-sumge0 42995  df-ovoln 43169 This theorem is referenced by:  hspmbllem3  43260
 Copyright terms: Public domain W3C validator