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 41320
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 10351 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (𝜑𝐸 ∈ ℝ+)
65rpred 12082 . . . 4 (𝜑𝐸 ∈ ℝ)
74, 6readdcld 10351 . . 3 (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8 nfv 2008 . . . 4 𝑗𝜑
9 nnex 11308 . . . . 5 ℕ ∈ V
109a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
11 icossicc 12475 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
12 hspmbllem2.l . . . . . 6 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
13 hspmbllem2.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
1413adantr 468 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15 hspmbllem2.c . . . . . . . 8 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
1615ffvelrnda 6578 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
17 elmapi 8111 . . . . . . 7 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
1816, 17syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
19 hspmbllem2.d . . . . . . . 8 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
2019ffvelrnda 6578 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
21 elmapi 8111 . . . . . . 7 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
2220, 21syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
2312, 14, 18, 22hoidmvcl 41275 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
2411, 23sseldi 3793 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 41118 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (𝜑𝐾𝑋)
27 ne0i 4119 . . . . . . . . 9 (𝐾𝑋𝑋 ≠ ∅)
2826, 27syl 17 . . . . . . . 8 (𝜑𝑋 ≠ ∅)
2928adantr 468 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
3012, 14, 29, 18, 22hoidmvn0val 41277 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
3130mpteq2dva 4934 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))))
3231fveq2d 6409 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))))
33 hspmbllem2.g . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
3432, 33eqbrtrd 4862 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
357, 25, 34ge0lere 40236 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
3837adantr 468 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
3936, 38, 14, 22hsphoif 41269 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
4012, 14, 18, 39hoidmvcl 41275 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,)+∞))
4111, 40sseldi 3793 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 41118 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ (0[,]+∞))
43 oveq2 6879 . . . . . . . . . . 11 (𝑥 = 𝑦 → (ℝ ↑𝑚 𝑥) = (ℝ ↑𝑚 𝑦))
44 eqeq1 2809 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45 prodeq1 14856 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
4644, 45ifbieq2d 4301 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
4743, 43, 46mpt2eq123dv 6944 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4847cbvmptv 4940 . . . . . . . . 9 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4912, 48eqtri 2827 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
50 diffi 8428 . . . . . . . . . . 11 (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52 snfi 8274 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (𝜑 → {𝐾} ∈ Fin)
54 unfi 8463 . . . . . . . . . 10 (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 575 . . . . . . . . 9 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5655adantr 468 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57 snidg 4397 . . . . . . . . . . . 12 (𝐾𝑋𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝐾})
59 elun2 3977 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61 neldifsnd 4511 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
6260, 61eldifd 3777 . . . . . . . . 9 (𝜑𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
6362adantr 468 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64 eqid 2805 . . . . . . . 8 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65 eqid 2805 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
66 uncom 3953 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
6826snssd 4527 . . . . . . . . . . . . 13 (𝜑 → {𝐾} ⊆ 𝑋)
69 undif 4242 . . . . . . . . . . . . 13 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7068, 69sylib 209 . . . . . . . . . . . 12 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7167, 70eqtrd 2839 . . . . . . . . . . 11 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7271adantr 468 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7372feq2d 6239 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶𝑗):𝑋⟶ℝ))
7418, 73mpbird 248 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7572feq2d 6239 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷𝑗):𝑋⟶ℝ))
7622, 75mpbird 248 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 41279 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)))
7871fveq2d 6409 . . . . . . . . . 10 (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
79 eqidd 2806 . . . . . . . . . 10 (𝜑 → (𝐶𝑗) = (𝐶𝑗))
8036a1i 11 . . . . . . . . . . . . 13 (𝜑𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8171oveq2d 6887 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑𝑚 𝑋))
8271mpteq1d 4928 . . . . . . . . . . . . . . . 16 (𝜑 → ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))
8381, 82mpteq12dv 4923 . . . . . . . . . . . . . . 15 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8483eqcomd 2811 . . . . . . . . . . . . . 14 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8584mpteq2dv 4935 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8680, 85eqtr2d 2840 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = 𝑇)
8786fveq1d 6407 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌) = (𝑇𝑌))
8887fveq1d 6407 . . . . . . . . . 10 (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗)) = ((𝑇𝑌)‘(𝐷𝑗)))
8978, 79, 88oveq123d 6892 . . . . . . . . 9 (𝜑 → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9089adantr 468 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9178adantr 468 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
9291oveqd 6888 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) = ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
9390, 92breq12d 4853 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) ↔ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))))
9477, 93mpbid 223 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
958, 10, 41, 24, 94sge0lempt 41103 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
9635, 42, 95ge0lere 40236 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
9897, 38, 14, 18hoidifhspf 41311 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
9912, 14, 98, 22hoidmvcl 41275 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
10099fmpttd 6604 . . . . . . 7 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
10111a1i 11 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102100, 101fssd 6267 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
10310, 102sge0cl 41074 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
10411, 99sseldi 3793 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
10526adantr 468 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐾𝑋)
10612, 14, 18, 22, 105, 97, 38hoidifhspdmvle 41313 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
1078, 10, 104, 24, 106sge0lempt 41103 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
10835, 103, 107ge0lere 40236 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
10937adantr 468 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
11013adantr 468 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111 eleq1w 2867 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112111anbi2d 616 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑙 ∈ ℕ)))
113 fveq2 6405 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
114113feq1d 6238 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝐷𝑗):𝑋⟶ℝ ↔ (𝐷𝑙):𝑋⟶ℝ))
115112, 114imbi12d 335 . . . . . . . . . 10 (𝑗 = 𝑙 → (((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ) ↔ ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)))
116115, 22chvarv 2439 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)
11736, 109, 110, 116hsphoif 41269 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ)
118 reex 10309 . . . . . . . . . . . 12 ℝ ∈ V
119118a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ V)
120119, 13jca 503 . . . . . . . . . 10 (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121120adantr 468 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122 elmapg 8102 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
123121, 122syl 17 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
124117, 123mpbird 248 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋))
125124fmpttd 6604 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
126 simpl 470 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
127 elinel1 3995 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
128127adantl 469 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
129 hspmbllem2.a . . . . . . . . . . . . . 14 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
130129sselda 3795 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
131 eliun 4712 . . . . . . . . . . . . 13 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
132130, 131sylib 209 . . . . . . . . . . . 12 ((𝜑𝑓𝐴) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
133126, 128, 132syl2anc 575 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
134 simpll 774 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135 elinel2 3996 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
136135adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
137136adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
138 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139 ixpfn 8148 . . . . . . . . . . . . . . . . 17 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140139adantl 469 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141 nfv 2008 . . . . . . . . . . . . . . . . . 18 𝑘((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142 nfcv 2947 . . . . . . . . . . . . . . . . . . 19 𝑘𝑓
143 nfixp1 8162 . . . . . . . . . . . . . . . . . . 19 𝑘X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
144142, 143nfel 2960 . . . . . . . . . . . . . . . . . 18 𝑘 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
145141, 144nfan 1993 . . . . . . . . . . . . . . . . 17 𝑘(((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
146183adant3 1155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐶𝑗):𝑋⟶ℝ)
147 simp3 1161 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑘𝑋)
148146, 147ffvelrnd 6579 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
149148rexrd 10371 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
150149ad5ant135 1477 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
151393adant3 1155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
152151, 147ffvelrnd 6579 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ)
153152rexrd 10371 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
154153ad5ant135 1477 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
155 iftrue 4282 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156 ioossre 12449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)𝑌) ⊆ ℝ
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158155, 157eqsstrd 3833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159 iffalse 4285 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160 ssid 3817 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162159, 161eqsstrd 3833 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163158, 162pm2.61i 176 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
165 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166165, 13, 26, 37hspval 41302 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167166adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168164, 167eleqtrd 2886 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169168adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170 simpr 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑘𝑋)
171 vex 3393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
172171elixp 8149 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173172biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174173simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175174adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → 𝑘𝑋)
177 rspa 3117 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178175, 176, 177syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179169, 170, 178syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180163, 179sseldi 3793 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
181180rexrd 10371 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
182181ad4ant14 750 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
183149ad4ant124 1208 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
184223adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐷𝑗):𝑋⟶ℝ)
185184, 147ffvelrnd 6579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ)
186185rexrd 10371 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
187186ad4ant124 1208 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
188171elixp 8149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
189188biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
190189simprd 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
191190adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
192 simpr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → 𝑘𝑋)
193 rspa 3117 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
194191, 192, 193syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
195194adantll 696 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
196 icogelb 12439 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
197183, 187, 195, 196syl3anc 1483 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
198197adantl3r 747 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
199 icoltub 40212 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
200183, 187, 195, 199syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
201200adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
202201ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
203 simpll 774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205203, 204jca 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
2062053ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝜑𝑗 ∈ ℕ))
207 simp2 1160 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208 simp3 1161 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) ≤ 𝑌)
209 fveq2 6405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝐾))
210209breq1d 4850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
211210biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) ≤ 𝑌)
212211iftrued 4284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝐾))
213209eqcomd 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
214213adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
215212, 214eqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
2162153adant1 1153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
217 breq2 4844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌 → ((𝑐) ≤ 𝑦 ↔ (𝑐) ≤ 𝑌))
218 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌𝑦 = 𝑌)
219217, 218ifbieq2d 4301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌 → if((𝑐) ≤ 𝑦, (𝑐), 𝑦) = if((𝑐) ≤ 𝑌, (𝑐), 𝑌))
220219ifeq2d 4295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑌 → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)) = if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))
221220mpteq2dv 4935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑌 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))))
222221mpteq2dv 4935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
223222adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑦 = 𝑌) → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
224 ovex 6903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑𝑚 𝑋) ∈ V
225224mptex 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V
226225a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V)
22780, 223, 37, 226fvmptd 6506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
228227adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
229 fveq1 6404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → (𝑐) = ((𝐷𝑗)‘))
230229breq1d 4850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (𝐷𝑗) → ((𝑐) ≤ 𝑌 ↔ ((𝐷𝑗)‘) ≤ 𝑌))
231230, 229ifbieq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → if((𝑐) ≤ 𝑌, (𝑐), 𝑌) = if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))
232229, 231ifeq12d 4296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (𝐷𝑗) → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)) = if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))
233232mpteq2dv 4935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (𝐷𝑗) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
234233adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷𝑗)) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
235 mptexg 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
23613, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
237236adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
238228, 234, 20, 237fvmptd 6506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
239238fveq1d 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
2402393adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
241 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝜑)
242 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝑘 = 𝐾)
243241, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝐾𝑋)
244242, 243eqeltrd 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝑘𝑋)
245 eqidd 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
246 eleq1w 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ( ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
247 fveq2 6405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ((𝐷𝑗)‘) = ((𝐷𝑗)‘𝑘))
248247breq1d 4850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = 𝑘 → (((𝐷𝑗)‘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝑘) ≤ 𝑌))
249248, 247ifbieq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌) = if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌))
250246, 247, 249ifbieq12d 4303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑘 → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
251250adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
252 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → 𝑘𝑋)
253 fvexd 6420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝐷𝑗)‘𝑘) ∈ V)
254 ifexg 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐷𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
255253, 37, 254syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
256 ifexg 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐷𝑗)‘𝑘) ∈ V ∧ if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
257253, 255, 256syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
258257adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
259245, 251, 252, 258fvmptd 6506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘𝑋) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
260241, 244, 259syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
261 eleq1 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
262210, 209ifbieq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
263261, 209, 262ifbieq12d 4303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
264263adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
265260, 264eqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
2662653adant2 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
267 neldifsnd 4511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
268267iffalsed 4287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
2692683ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
270240, 266, 2693eqtrrd 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2712703expa 1140 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2722713adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
273216, 272eqtr3d 2841 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
274206, 207, 208, 273syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
275274ad5ant145 1479 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
276202, 275breqtrd 4866 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
277 mnfxr 10378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
278277a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → -∞ ∈ ℝ*)
27937rexrd 10371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑌 ∈ ℝ*)
280279adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑌 ∈ ℝ*)
2812803ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
2821793adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
2831553ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
284282, 283eleqtrd 2886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
285 iooltub 40214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ*𝑌 ∈ ℝ* ∧ (𝑓𝑘) ∈ (-∞(,)𝑌)) → (𝑓𝑘) < 𝑌)
286278, 281, 284, 285syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
2872863adant1r 1216 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
288287ad4ant123 1206 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < 𝑌)
289 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌)
290210notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
291290adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
292289, 291mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌)
293292iffalsed 4287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = 𝑌)
294 eqidd 2806 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
295293, 294eqtr2d 2840 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
296295adantll 696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
297271adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
298297adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
299298adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
300296, 299eqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
301288, 300breqtrd 4866 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
302301adantl3r 747 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
303276, 302pm2.61dan 838 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
304201adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
3052383adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
306250adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3072583adant2 1154 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
308305, 306, 147, 307fvmptd 6506 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3093083expa 1140 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
310309adantllr 701 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
311310ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
312 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘𝑋)
313 neqne 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘 = 𝐾𝑘𝐾)
314 nelsn 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘𝐾 → ¬ 𝑘 ∈ {𝐾})
315313, 314syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
316315adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
317312, 316eldifd 3777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
318317iftrued 4284 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
319318adantll 696 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
320311, 319eqtr2d 2840 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
321304, 320breqtrd 4866 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
322303, 321pm2.61dan 838 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
323150, 154, 182, 198, 322elicod 12438 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
324323ex 399 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
325145, 324ralrimi 3144 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
326140, 325jca 503 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
327171elixp 8149 . . . . . . . . . . . . . . 15 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
328326, 327sylibr 225 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
329328ex 399 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
330134, 137, 138, 329syl21anc 857 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
331330reximdva 3203 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
332133, 331mpd 15 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
333 eliun 4712 . . . . . . . . . 10 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
334332, 333sylibr 225 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
335334ralrimiva 3153 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
336 dfss3 3784 . . . . . . . 8 ((𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
337335, 336sylibr 225 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
338 eqidd 2806 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))))
339 2fveq3 6410 . . . . . . . . . . . . 13 (𝑙 = 𝑗 → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
340339adantl 469 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
341 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
342 fvexd 6420 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝑇𝑌)‘(𝐷𝑗)) ∈ V)
343338, 340, 341, 342fvmptd 6506 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗) = ((𝑇𝑌)‘(𝐷𝑗)))
344343fveq1d 6407 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
345344oveq2d 6887 . . . . . . . . 9 (𝑗 ∈ ℕ → (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
346345ixpeq2dv 8158 . . . . . . . 8 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
347346iuneq2i 4727 . . . . . . 7 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
348337, 347syl6sseqr 3846 . . . . . 6 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)))
34913, 15, 125, 348, 12ovnlecvr2 41303 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))))
350343oveq2d 6887 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
351350mpteq2ia 4930 . . . . . . 7 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
352351fveq2i 6408 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗)))))
353352a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
354349, 353breqtrd 4866 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
35515ffvelrnda 6578 . . . . . . . . . 10 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋))
356 elmapi 8111 . . . . . . . . . 10 ((𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑙):𝑋⟶ℝ)
357355, 356syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙):𝑋⟶ℝ)
35897, 109, 110, 357hoidifhspf 41311 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ)
359 elmapg 8102 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
360120, 359syl 17 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
361360adantr 468 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
362358, 361mpbird 248 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋))
363362fmpttd 6604 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
364 simpl 470 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
365 eldifi 3928 . . . . . . . . . . . 12 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
366365adantl 469 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
367364, 366, 132syl2anc 575 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
368139adantl 469 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
369 nfv 2008 . . . . . . . . . . . . . . . . 17 𝑘((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
370369, 144nfan 1993 . . . . . . . . . . . . . . . 16 𝑘(((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
371983adant3 1155 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
372371, 147ffvelrnd 6579 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ)
373372rexrd 10371 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
374373ad5ant135 1477 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
375187adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
3761483expa 1140 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
3771863expa 1140 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
378 icossre 12468 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ*) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
379376, 377, 378syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
380379adantlr 697 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
381380, 195sseldd 3796 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
382381rexrd 10371 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
383382adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
384383adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑌 ∈ ℝ)
385143adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
38697, 384, 385, 146, 147hoidifhspval3 41312 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
387386ad5ant134 1475 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
388 iftrue 4282 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
389388adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
390387, 389eqtrd 2839 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
391390adantllr 701 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
392 iftrue 4282 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
393392adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
394197adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
395394ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
396393, 395eqbrtrd 4862 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
397 iffalse 4285 . . . . . . . . . . . . . . . . . . . . . . 23 𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
398397adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
399 simpl1 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))))
400 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝑘))
401 fveq2 6405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝐾 → (𝑓𝑘) = (𝑓𝐾))
402401breq2d 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑌 ≤ (𝑓𝑘) ↔ 𝑌 ≤ (𝑓𝐾)))
403402notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
404403adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
405400, 404mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
4064053ad2antl3 1231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
407401eqcomd 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑓𝐾) = (𝑓𝑘))
4084073ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) = (𝑓𝑘))
409367adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
410 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
411410ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝜑𝑗 ∈ ℕ))
412 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
413252ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑘𝑋)
414411, 412, 413, 381syl21anc 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) ∈ ℝ)
415414ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
416415rexlimdva 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
417416adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
418409, 417mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
4194183adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
420408, 419eqeltrd 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) ∈ ℝ)
421420adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) ∈ ℝ)
422399, 364, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑌 ∈ ℝ)
423421, 422ltnled 10466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ((𝑓𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
424406, 423mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) < 𝑌)
425368, 367r19.29a 3265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 Fn 𝑋)
426425adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → 𝑓 Fn 𝑋)
427277a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ*)
428279ad4antr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
429418ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
430429mnfltd 12170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓𝑘))
431401adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) = (𝑓𝐾))
432 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝐾) < 𝑌)
433431, 432eqbrtrd 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
434433ad4ant24 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
435427, 428, 429, 430, 434eliood 40201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
436155eqcomd 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437436adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
438435, 437eleqtrd 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439418ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
440159eqcomd 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441440adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
442439, 441eleqtrd 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
443438, 442pm2.61dan 838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
444443ralrimiva 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
445426, 444jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
446399, 424, 445syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
447446, 172sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
448166eqcomd 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
449448ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
4504493ad2antl1 1229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
451447, 450eleqtrd 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
452 eldifn 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
453452adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
4544533ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
455454adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
456451, 455condan 843 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
457456ad5ant145 1479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
458457adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → 𝑌 ≤ (𝑓𝑘))
459398, 458eqbrtrd 4862 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
460396, 459pm2.61dan 838 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
461391, 460eqbrtrd 4862 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
462386ad5ant124 1471 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
463 iffalse 4285 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
464463adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
465462, 464eqtrd 2839 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = ((𝐶𝑗)‘𝑘))
466197adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
467465, 466eqbrtrd 4862 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
468467adantl4r 756 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
469461, 468pm2.61dan 838 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
470200adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
471374, 375, 383, 469, 470elicod 12438 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
472471ex 399 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
473370, 472ralrimi 3144 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
474368, 473jca 503 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
475171elixp 8149 . . . . . . . . . . . . . 14 (𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
476474, 475sylibr 225 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
477 eqidd 2806 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))))
478 2fveq3 6410 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
479478adantl 469 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
480 fvexd 6420 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((𝑆𝑌)‘(𝐶𝑗)) ∈ V)
481477, 479, 341, 480fvmptd 6506 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗) = ((𝑆𝑌)‘(𝐶𝑗)))
482481fveq1d 6407 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘) = (((𝑆𝑌)‘(𝐶𝑗))‘𝑘))
483482oveq1d 6886 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
484483ixpeq2dv 8158 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
485484ad2antlr 709 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
486485eleq2d 2870 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
487476, 486mpbird 248 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
488487ex 399 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
489488reximdva 3203 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
490367, 489mpd 15 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
491 eliun 4712 . . . . . . . . 9 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
492490, 491sylibr 225 . . . . . . . 8 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
493492ralrimiva 3153 . . . . . . 7 (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
494 dfss3 3784 . . . . . . 7 ((𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
495493, 494sylibr 225 . . . . . 6 (𝜑 → (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
49613, 363, 19, 495, 12ovnlecvr2 41303 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))))
497481oveq1d 6886 . . . . . . . 8 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
498497mpteq2ia 4930 . . . . . . 7 (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
499498fveq2i 6408 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
500499a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
501496, 500breqtrd 4866 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
5021, 2, 96, 108, 354, 501leadd12dd 40009 . . 3 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50314, 105, 38, 18, 22, 12, 36, 97hspmbllem1 41319 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
504503mpteq2dva 4934 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
505504fveq2d 6409 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
5068, 10, 41, 104sge0xadd 41128 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50796, 108rexaddd 12279 . . . 4 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
508505, 506, 5073eqtrrd 2844 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
509502, 508breqtrd 4866 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
5103, 35, 7, 509, 34letrd 10476 1 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2158  wne 2977  wral 3095  wrex 3096  Vcvv 3390  cdif 3763  cun 3764  cin 3765  wss 3766  c0 4113  ifcif 4276  {csn 4367   ciun 4708   class class class wbr 4840  cmpt 4919   Fn wfn 6093  wf 6094  cfv 6098  (class class class)co 6871  cmpt2 6873  𝑚 cmap 8089  Xcixp 8142  Fincfn 8189  cr 10217  0cc0 10218   + caddc 10221  +∞cpnf 10353  -∞cmnf 10354  *cxr 10355   < clt 10356  cle 10357  cn 11302  +crp 12042   +𝑒 cxad 12156  (,)cioo 12389  [,)cico 12391  [,]cicc 12392  cprod 14852  volcvol 23440  Σ^csumge0 41055  voln*covoln 41229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295  ax-pre-sup 10296
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-er 7976  df-map 8091  df-pm 8092  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fi 8553  df-sup 8584  df-inf 8585  df-oi 8651  df-card 9045  df-cda 9272  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-n0 11556  df-z 11640  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-rlim 14439  df-sum 14636  df-prod 14853  df-rest 16284  df-topgen 16305  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-top 20908  df-topon 20925  df-bases 20960  df-cmp 21400  df-ovol 23441  df-vol 23442  df-sumge0 41056  df-ovoln 41230
This theorem is referenced by:  hspmbllem3  41321
  Copyright terms: Public domain W3C validator