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

Theorem hspmbllem2 39517
 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 9948 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (𝜑𝐸 ∈ ℝ+)
65rpred 11748 . . . 4 (𝜑𝐸 ∈ ℝ)
74, 6readdcld 9948 . . 3 (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8 nfv 1830 . . . 4 𝑗𝜑
9 nnex 10903 . . . . 5 ℕ ∈ V
109a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
11 icossicc 12131 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
12 hspmbllem2.l . . . . . 6 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
13 hspmbllem2.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
1413adantr 480 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15 hspmbllem2.c . . . . . . . 8 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
1615ffvelrnda 6267 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
17 elmapi 7765 . . . . . . 7 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
1816, 17syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
19 hspmbllem2.d . . . . . . . 8 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
2019ffvelrnda 6267 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
21 elmapi 7765 . . . . . . 7 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
2220, 21syl 17 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
2312, 14, 18, 22hoidmvcl 39472 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
2411, 23sseldi 3566 . . . 4 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 39318 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (𝜑𝐾𝑋)
27 ne0i 3880 . . . . . . . . 9 (𝐾𝑋𝑋 ≠ ∅)
2826, 27syl 17 . . . . . . . 8 (𝜑𝑋 ≠ ∅)
2928adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
3012, 14, 29, 18, 22hoidmvn0val 39474 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
3130mpteq2dva 4672 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))))
3231fveq2d 6107 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))))
33 hspmbllem2.g . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
3432, 33eqbrtrd 4605 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
357, 25, 34ge0lere 38606 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
3837adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
3936, 38, 14, 22hsphoif 39466 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
4012, 14, 18, 39hoidmvcl 39472 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,)+∞))
4111, 40sseldi 3566 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 39318 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ (0[,]+∞))
43 oveq2 6557 . . . . . . . . . . 11 (𝑥 = 𝑦 → (ℝ ↑𝑚 𝑥) = (ℝ ↑𝑚 𝑦))
44 eqeq1 2614 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45 prodeq1 14478 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
4644, 45ifbieq2d 4061 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
4743, 43, 46mpt2eq123dv 6615 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4847cbvmptv 4678 . . . . . . . . 9 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
4912, 48eqtri 2632 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑦), 𝑏 ∈ (ℝ ↑𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘𝑦 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
50 diffi 8077 . . . . . . . . . . 11 (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52 snfi 7923 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (𝜑 → {𝐾} ∈ Fin)
54 unfi 8112 . . . . . . . . . 10 (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 691 . . . . . . . . 9 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
5655adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57 snidg 4153 . . . . . . . . . . . 12 (𝐾𝑋𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝐾})
59 elun2 3743 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61 neldifsnd 4263 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
6260, 61eldifd 3551 . . . . . . . . 9 (𝜑𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
6362adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64 eqid 2610 . . . . . . . 8 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65 eqid 2610 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
66 uncom 3719 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
6826snssd 4281 . . . . . . . . . . . . 13 (𝜑 → {𝐾} ⊆ 𝑋)
69 undif 4001 . . . . . . . . . . . . 13 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7068, 69sylib 207 . . . . . . . . . . . 12 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
7167, 70eqtrd 2644 . . . . . . . . . . 11 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7271adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
7372feq2d 5944 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶𝑗):𝑋⟶ℝ))
7418, 73mpbird 246 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7572feq2d 5944 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷𝑗):𝑋⟶ℝ))
7622, 75mpbird 246 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 39476 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)))
7871fveq2d 6107 . . . . . . . . . 10 (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
79 eqidd 2611 . . . . . . . . . 10 (𝜑 → (𝐶𝑗) = (𝐶𝑗))
8036a1i 11 . . . . . . . . . . . . 13 (𝜑𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8171oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑𝑚 𝑋))
8271mpteq1d 4666 . . . . . . . . . . . . . . . 16 (𝜑 → ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))
8381, 82mpteq12dv 4663 . . . . . . . . . . . . . . 15 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8483eqcomd 2616 . . . . . . . . . . . . . 14 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))
8584mpteq2dv 4673 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))))
8680, 85eqtr2d 2645 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))))) = 𝑇)
8786fveq1d 6105 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌) = (𝑇𝑌))
8887fveq1d 6105 . . . . . . . . . 10 (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗)) = ((𝑇𝑌)‘(𝐷𝑗)))
8978, 79, 88oveq123d 6570 . . . . . . . . 9 (𝜑 → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9089adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
9178adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿𝑋))
9291oveqd 6566 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) = ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
9390, 92breq12d 4596 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ ( ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))))‘𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷𝑗)) ↔ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))))
9477, 93mpbid 221 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
958, 10, 41, 24, 94sge0lempt 39303 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
9635, 42, 95ge0lere 38606 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
9897, 38, 14, 18hoidifhspf 39508 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
9912, 14, 98, 22hoidmvcl 39472 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
100 eqid 2610 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
10199, 100fmptd 6292 . . . . . . 7 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
10211a1i 11 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
103101, 102fssd 5970 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
10410, 103sge0cl 39274 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ (0[,]+∞))
10511, 99sseldi 3566 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ∈ (0[,]+∞))
10626adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐾𝑋)
10712, 14, 18, 22, 106, 97, 38hoidifhspdmvle 39510 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)) ≤ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
1088, 10, 105, 24, 107sge0lempt 39303 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
10935, 104, 108ge0lere 38606 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))) ∈ ℝ)
11037adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
11113adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
112 eleq1 2676 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
113112anbi2d 736 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑙 ∈ ℕ)))
114 fveq2 6103 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
115114feq1d 5943 . . . . . . . . . . 11 (𝑗 = 𝑙 → ((𝐷𝑗):𝑋⟶ℝ ↔ (𝐷𝑙):𝑋⟶ℝ))
116113, 115imbi12d 333 . . . . . . . . . 10 (𝑗 = 𝑙 → (((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ) ↔ ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)))
117116, 22chvarv 2251 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐷𝑙):𝑋⟶ℝ)
11836, 110, 111, 117hsphoif 39466 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ)
119 reex 9906 . . . . . . . . . . . 12 ℝ ∈ V
120119a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ V)
121120, 13jca 553 . . . . . . . . . 10 (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122121adantr 480 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
123 elmapg 7757 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
124122, 123syl 17 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑇𝑌)‘(𝐷𝑙)):𝑋⟶ℝ))
125118, 124mpbird 246 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑙)) ∈ (ℝ ↑𝑚 𝑋))
126 eqid 2610 . . . . . . 7 (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))
127125, 126fmptd 6292 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
128 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
129 elinel1 3761 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
130129adantl 481 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
131 hspmbllem2.a . . . . . . . . . . . . . 14 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
132131sselda 3568 . . . . . . . . . . . . 13 ((𝜑𝑓𝐴) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
133 eliun 4460 . . . . . . . . . . . . 13 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
134132, 133sylib 207 . . . . . . . . . . . 12 ((𝜑𝑓𝐴) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
135128, 130, 134syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
136128adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
137 elinel2 3762 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
138137adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
139138adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
140 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
141 ixpfn 7800 . . . . . . . . . . . . . . . . 17 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
142141adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
143 nfv 1830 . . . . . . . . . . . . . . . . . 18 𝑘((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
144 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑘𝑓
145 nfixp1 7814 . . . . . . . . . . . . . . . . . . 19 𝑘X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
146144, 145nfel 2763 . . . . . . . . . . . . . . . . . 18 𝑘 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))
147143, 146nfan 1816 . . . . . . . . . . . . . . . . 17 𝑘(((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
148183adant3 1074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐶𝑗):𝑋⟶ℝ)
149 simp3 1056 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑘𝑋)
150148, 149ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
151150rexrd 9968 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
152151ad5ant135 1306 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
153393adant3 1074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)):𝑋⟶ℝ)
154153, 149ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ)
155154rexrd 9968 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
156155ad5ant135 1306 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) ∈ ℝ*)
157 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
158 ioossre 12106 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)𝑌) ⊆ ℝ
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
160157, 159eqsstrd 3602 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
161 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
162 ssid 3587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝐾 → ℝ ⊆ ℝ)
164161, 163eqsstrd 3602 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
165160, 164pm2.61i 175 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
166 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
167 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
168167, 13, 26, 37hspval 39499 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169168adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → (𝐾(𝐻𝑋)𝑌) = X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170166, 169eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
171170adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
172 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → 𝑘𝑋)
173 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
174173elixp 7801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
175174biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
176175simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
177176adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → 𝑘𝑋)
179 rspa 2914 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180177, 178, 179syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
181171, 172, 180syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
182165, 181sseldi 3566 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
183182rexrd 9968 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
184183ad4ant14 1285 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
185151ad4ant124 1287 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ*)
186223adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (𝐷𝑗):𝑋⟶ℝ)
187186, 149ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ)
188187rexrd 9968 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
189188ad4ant124 1287 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
190173elixp 7801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
191190biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
192191simprd 478 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
193192adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
194 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → 𝑘𝑋)
195 rspa 2914 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
196193, 194, 195syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
197196adantll 746 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
198 icogelb 12096 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
199185, 189, 197, 198syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
200199ad5ant1345 1308 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
201 icoltub 38579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
202185, 189, 197, 201syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
203202ad5ant1345 1308 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
204203ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
205 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
206 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
207205, 206jca 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
2082073ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝜑𝑗 ∈ ℕ))
209 simp2 1055 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
210 simp3 1056 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) ≤ 𝑌)
211 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝐾))
212211breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
213212biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) ≤ 𝑌)
214213iftrued 4044 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝐾))
215211eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝐾 → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
216215adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝐾) = ((𝐷𝑗)‘𝑘))
217214, 216eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
2182173adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = ((𝐷𝑗)‘𝑘))
219 breq2 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌 → ((𝑐) ≤ 𝑦 ↔ (𝑐) ≤ 𝑌))
220 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 = 𝑌𝑦 = 𝑌)
221219, 220ifbieq2d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑌 → if((𝑐) ≤ 𝑦, (𝑐), 𝑦) = if((𝑐) ≤ 𝑌, (𝑐), 𝑌))
222221ifeq2d 4055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 𝑌 → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)) = if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))
223222mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = 𝑌 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))))
224223mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
225224adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑦 = 𝑌) → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑦, (𝑐), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
226 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑𝑚 𝑋) ∈ V
227226mptex 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))) ∈ V)
22980, 225, 37, 228fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
230229adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑌) = (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)))))
231 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → (𝑐) = ((𝐷𝑗)‘))
232231breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (𝐷𝑗) → ((𝑐) ≤ 𝑌 ↔ ((𝐷𝑗)‘) ≤ 𝑌))
233232, 231ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (𝐷𝑗) → if((𝑐) ≤ 𝑌, (𝑐), 𝑌) = if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))
234231, 233ifeq12d 4056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (𝐷𝑗) → if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌)) = if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))
235234mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (𝐷𝑗) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
236235adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷𝑗)) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), (𝑐), if((𝑐) ≤ 𝑌, (𝑐), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
237 mptexg 6389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
23813, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
239238adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑗 ∈ ℕ) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) ∈ V)
240230, 236, 20, 239fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
241240fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ℕ) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
2422413adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘))
243 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝜑)
244 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝑘 = 𝐾)
245243, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 = 𝐾) → 𝐾𝑋)
246244, 245eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 = 𝐾) → 𝑘𝑋)
247 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
248 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ( ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
249 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → ((𝐷𝑗)‘) = ((𝐷𝑗)‘𝑘))
250249breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( = 𝑘 → (((𝐷𝑗)‘) ≤ 𝑌 ↔ ((𝐷𝑗)‘𝑘) ≤ 𝑌))
251250, 249ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( = 𝑘 → if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌) = if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌))
252248, 249, 251ifbieq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( = 𝑘 → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
253252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
254 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → 𝑘𝑋)
255 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐷𝑗)‘𝑘) ∈ V
256255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((𝐷𝑗)‘𝑘) ∈ V)
257 ifexg 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐷𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
258256, 37, 257syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V)
259 ifexg 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐷𝑗)‘𝑘) ∈ V ∧ if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
260256, 258, 259syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
261260adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
262247, 253, 254, 261fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘𝑋) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
263243, 246, 262syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
264 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
265212, 211ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
266264, 211, 265ifbieq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
267266adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
268263, 267eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
2692683adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)))
270 neldifsnd 4263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
271270iffalsed 4047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
2722713ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝐾), if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌)) = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
273242, 269, 2723eqtrrd 2649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2742733expa 1257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
2752743adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
276218, 275eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
277208, 209, 210, 276syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
278277ad5ant145 1307 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
279204, 278breqtrd 4609 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
280 mnfxr 9975 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
281280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → -∞ ∈ ℝ*)
28237rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑌 ∈ ℝ*)
283282adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) → 𝑌 ∈ ℝ*)
2842833ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
2851813adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
2861573ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
287285, 286eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
288 iooltub 38582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ*𝑌 ∈ ℝ* ∧ (𝑓𝑘) ∈ (-∞(,)𝑌)) → (𝑓𝑘) < 𝑌)
289281, 284, 287, 288syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
2902893adant1r 1311 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
291290ad4ant123 1286 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < 𝑌)
292 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌)
293212notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝐾 → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
294293adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌))
295292, 294mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷𝑗)‘𝐾) ≤ 𝑌)
296295iffalsed 4047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = 𝑌)
297 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
298296, 297eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 = 𝐾 ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
299298adantll 746 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌))
300274adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
301300adantlllr 38222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
302301adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷𝑗)‘𝐾) ≤ 𝑌, ((𝐷𝑗)‘𝐾), 𝑌) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
303299, 302eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
304291, 303breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
305304ad5ant1345 1308 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷𝑗)‘𝑘) ≤ 𝑌) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
306279, 305pm2.61dan 828 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
307203adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
3082403adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑇𝑌)‘(𝐷𝑗)) = (𝑋 ↦ if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌))))
309252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) ∧ = 𝑘) → if( ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘), if(((𝐷𝑗)‘) ≤ 𝑌, ((𝐷𝑗)‘), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3102613adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) ∈ V)
311308, 309, 149, 310fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
3123113expa 1257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
313312adantllr 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
314313ad4ant13 1284 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇𝑌)‘(𝐷𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)))
315 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘𝑋)
316 neqne 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑘 = 𝐾𝑘𝐾)
317 nelsn 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘𝐾 → ¬ 𝑘 ∈ {𝐾})
318316, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
319318adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
320315, 319eldifd 3551 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
321320iftrued 4044 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
322321adantll 746 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷𝑗)‘𝑘), if(((𝐷𝑗)‘𝑘) ≤ 𝑌, ((𝐷𝑗)‘𝑘), 𝑌)) = ((𝐷𝑗)‘𝑘))
323314, 322eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
324307, 323breqtrd 4609 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
325306, 324pm2.61dan 828 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
326152, 156, 184, 200, 325elicod 12095 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
327326ex 449 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
328147, 327ralrimi 2940 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
329142, 328jca 553 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
330173elixp 7801 . . . . . . . . . . . . . . 15 (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
331329, 330sylibr 223 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
332331ex 449 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝐾(𝐻𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
333136, 139, 140, 332syl21anc 1317 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
334333reximdva 3000 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))))
335135, 334mpd 15 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
336 eliun 4460 . . . . . . . . . 10 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
337335, 336sylibr 223 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
338337ralrimiva 2949 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
339 dfss3 3558 . . . . . . . 8 ((𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
340338, 339sylibr 223 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
341 eqidd 2611 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙))))
342 fveq2 6103 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
343342fveq2d 6107 . . . . . . . . . . . . 13 (𝑙 = 𝑗 → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
344343adantl 481 . . . . . . . . . . . 12 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇𝑌)‘(𝐷𝑙)) = ((𝑇𝑌)‘(𝐷𝑗)))
345 id 22 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
346 fvex 6113 . . . . . . . . . . . . 13 ((𝑇𝑌)‘(𝐷𝑗)) ∈ V
347346a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝑇𝑌)‘(𝐷𝑗)) ∈ V)
348341, 344, 345, 347fvmptd 6197 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗) = ((𝑇𝑌)‘(𝐷𝑗)))
349348fveq1d 6105 . . . . . . . . . 10 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘) = (((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
350349oveq2d 6565 . . . . . . . . 9 (𝑗 ∈ ℕ → (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
351350ixpeq2dv 7810 . . . . . . . 8 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘)))
352351iuneq2i 4475 . . . . . . 7 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑇𝑌)‘(𝐷𝑗))‘𝑘))
353340, 352syl6sseqr 3615 . . . . . 6 (𝜑 → (𝐴 ∩ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)‘𝑘)))
35413, 15, 127, 353, 12ovnlecvr2 39500 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))))
355348oveq2d 6565 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)) = ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
356355mpteq2ia 4668 . . . . . . 7 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))
357356fveq2i 6106 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗)))))
358357a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑙 ∈ ℕ ↦ ((𝑇𝑌)‘(𝐷𝑙)))‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
359354, 358breqtrd 4609 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))))
36015ffvelrnda 6267 . . . . . . . . . 10 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋))
361 elmapi 7765 . . . . . . . . . 10 ((𝐶𝑙) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑙):𝑋⟶ℝ)
362360, 361syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ℕ) → (𝐶𝑙):𝑋⟶ℝ)
36397, 110, 111, 362hoidifhspf 39508 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ)
364 elmapg 7757 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
365121, 364syl 17 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
366365adantr 480 . . . . . . . 8 ((𝜑𝑙 ∈ ℕ) → (((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋) ↔ ((𝑆𝑌)‘(𝐶𝑙)):𝑋⟶ℝ))
367363, 366mpbird 246 . . . . . . 7 ((𝜑𝑙 ∈ ℕ) → ((𝑆𝑌)‘(𝐶𝑙)) ∈ (ℝ ↑𝑚 𝑋))
368 eqid 2610 . . . . . . 7 (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))
369367, 368fmptd 6292 . . . . . 6 (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))):ℕ⟶(ℝ ↑𝑚 𝑋))
370 simpl 472 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝜑)
371 eldifi 3694 . . . . . . . . . . . 12 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → 𝑓𝐴)
372371adantl 481 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓𝐴)
373370, 372, 134syl2anc 691 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
374141adantl 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
375 nfv 1830 . . . . . . . . . . . . . . . . 17 𝑘((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
376375, 146nfan 1816 . . . . . . . . . . . . . . . 16 𝑘(((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
377983adant3 1074 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → ((𝑆𝑌)‘(𝐶𝑗)):𝑋⟶ℝ)
378377, 149ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ)
379378rexrd 9968 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
380379ad5ant135 1306 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ∈ ℝ*)
381189adantl3r 782 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
3821503expa 1257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ∈ ℝ)
3831883expa 1257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐷𝑗)‘𝑘) ∈ ℝ*)
384 icossre 12125 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷𝑗)‘𝑘) ∈ ℝ*) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
385382, 383, 384syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
386385adantlr 747 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ⊆ ℝ)
387386, 197sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
388387rexrd 9968 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
389388ad5ant1345 1308 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ*)
390383adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑌 ∈ ℝ)
391143adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
39297, 390, 391, 148, 149hoidifhspval3 39509 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
393392ad5ant134 1305 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
394 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
395394adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
396393, 395eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
397396adantllr 751 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌))
398 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
399398adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = ((𝐶𝑗)‘𝑘))
400199adantl3r 782 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
401400ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
402399, 401eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
403 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . 23 𝑌 ≤ ((𝐶𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
404403adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) = 𝑌)
405 simpl1 1057 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))))
406 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝑘))
407 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝐾 → (𝑓𝑘) = (𝑓𝐾))
408407breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑌 ≤ (𝑓𝑘) ↔ 𝑌 ≤ (𝑓𝐾)))
409408notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
410409adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (¬ 𝑌 ≤ (𝑓𝑘) ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
411406, 410mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
4124113ad2antl3 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑌 ≤ (𝑓𝐾))
413407eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (𝑓𝐾) = (𝑓𝑘))
4144133ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) = (𝑓𝑘))
415373adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
416 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑗 ∈ ℕ) → (𝜑𝑗 ∈ ℕ))
417416ad4ant13 1284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝜑𝑗 ∈ ℕ))
418 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
419254ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑘𝑋)
420417, 418, 419, 387syl21anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓𝑘) ∈ ℝ)
421420ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘𝑋) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
422421rexlimdva 3013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
423422adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → (𝑓𝑘) ∈ ℝ))
424415, 423mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
4254243adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
426414, 425eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → (𝑓𝐾) ∈ ℝ)
427426adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) ∈ ℝ)
428405, 370, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑌 ∈ ℝ)
429427, 428ltnled 10063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ((𝑓𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓𝐾)))
430412, 429mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓𝐾) < 𝑌)
431374, 373r19.29a 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 Fn 𝑋)
432431adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → 𝑓 Fn 𝑋)
433280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ*)
434282ad4antr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ*)
435424ad4ant13 1284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
436435mnfltd 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓𝑘))
437407adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) = (𝑓𝐾))
438 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝐾) < 𝑌)
439437, 438eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓𝐾) < 𝑌𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
440439ad4ant24 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) < 𝑌)
441433, 434, 435, 436, 440eliood 38567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ (-∞(,)𝑌))
442157eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
443442adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
444441, 443eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
445424ad4ant13 1284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ ℝ)
446161eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
447446adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
448445, 447eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
449444, 448pm2.61dan 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
450449ralrimiva 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
451432, 450jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ (𝑓𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
452405, 430, 451syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
453452, 174sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
454168eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
455454ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
4564553ad2antl1 1216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → X𝑘𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻𝑋)𝑌))
457453, 456eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
458 eldifn 3695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
459458adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
4604593ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
461460adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻𝑋)𝑌))
462457, 461condan 831 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑘𝑋𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
463462ad5ant145 1307 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓𝑘))
464463adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → 𝑌 ≤ (𝑓𝑘))
465404, 464eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
466402, 465pm2.61dan 828 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌) ≤ (𝑓𝑘))
467397, 466eqbrtrd 4605 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
468392ad5ant124 1303 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)))
469 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
470469adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶𝑗)‘𝑘), ((𝐶𝑗)‘𝑘), 𝑌), ((𝐶𝑗)‘𝑘)) = ((𝐶𝑗)‘𝑘))
471468, 470eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) = ((𝐶𝑗)‘𝑘))
472199adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶𝑗)‘𝑘) ≤ (𝑓𝑘))
473471, 472eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
474473adantl4r 783 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
475467, 474pm2.61dan 828 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (((𝑆𝑌)‘(𝐶𝑗))‘𝑘) ≤ (𝑓𝑘))
476202adantl3r 782 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) < ((𝐷𝑗)‘𝑘))
477380, 381, 389, 475, 476elicod 12095 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
478477ex 449 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑘𝑋 → (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
479376, 478ralrimi 2940 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
480374, 479jca 553 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
481173elixp 7801 . . . . . . . . . . . . . 14 (𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
482480, 481sylibr 223 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
483 eqidd 2611 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙))))
484 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑗 → (𝐶𝑙) = (𝐶𝑗))
485484fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
486485adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆𝑌)‘(𝐶𝑙)) = ((𝑆𝑌)‘(𝐶𝑗)))
487 fvex 6113 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑌)‘(𝐶𝑗)) ∈ V
488487a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((𝑆𝑌)‘(𝐶𝑗)) ∈ V)
489483, 486, 345, 488fvmptd 6197 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗) = ((𝑆𝑌)‘(𝐶𝑗)))
490489fveq1d 6105 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘) = (((𝑆𝑌)‘(𝐶𝑗))‘𝑘))
491490oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
492491ixpeq2dv 7810 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
493492ad2antlr 759 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘)))
494493eleq2d 2673 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → (𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ 𝑓X𝑘𝑋 ((((𝑆𝑌)‘(𝐶𝑗))‘𝑘)[,)((𝐷𝑗)‘𝑘))))
495482, 494mpbird 246 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
496495ex 449 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
497496reximdva 3000 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
498373, 497mpd 15 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
499 eliun 4460 . . . . . . . . 9 (𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
500498, 499sylibr 223 . . . . . . . 8 ((𝜑𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) → 𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
501500ralrimiva 2949 . . . . . . 7 (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
502 dfss3 3558 . . . . . . 7 ((𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻𝑋)𝑌))𝑓 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
503501, 502sylibr 223 . . . . . 6 (𝜑 → (𝐴 ∖ (𝐾(𝐻𝑋)𝑌)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
50413, 369, 19, 503, 12ovnlecvr2 39500 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))))
505489oveq1d 6564 . . . . . . . 8 (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
506505mpteq2ia 4668 . . . . . . 7 (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))
507506fveq2i 6106 . . . . . 6 ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
508507a1i 11 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆𝑌)‘(𝐶𝑙)))‘𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
509504, 508breqtrd 4609 . . . 4 (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
5101, 2, 96, 109, 359, 509leadd12dd 38473 . . 3 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
51114, 106, 38, 18, 22, 12, 36, 97hspmbllem1 39516 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))
512511mpteq2dva 4672 . . . . 5 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗)))))
513512fveq2d 6107 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
5148, 10, 41, 105sge0xadd 39328 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))) +𝑒 (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
51596, 109rexaddd 11939 . . . 4 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) +𝑒^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))))
516513, 514, 5153eqtrrd 2649 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)((𝑇𝑌)‘(𝐷𝑗))))) + (Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆𝑌)‘(𝐶𝑗))(𝐿𝑋)(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
517510, 516breqtrd 4609 . 2 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
5183, 35, 7, 517, 34letrd 10073 1 (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑𝑚 cmap 7744  Xcixp 7794  Fincfn 7841  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  ℕcn 10897  ℝ+crp 11708   +𝑒 cxad 11820  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  ∏cprod 14474  volcvol 23039  Σ^csumge0 39255  voln*covoln 39426 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-sumge0 39256  df-ovoln 39427 This theorem is referenced by:  hspmbllem3  39518
 Copyright terms: Public domain W3C validator