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 44165
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 11004 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (𝜑𝐸 ∈ ℝ+)
65rpred 12772 . . . 4 (𝜑𝐸 ∈ ℝ)
74, 6readdcld 11004 . . 3 (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8 nfv 1917 . . . 4 𝑗𝜑
9 nnex 11979 . . . . 5 ℕ ∈ V
109a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
11 icossicc 13168 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
12 hspmbllem2.l . . . . . 6 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
13 hspmbllem2.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
1413adantr 481 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15 hspmbllem2.c . . . . . . . 8 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑋))
1615ffvelrnda 6961 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑m 𝑋))
17 elmapi 8637 . . . . . . 7 ((𝐶𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
1816, 17syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
19 hspmbllem2.d . . . . . . . 8 (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑋))
2019ffvelrnda 6961 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑m 𝑋))
21 elmapi 8637 . . . . . . 7 ((𝐷𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
2220, 21syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
2312, 14, 18, 22hoidmvcl 44120 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
2411, 23sselid 3919 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 43963 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (𝜑𝐾𝑋)
27 ne0i 4268 . . . . . . . . 9 (𝐾𝑋𝑋 ≠ ∅)
2826, 27syl 17 . . . . . . . 8 (𝜑𝑋 ≠ ∅)
2928adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
3012, 14, 29, 18, 22hoidmvn0val 44122 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
3130mpteq2dva 5174 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))))
3231fveq2d 6778 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))))
33 hspmbllem2.g . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
3432, 33eqbrtrd 5096 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
357, 25, 34ge0lere 43070 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
3837adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
3936, 38, 14, 22hsphoif 44114 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
4012, 14, 18, 39hoidmvcl 44120 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,)+∞))
4111, 40sselid 3919 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 43963 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ (0[,]+∞))
43 oveq2 7283 . . . . . . . . . . 11 (𝑥 = 𝑦 → (ℝ ↑m 𝑥) = (ℝ ↑m 𝑦))
44 eqeq1 2742 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45 prodeq1 15619 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
4644, 45ifbieq2d 4485 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
4743, 43, 46mpoeq123dv 7350 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4847cbvmptv 5187 . . . . . . . . 9 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4912, 48eqtri 2766 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
50 diffi 8962 . . . . . . . . . . 11 (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52 snfi 8834 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (𝜑 → {𝐾} ∈ Fin)
54 unfi 8955 . . . . . . . . . 10 (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5655adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57 snidg 4595 . . . . . . . . . . . 12 (𝐾𝑋𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝐾})
59 elun2 4111 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61 neldifsnd 4726 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
6260, 61eldifd 3898 . . . . . . . . 9 (𝜑𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
6362adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64 eqid 2738 . . . . . . . 8 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65 eqid 2738 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
66 uncom 4087 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
6826snssd 4742 . . . . . . . . . . . . 13 (𝜑 → {𝐾} ⊆ 𝑋)
69 undif 4415 . . . . . . . . . . . . 13 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7068, 69sylib 217 . . . . . . . . . . . 12 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7167, 70eqtrd 2778 . . . . . . . . . . 11 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7271adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7372feq2d 6586 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶𝑗):𝑋⟶ℝ))
7418, 73mpbird 256 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7572feq2d 6586 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷𝑗):𝑋⟶ℝ))
7622, 75mpbird 256 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 44124 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)))
7871fveq2d 6778 . . . . . . . . . 10 (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
79 eqidd 2739 . . . . . . . . . 10 (𝜑 → (𝐶𝑗) = (𝐶𝑗))
8036a1i 11 . . . . . . . . . . . . 13 (𝜑𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8171oveq2d 7291 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑m 𝑋))
8271mpteq1d 5169 . . . . . . . . . . . . . . . 16 (𝜑 → ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))
8381, 82mpteq12dv 5165 . . . . . . . . . . . . . . 15 (𝜑 → (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8483eqcomd 2744 . . . . . . . . . . . . . 14 (𝜑 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8584mpteq2dv 5176 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8680, 85eqtr2d 2779 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = 𝑇)
8786fveq1d 6776 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌) = (𝑇𝑌))
8887fveq1d 6776 . . . . . . . . . 10 (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗)) = ((𝑇𝑌)‘(𝐷𝑗)))
8978, 79, 88oveq123d 7296 . . . . . . . . 9 (𝜑 → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9089adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9178adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
9291oveqd 7292 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) = ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
9390, 92breq12d 5087 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) ↔ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))))
9477, 93mpbid 231 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
958, 10, 41, 24, 94sge0lempt 43948 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
9635, 42, 95ge0lere 43070 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
9897, 38, 14, 18hoidifhspf 44156 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
9912, 14, 98, 22hoidmvcl 44120 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
10099fmpttd 6989 . . . . . . 7 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
10111a1i 11 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102100, 101fssd 6618 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
10310, 102sge0cl 43919 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
10411, 99sselid 3919 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
10526adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐾𝑋)
10612, 14, 18, 22, 105, 97, 38hoidifhspdmvle 44158 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
1078, 10, 104, 24, 106sge0lempt 43948 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
10835, 103, 107ge0lere 43070 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
10937adantr 481 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
11013adantr 481 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111 eleq1w 2821 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112111anbi2d 629 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑙 ∈ ℕ)))
113 fveq2 6774 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
114113feq1d 6585 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝐷𝑗):𝑋⟶ℝ ↔ (𝐷𝑙):𝑋⟶ℝ))
115112, 114imbi12d 345 . . . . . . . . . 10 (𝑗 = 𝑙 → (((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ) ↔ ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)))
116115, 22chvarvv 2002 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)
11736, 109, 110, 116hsphoif 44114 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ)
118 reex 10962 . . . . . . . . . . . 12 ℝ ∈ V
119118a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ V)
120119, 13jca 512 . . . . . . . . . 10 (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121120adantr 481 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122 elmapg 8628 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
123121, 122syl 17 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
124117, 123mpbird 256 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑m 𝑋))
125124fmpttd 6989 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))):ℕ⟶(ℝ ↑m 𝑋))
126 simpl 483 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
127 elinel1 4129 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
128127adantl 482 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
129 hspmbllem2.a . . . . . . . . . . . . . 14 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
130129sselda 3921 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
131 eliun 4928 . . . . . . . . . . . . 13 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
132130, 131sylib 217 . . . . . . . . . . . 12 ((𝜑𝑓𝐴) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
133126, 128, 132syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
134 simpll 764 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135 elinel2 4130 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
136135adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
137136adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
138 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139 ixpfn 8691 . . . . . . . . . . . . . . . . 17 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140139adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑘((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑘𝑓
143 nfixp1 8706 . . . . . . . . . . . . . . . . . . 19 𝑘X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
144142, 143nfel 2921 . . . . . . . . . . . . . . . . . 18 𝑘 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
145141, 144nfan 1902 . . . . . . . . . . . . . . . . 17 𝑘(((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
146183adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐶𝑗):𝑋⟶ℝ)
147 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑘𝑋)
148146, 147ffvelrnd 6962 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
149148rexrd 11025 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
150149ad5ant135 1367 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
151393adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
152151, 147ffvelrnd 6962 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ)
153152rexrd 11025 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
154153ad5ant135 1367 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
155 iftrue 4465 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156 ioossre 13140 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)𝑌) ⊆ ℝ
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158155, 157eqsstrd 3959 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159 iffalse 4468 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160 ssid 3943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162159, 161eqsstrd 3959 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163158, 162pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
165 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166165, 13, 26, 37hspval 44147 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167166adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168164, 167eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169168adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑘𝑋)
171 vex 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
172171elixp 8692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173172biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174173simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175174adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → 𝑘𝑋)
177 rspa 3132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178175, 176, 177syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179169, 170, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180163, 179sselid 3919 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
181180rexrd 11025 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
182181ad4ant14 749 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
183149ad4ant124 1172 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
184223adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐷𝑗):𝑋⟶ℝ)
185184, 147ffvelrnd 6962 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ)
186185rexrd 11025 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
187186ad4ant124 1172 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
188171elixp 8692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
189188biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
190189simprd 496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
191190adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
192 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → 𝑘𝑋)
193 rspa 3132 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
194191, 192, 193syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
195194adantll 711 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
196 icogelb 13130 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
197183, 187, 195, 196syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
198197adantl3r 747 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
199 icoltub 43046 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
200183, 187, 195, 199syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
201200adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
202201ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
203 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205203, 204jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
2062053ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝜑𝑗 ∈ ℕ))
207 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) ≤ 𝑌)
209 fveq2 6774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝐾))
210209breq1d 5084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
211210biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) ≤ 𝑌)
212211iftrued 4467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝐾))
213209eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
214213adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
215212, 214eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
2162153adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
217 breq2 5078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌 → ((𝑐) ≤ 𝑦 ↔ (𝑐) ≤ 𝑌))
218 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌𝑦 = 𝑌)
219217, 218ifbieq2d 4485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑌 → if((𝑐) ≤ 𝑦, (𝑐), 𝑦) = if((𝑐) ≤ 𝑌, (𝑐), 𝑌))
220219ifeq2d 4479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑌 → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)) = if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))
221220mpteq2dv 5176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑌 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))))
222221mpteq2dv 5176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
223 ovex 7308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑m 𝑋) ∈ V
224223mptex 7099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V
225224a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V)
22636, 222, 37, 225fvmptd3 6898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
227226adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
228 fveq1 6773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → (𝑐) = ((𝐷𝑗)‘))
229228breq1d 5084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (𝐷𝑗) → ((𝑐) ≤ 𝑌 ↔ ((𝐷𝑗)‘) ≤ 𝑌))
230229, 228ifbieq1d 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → if((𝑐) ≤ 𝑌, (𝑐), 𝑌) = if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))
231228, 230ifeq12d 4480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (𝐷𝑗) → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)) = if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))
232231mpteq2dv 5176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (𝐷𝑗) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
233232adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷𝑗)) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
234 mptexg 7097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
23513, 234syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
237227, 233, 20, 236fvmptd 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
238237fveq1d 6776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
2392383adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
240 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝜑)
241 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝑘 = 𝐾)
242240, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝐾𝑋)
243241, 242eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝑘𝑋)
244 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
245 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ( ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246 fveq2 6774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ((𝐷𝑗)‘) = ((𝐷𝑗)‘𝑘))
247246breq1d 5084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = 𝑘 → (((𝐷𝑗)‘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝑘) ≤ 𝑌))
248247, 246ifbieq1d 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌) = if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌))
249245, 246, 248ifbieq12d 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑘 → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
250249adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
251 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → 𝑘𝑋)
252 fvexd 6789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝐷𝑗)‘𝑘) ∈ V)
253252, 37ifexd 4507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
254252, 253ifexd 4507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
255254adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
256244, 250, 251, 255fvmptd 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘𝑋) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
257240, 243, 256syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
258 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
259210, 209ifbieq1d 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
260258, 209, 259ifbieq12d 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
261260adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
262257, 261eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
2632623adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
264 neldifsnd 4726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
265264iffalsed 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
2662653ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
267239, 263, 2663eqtrrd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2682673expa 1117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2692683adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
270216, 269eqtr3d 2780 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
271206, 207, 208, 270syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
272271ad5ant145 1368 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
273202, 272breqtrd 5100 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
274 mnfxr 11032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
275274a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → -∞ ∈ ℝ*)
27637rexrd 11025 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑌 ∈ ℝ*)
277276adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑌 ∈ ℝ*)
2782773ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
2791793adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
2801553ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
281279, 280eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
282 iooltub 43048 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ*𝑌 ∈ ℝ* ∧ (𝑓𝑘) ∈ (-∞(,)𝑌)) → (𝑓𝑘) < 𝑌)
283275, 278, 281, 282syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
2842833adant1r 1176 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
285284ad4ant123 1171 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < 𝑌)
286 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌)
287210notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
288287adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
289286, 288mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌)
290289iffalsed 4470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = 𝑌)
291 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
292290, 291eqtr2d 2779 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
293292adantll 711 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
294268adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
295294adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
296295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
297293, 296eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
298285, 297breqtrd 5100 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
299298adantl3r 747 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
300273, 299pm2.61dan 810 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
301201adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
3022373adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
303249adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3042553adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
305302, 303, 147, 304fvmptd 6882 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3063053expa 1117 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
307306adantllr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
308307ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
309 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘𝑋)
310 neqne 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘 = 𝐾𝑘𝐾)
311 nelsn 4601 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘𝐾 → ¬ 𝑘 ∈ {𝐾})
312310, 311syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
313312adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
314309, 313eldifd 3898 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
315314iftrued 4467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
316315adantll 711 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
317308, 316eqtr2d 2779 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
318301, 317breqtrd 5100 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
319300, 318pm2.61dan 810 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
320150, 154, 182, 198, 319elicod 13129 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
321320ex 413 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
322145, 321ralrimi 3141 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
323140, 322jca 512 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
324171elixp 8692 . . . . . . . . . . . . . . 15 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
325323, 324sylibr 233 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
326325ex 413 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
327134, 137, 138, 326syl21anc 835 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
328327reximdva 3203 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
329133, 328mpd 15 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
330 eliun 4928 . . . . . . . . . 10 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
331329, 330sylibr 233 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
332331ralrimiva 3103 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
333 dfss3 3909 . . . . . . . 8 ((𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
334332, 333sylibr 233 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
335 eqidd 2739 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))))
336 2fveq3 6779 . . . . . . . . . . . . 13 (𝑙 = 𝑗 → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
337336adantl 482 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
338 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
339 fvexd 6789 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝑇𝑌)‘(𝐷𝑗)) ∈ V)
340335, 337, 338, 339fvmptd 6882 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗) = ((𝑇𝑌)‘(𝐷𝑗)))
341340fveq1d 6776 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
342341oveq2d 7291 . . . . . . . . 9 (𝑗 ∈ ℕ → (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
343342ixpeq2dv 8701 . . . . . . . 8 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
344343iuneq2i 4945 . . . . . . 7 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
345334, 344sseqtrrdi 3972 . . . . . 6 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)))
34613, 15, 125, 345, 12ovnlecvr2 44148 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))))
347340oveq2d 7291 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
348347mpteq2ia 5177 . . . . . . 7 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
349348fveq2i 6777 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗)))))
350349a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
351346, 350breqtrd 5100 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
35215ffvelrnda 6961 . . . . . . . . . 10 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙) ∈ (ℝ ↑m 𝑋))
353 elmapi 8637 . . . . . . . . . 10 ((𝐶𝑙) ∈ (ℝ ↑m 𝑋) → (𝐶𝑙):𝑋⟶ℝ)
354352, 353syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙):𝑋⟶ℝ)
35597, 109, 110, 354hoidifhspf 44156 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ)
356 elmapg 8628 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
357120, 356syl 17 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
358357adantr 481 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
359355, 358mpbird 256 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑m 𝑋))
360359fmpttd 6989 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))):ℕ⟶(ℝ ↑m 𝑋))
361 simpl 483 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
362 eldifi 4061 . . . . . . . . . . . 12 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
363362adantl 482 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
364361, 363, 132syl2anc 584 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
365139adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
366 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑘((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
367366, 144nfan 1902 . . . . . . . . . . . . . . . 16 𝑘(((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
368983adant3 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
369368, 147ffvelrnd 6962 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ)
370369rexrd 11025 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
371370ad5ant135 1367 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
372187adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
3731483expa 1117 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
3741863expa 1117 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
375 icossre 13160 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ*) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
376373, 374, 375syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
377376adantlr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
378377, 195sseldd 3922 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
379378rexrd 11025 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
380379adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
381383adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑌 ∈ ℝ)
382143adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
38397, 381, 382, 146, 147hoidifhspval3 44157 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
384383ad5ant134 1366 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
385 iftrue 4465 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
386385adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
387384, 386eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
388387adantllr 716 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
389 iftrue 4465 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
390389adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
391197adantl3r 747 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
392391ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
393390, 392eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
394 iffalse 4468 . . . . . . . . . . . . . . . . . . . . . . 23 𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
395394adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
396 simpl1 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))))
397 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝑘))
398 fveq2 6774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝐾 → (𝑓𝑘) = (𝑓𝐾))
399398breq2d 5086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑌 ≤ (𝑓𝑘) ↔ 𝑌 ≤ (𝑓𝐾)))
400399notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
401400adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
402397, 401mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
4034023ad2antl3 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
404398eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑓𝐾) = (𝑓𝑘))
4054043ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) = (𝑓𝑘))
406364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
407 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
408407ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝜑𝑗 ∈ ℕ))
409 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
410251ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑘𝑋)
411408, 409, 410, 378syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) ∈ ℝ)
412411rexlimdva2 3216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
413412adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
414406, 413mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
4154143adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
416405, 415eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) ∈ ℝ)
417416adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) ∈ ℝ)
418396, 361, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑌 ∈ ℝ)
419417, 418ltnled 11122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ((𝑓𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
420403, 419mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) < 𝑌)
421365, 364r19.29a 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 Fn 𝑋)
422421adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → 𝑓 Fn 𝑋)
423274a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ*)
424276ad4antr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
425414ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
426425mnfltd 12860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓𝑘))
427398adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) = (𝑓𝐾))
428 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝐾) < 𝑌)
429427, 428eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
430429ad4ant24 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
431423, 424, 425, 426, 430eliood 43036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
432155eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
433432adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
434431, 433eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435414ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
436159eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437436adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
438435, 437eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439434, 438pm2.61dan 810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440439ralrimiva 3103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441422, 440jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
442396, 420, 441syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
443442, 172sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
444166eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
445444ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
4464453ad2antl1 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
447443, 446eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
448 eldifn 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
449448adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
4504493ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
451450adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
452447, 451condan 815 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
453452ad5ant145 1368 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
454453adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → 𝑌 ≤ (𝑓𝑘))
455395, 454eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
456393, 455pm2.61dan 810 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
457388, 456eqbrtrd 5096 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
458383ad5ant124 1364 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
459 iffalse 4468 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
460459adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
461458, 460eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = ((𝐶𝑗)‘𝑘))
462197adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
463461, 462eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
464463adantl4r 752 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
465457, 464pm2.61dan 810 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
466200adantl3r 747 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
467371, 372, 380, 465, 466elicod 13129 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
468467ex 413 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
469367, 468ralrimi 3141 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
470365, 469jca 512 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
471171elixp 8692 . . . . . . . . . . . . . 14 (𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
472470, 471sylibr 233 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
473 eqidd 2739 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))))
474 2fveq3 6779 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
475474adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
476 fvexd 6789 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((𝑆𝑌)‘(𝐶𝑗)) ∈ V)
477473, 475, 338, 476fvmptd 6882 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗) = ((𝑆𝑌)‘(𝐶𝑗)))
478477fveq1d 6776 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘) = (((𝑆𝑌)‘(𝐶𝑗))‘𝑘))
479478oveq1d 7290 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
480479ixpeq2dv 8701 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
481480ad2antlr 724 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
482481eleq2d 2824 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
483472, 482mpbird 256 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
484483ex 413 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
485484reximdva 3203 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
486364, 485mpd 15 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
487 eliun 4928 . . . . . . . . 9 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
488486, 487sylibr 233 . . . . . . . 8 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
489488ralrimiva 3103 . . . . . . 7 (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
490 dfss3 3909 . . . . . . 7 ((𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
491489, 490sylibr 233 . . . . . 6 (𝜑 → (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
49213, 360, 19, 491, 12ovnlecvr2 44148 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))))
493477oveq1d 7290 . . . . . . . 8 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
494493mpteq2ia 5177 . . . . . . 7 (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
495494fveq2i 6777 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
496495a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
497492, 496breqtrd 5100 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
4981, 2, 96, 108, 351, 497leadd12dd 42855 . . 3 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
49914, 105, 38, 18, 22, 12, 36, 97hspmbllem1 44164 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
500499mpteq2dva 5174 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
501500fveq2d 6778 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
5028, 10, 41, 104sge0xadd 43973 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
50396, 108rexaddd 12968 . . . 4 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
504501, 502, 5033eqtrrd 2783 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
505498, 504breqtrd 5100 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
5063, 35, 7, 505, 34letrd 11132 1 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  Vcvv 3432  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256  ifcif 4459  {csn 4561   ciun 4924   class class class wbr 5074  cmpt 5157   Fn wfn 6428  wf 6429  cfv 6433  (class class class)co 7275  cmpo 7277  m cmap 8615  Xcixp 8685  Fincfn 8733  cr 10870  0cc0 10871   + caddc 10874  +∞cpnf 11006  -∞cmnf 11007  *cxr 11008   < clt 11009  cle 11010  cn 11973  +crp 12730   +𝑒 cxad 12846  (,)cioo 13079  [,)cico 13081  [,]cicc 13082  cprod 15615  volcvol 24627  Σ^csumge0 43900  voln*covoln 44074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-rlim 15198  df-sum 15398  df-prod 15616  df-rest 17133  df-topgen 17154  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-top 22043  df-topon 22060  df-bases 22096  df-cmp 22538  df-ovol 24628  df-vol 24629  df-sumge0 43901  df-ovoln 44075
This theorem is referenced by:  hspmbllem3  44166
  Copyright terms: Public domain W3C validator