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 44769
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 11142 . 2 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜π΄) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (πœ‘ β†’ 𝐸 ∈ ℝ+)
65rpred 12911 . . . 4 (πœ‘ β†’ 𝐸 ∈ ℝ)
74, 6readdcld 11142 . . 3 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸) ∈ ℝ)
8 nfv 1917 . . . 4 β„²π‘—πœ‘
9 nnex 12117 . . . . 5 β„• ∈ V
109a1i 11 . . . 4 (πœ‘ β†’ β„• ∈ V)
11 icossicc 13307 . . . . 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 𝑋))
1615ffvelcdmda 7031 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—) ∈ (ℝ ↑m 𝑋))
17 elmapi 8745 . . . . . . 7 ((πΆβ€˜π‘—) ∈ (ℝ ↑m 𝑋) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
1816, 17syl 17 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
19 hspmbllem2.d . . . . . . . 8 (πœ‘ β†’ 𝐷:β„•βŸΆ(ℝ ↑m 𝑋))
2019ffvelcdmda 7031 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—) ∈ (ℝ ↑m 𝑋))
21 elmapi 8745 . . . . . . 7 ((π·β€˜π‘—) ∈ (ℝ ↑m 𝑋) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
2220, 21syl 17 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
2312, 14, 18, 22hoidmvcl 44724 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,)+∞))
2411, 23sselid 3940 . . . 4 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 44567 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ 𝑋)
27 ne0i 4292 . . . . . . . . 9 (𝐾 ∈ 𝑋 β†’ 𝑋 β‰  βˆ…)
2826, 27syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑋 β‰  βˆ…)
2928adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑋 β‰  βˆ…)
3012, 14, 29, 18, 22hoidmvn0val 44726 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
3130mpteq2dva 5203 . . . . 5 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))))
3231fveq2d 6843 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))))
33 hspmbllem2.g . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))) ≀ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸))
3432, 33eqbrtrd 5125 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸))
357, 25, 34ge0lere 43671 . 2 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
3837adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ π‘Œ ∈ ℝ)
3936, 38, 14, 22hsphoif 44718 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)):π‘‹βŸΆβ„)
4012, 14, 18, 39hoidmvcl 44724 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ∈ (0[,)+∞))
4111, 40sselid 3940 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 44567 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞))
43 oveq2 7359 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ (ℝ ↑m π‘₯) = (ℝ ↑m 𝑦))
44 eqeq1 2741 . . . . . . . . . . . 12 (π‘₯ = 𝑦 β†’ (π‘₯ = βˆ… ↔ 𝑦 = βˆ…))
45 prodeq1 15752 . . . . . . . . . . . 12 (π‘₯ = 𝑦 β†’ βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))) = βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))
4644, 45ifbieq2d 4510 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ if(π‘₯ = βˆ…, 0, βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜)))) = if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜)))))
4743, 43, 46mpoeq123dv 7426 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ (π‘Ž ∈ (ℝ ↑m π‘₯), 𝑏 ∈ (ℝ ↑m π‘₯) ↦ if(π‘₯ = βˆ…, 0, βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))) = (π‘Ž ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))))
4847cbvmptv 5216 . . . . . . . . 9 (π‘₯ ∈ Fin ↦ (π‘Ž ∈ (ℝ ↑m π‘₯), 𝑏 ∈ (ℝ ↑m π‘₯) ↦ if(π‘₯ = βˆ…, 0, βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜)))))) = (𝑦 ∈ Fin ↦ (π‘Ž ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))))
4912, 48eqtri 2765 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (π‘Ž ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))))
50 diffi 9081 . . . . . . . . . . 11 (𝑋 ∈ Fin β†’ (𝑋 βˆ– {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 βˆ– {𝐾}) ∈ Fin)
52 snfi 8946 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {𝐾} ∈ Fin)
54 unfi 9074 . . . . . . . . . 10 (((𝑋 βˆ– {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ∈ Fin)
5551, 53, 54syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ∈ Fin)
5655adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ∈ Fin)
57 snidg 4618 . . . . . . . . . . . 12 (𝐾 ∈ 𝑋 β†’ 𝐾 ∈ {𝐾})
5826, 57syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ {𝐾})
59 elun2 4135 . . . . . . . . . . 11 (𝐾 ∈ {𝐾} β†’ 𝐾 ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))
6058, 59syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐾 ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))
61 neldifsnd 4751 . . . . . . . . . 10 (πœ‘ β†’ Β¬ 𝐾 ∈ (𝑋 βˆ– {𝐾}))
6260, 61eldifd 3919 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ (((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) βˆ– (𝑋 βˆ– {𝐾})))
6362adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝐾 ∈ (((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) βˆ– (𝑋 βˆ– {𝐾})))
64 eqid 2737 . . . . . . . 8 ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})
65 eqid 2737 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
66 uncom 4111 . . . . . . . . . . . . 13 ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ({𝐾} βˆͺ (𝑋 βˆ– {𝐾}))
6766a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})))
6826snssd 4767 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝐾} βŠ† 𝑋)
69 undif 4439 . . . . . . . . . . . . 13 ({𝐾} βŠ† 𝑋 ↔ ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})) = 𝑋)
7068, 69sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})) = 𝑋)
7167, 70eqtrd 2777 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = 𝑋)
7271adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = 𝑋)
7372feq2d 6651 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—):((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})βŸΆβ„ ↔ (πΆβ€˜π‘—):π‘‹βŸΆβ„))
7418, 73mpbird 256 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—):((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})βŸΆβ„)
7572feq2d 6651 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π·β€˜π‘—):((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})βŸΆβ„ ↔ (π·β€˜π‘—):π‘‹βŸΆβ„))
7622, 75mpbird 256 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})βŸΆβ„)
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 44728 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)))
7871fveq2d 6843 . . . . . . . . . 10 (πœ‘ β†’ (πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (πΏβ€˜π‘‹))
79 eqidd 2738 . . . . . . . . . 10 (πœ‘ β†’ (πΆβ€˜π‘—) = (πΆβ€˜π‘—))
8036a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))))
8171oveq2d 7367 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (ℝ ↑m 𝑋))
8271mpteq1d 5198 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))
8381, 82mpteq12dv 5194 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
8483eqcomd 2743 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))) = (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
8584mpteq2dv 5205 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))))
8680, 85eqtr2d 2778 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))) = 𝑇)
8786fveq1d 6841 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ) = (π‘‡β€˜π‘Œ))
8887fveq1d 6841 . . . . . . . . . 10 (πœ‘ β†’ (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—)) = ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))
8978, 79, 88oveq123d 7372 . . . . . . . . 9 (πœ‘ β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
9089adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
9178adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (πΏβ€˜π‘‹))
9291oveqd 7368 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
9390, 92breq12d 5116 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)) ↔ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))))
9477, 93mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
958, 10, 41, 24, 94sge0lempt 44552 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
9635, 42, 95ge0lere 43671 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž = 𝐾, if(π‘₯ ≀ (π‘β€˜β„Ž), (π‘β€˜β„Ž), π‘₯), (π‘β€˜β„Ž)))))
9897, 38, 14, 18hoidifhspf 44760 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)):π‘‹βŸΆβ„)
9912, 14, 98, 22hoidmvcl 44724 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,)+∞))
10099fmpttd 7059 . . . . . . 7 (πœ‘ β†’ (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))):β„•βŸΆ(0[,)+∞))
10111a1i 11 . . . . . . 7 (πœ‘ β†’ (0[,)+∞) βŠ† (0[,]+∞))
102100, 101fssd 6683 . . . . . 6 (πœ‘ β†’ (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))):β„•βŸΆ(0[,]+∞))
10310, 102sge0cl 44523 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ (0[,]+∞))
10411, 99sselid 3940 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,]+∞))
10526adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝐾 ∈ 𝑋)
10612, 14, 18, 22, 105, 97, 38hoidifhspdmvle 44762 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
1078, 10, 104, 24, 106sge0lempt 44552 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
10835, 103, 107ge0lere 43671 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ ℝ)
10937adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ π‘Œ ∈ ℝ)
11013adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ 𝑋 ∈ Fin)
111 eleq1w 2820 . . . . . . . . . . . 12 (𝑗 = 𝑙 β†’ (𝑗 ∈ β„• ↔ 𝑙 ∈ β„•))
112111anbi2d 629 . . . . . . . . . . 11 (𝑗 = 𝑙 β†’ ((πœ‘ ∧ 𝑗 ∈ β„•) ↔ (πœ‘ ∧ 𝑙 ∈ β„•)))
113 fveq2 6839 . . . . . . . . . . . 12 (𝑗 = 𝑙 β†’ (π·β€˜π‘—) = (π·β€˜π‘™))
114113feq1d 6650 . . . . . . . . . . 11 (𝑗 = 𝑙 β†’ ((π·β€˜π‘—):π‘‹βŸΆβ„ ↔ (π·β€˜π‘™):π‘‹βŸΆβ„))
115112, 114imbi12d 344 . . . . . . . . . 10 (𝑗 = 𝑙 β†’ (((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„) ↔ ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (π·β€˜π‘™):π‘‹βŸΆβ„)))
116115, 22chvarvv 2002 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (π·β€˜π‘™):π‘‹βŸΆβ„)
11736, 109, 110, 116hsphoif 44718 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)):π‘‹βŸΆβ„)
118 reex 11100 . . . . . . . . . . . 12 ℝ ∈ V
119118a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ ℝ ∈ V)
120119, 13jca 512 . . . . . . . . . 10 (πœ‘ β†’ (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121120adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122 elmapg 8736 . . . . . . . . 9 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)) ∈ (ℝ ↑m 𝑋) ↔ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)):π‘‹βŸΆβ„))
123121, 122syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)) ∈ (ℝ ↑m 𝑋) ↔ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)):π‘‹βŸΆβ„))
124117, 123mpbird 256 . . . . . . 7 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)) ∈ (ℝ ↑m 𝑋))
125124fmpttd 7059 . . . . . 6 (πœ‘ β†’ (𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™))):β„•βŸΆ(ℝ ↑m 𝑋))
126 simpl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ πœ‘)
127 elinel1 4153 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ 𝑓 ∈ 𝐴)
128127adantl 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ 𝑓 ∈ 𝐴)
129 hspmbllem2.a . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
130129sselda 3942 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
131 eliun 4956 . . . . . . . . . . . . 13 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
132130, 131sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
133126, 128, 132syl2anc 584 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
134 simpll 765 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) β†’ πœ‘)
135 elinel2 4154 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
136135adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
137136adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) β†’ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
138 simpr 485 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
139 ixpfn 8799 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ 𝑓 Fn 𝑋)
140139adantl 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 Fn 𝑋)
141 nfv 1917 . . . . . . . . . . . . . . . . . 18 β„²π‘˜((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•)
142 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜π‘“
143 nfixp1 8814 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))
144142, 143nfel 2919 . . . . . . . . . . . . . . . . . 18 β„²π‘˜ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))
145141, 144nfan 1902 . . . . . . . . . . . . . . . . 17 β„²π‘˜(((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
146183adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
147 simp3 1138 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
148146, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ)
149148rexrd 11163 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
150149ad5ant135 1368 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
151393adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)):π‘‹βŸΆβ„)
152151, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ)
153152rexrd 11163 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ*)
154153ad5ant135 1368 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ*)
155 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (-∞(,)π‘Œ))
156 ioossre 13279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-∞(,)π‘Œ) βŠ† ℝ
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝐾 β†’ (-∞(,)π‘Œ) βŠ† ℝ)
158155, 157eqsstrd 3980 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) βŠ† ℝ)
159 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = ℝ)
160 ssid 3964 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ βŠ† ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘˜ = 𝐾 β†’ ℝ βŠ† ℝ)
162159, 161eqsstrd 3980 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) βŠ† ℝ)
163158, 162pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . 22 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) βŠ† ℝ
164 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
165 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)))
166165, 13, 26, 37hspval 44751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐾(π»β€˜π‘‹)π‘Œ) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
167166adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ (𝐾(π»β€˜π‘‹)π‘Œ) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
168164, 167eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
169168adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
170 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
171 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑓 ∈ V
172171elixp 8800 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3229 . . . . . . . . . . . . . . . . . . . . . . . 24 ((βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
178175, 176, 177syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
179169, 170, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
180163, 179sselid 3940 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
181180rexrd 11163 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
182181ad4ant14 750 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
183149ad4ant124 1173 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
184223adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
185184, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ)
186185rexrd 11163 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
187186ad4ant124 1173 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
188171elixp 8800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
189188biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
190189simprd 496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
191190adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ∧ π‘˜ ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
192 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
193 rspa 3229 . . . . . . . . . . . . . . . . . . . . . . 23 ((βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
194191, 192, 193syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
195194adantll 712 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
196 icogelb 13269 . . . . . . . . . . . . . . . . . . . . 21 ((((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
197183, 187, 195, 196syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
198197adantl3r 748 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
199 icoltub 43647 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
200183, 187, 195, 199syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
201200adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
202201ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
203 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) β†’ πœ‘)
204 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
205203, 204jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) β†’ (πœ‘ ∧ 𝑗 ∈ β„•))
2062053ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (πœ‘ ∧ 𝑗 ∈ β„•))
207 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘˜ = 𝐾)
208 simp3 1138 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ)
209 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘˜ = 𝐾 β†’ ((π·β€˜π‘—)β€˜π‘˜) = ((π·β€˜π‘—)β€˜πΎ))
210209breq1d 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = 𝐾 β†’ (((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ ↔ ((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ))
211210biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ)
212211iftrued 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = ((π·β€˜π‘—)β€˜πΎ))
213209eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ = 𝐾 β†’ ((π·β€˜π‘—)β€˜πΎ) = ((π·β€˜π‘—)β€˜π‘˜))
214213adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜πΎ) = ((π·β€˜π‘—)β€˜π‘˜))
215212, 214eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = ((π·β€˜π‘—)β€˜π‘˜))
2162153adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = ((π·β€˜π‘—)β€˜π‘˜))
217 breq2 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = π‘Œ β†’ ((π‘β€˜β„Ž) ≀ 𝑦 ↔ (π‘β€˜β„Ž) ≀ π‘Œ))
218 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = π‘Œ β†’ 𝑦 = π‘Œ)
219217, 218ifbieq2d 4510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = π‘Œ β†’ if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦) = if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ))
220219ifeq2d 4504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = π‘Œ β†’ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)) = if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))
221220mpteq2dv 5205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = π‘Œ β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ))))
222221mpteq2dv 5205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = π‘Œ β†’ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))))
223 ovex 7384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (ℝ ↑m 𝑋) ∈ V
224223mptex 7169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))) ∈ V
225224a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (πœ‘ β†’ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))) ∈ V)
22636, 222, 37, 225fvmptd3 6968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (πœ‘ β†’ (π‘‡β€˜π‘Œ) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))))
227226adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘‡β€˜π‘Œ) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)))))
228 fveq1 6838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (π·β€˜π‘—) β†’ (π‘β€˜β„Ž) = ((π·β€˜π‘—)β€˜β„Ž))
229228breq1d 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (π·β€˜π‘—) β†’ ((π‘β€˜β„Ž) ≀ π‘Œ ↔ ((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ))
230229, 228ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (π·β€˜π‘—) β†’ if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ) = if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))
231228, 230ifeq12d 4505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (π·β€˜π‘—) β†’ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ)) = if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))
232231mpteq2dv 5205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = (π·β€˜π‘—) β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))))
233232adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑐 = (π·β€˜π‘—)) β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘Œ, (π‘β€˜β„Ž), π‘Œ))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))))
234 mptexg 7167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋 ∈ Fin β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))) ∈ V)
23513, 234syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (πœ‘ β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))) ∈ V)
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))) ∈ V)
237227, 233, 20, 236fvmptd 6952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))))
238237fveq1d 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜))
2392383adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ = 𝐾) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜))
240 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ πœ‘)
241 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ π‘˜ = 𝐾)
242240, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ 𝐾 ∈ 𝑋)
243241, 242eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ π‘˜ ∈ 𝑋)
244 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))))
245 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (β„Ž = π‘˜ β†’ (β„Ž ∈ (𝑋 βˆ– {𝐾}) ↔ π‘˜ ∈ (𝑋 βˆ– {𝐾})))
246 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (β„Ž = π‘˜ β†’ ((π·β€˜π‘—)β€˜β„Ž) = ((π·β€˜π‘—)β€˜π‘˜))
247246breq1d 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (β„Ž = π‘˜ β†’ (((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ ↔ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ))
248247, 246ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (β„Ž = π‘˜ β†’ if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ) = if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ))
249245, 246, 248ifbieq12d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (β„Ž = π‘˜ β†’ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
250249adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ π‘˜ ∈ 𝑋) ∧ β„Ž = π‘˜) β†’ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
251 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
252 fvexd 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (πœ‘ β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ V)
253252, 37ifexd 4532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (πœ‘ β†’ if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ) ∈ V)
254252, 253ifexd 4532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (πœ‘ β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) ∈ V)
255254adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) ∈ V)
256244, 250, 251, 255fvmptd 6952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
257240, 243, 256syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
258 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘˜ = 𝐾 β†’ (π‘˜ ∈ (𝑋 βˆ– {𝐾}) ↔ 𝐾 ∈ (𝑋 βˆ– {𝐾})))
259210, 209ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘˜ = 𝐾 β†’ if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ) = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
260258, 209, 259ifbieq12d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ = 𝐾 β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) = if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)))
261260adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) = if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)))
262257, 261eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘˜ = 𝐾) β†’ ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜) = if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)))
2632623adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ = 𝐾) β†’ ((β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)))β€˜π‘˜) = if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)))
264 neldifsnd 4751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘˜ = 𝐾 β†’ Β¬ 𝐾 ∈ (𝑋 βˆ– {𝐾}))
265264iffalsed 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = 𝐾 β†’ if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)) = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
2662653ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ = 𝐾) β†’ if(𝐾 ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜πΎ), if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ)) = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
267239, 263, 2663eqtrrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
2682673expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
2692683adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
270216, 269eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
271206, 207, 208, 270syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
272271ad5ant145 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
273202, 272breqtrd 5129 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
274 mnfxr 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
275274a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ -∞ ∈ ℝ*)
27637rexrd 11163 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ π‘Œ ∈ ℝ*)
277276adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ π‘Œ ∈ ℝ*)
2782773ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ π‘Œ ∈ ℝ*)
2791793adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
2801553ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (-∞(,)π‘Œ))
281279, 280eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)π‘Œ))
282 iooltub 43649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-∞ ∈ ℝ* ∧ π‘Œ ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ (-∞(,)π‘Œ)) β†’ (π‘“β€˜π‘˜) < π‘Œ)
283275, 278, 281, 282syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
2842833adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
285284ad4ant123 1172 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < π‘Œ)
286 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ)
287210notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ = 𝐾 β†’ (Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ ↔ Β¬ ((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ))
288287adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ ↔ Β¬ ((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ))
289286, 288mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ Β¬ ((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ)
290289iffalsed 4495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = π‘Œ)
291 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = π‘Œ)
292290, 291eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
293292adantll 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
294268adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
295294adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
296295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
297293, 296eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
298285, 297breqtrd 5129 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
299298adantl3r 748 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
300273, 299pm2.61dan 811 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
301201adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
3022373adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ))))
303249adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) ∧ β„Ž = π‘˜) β†’ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜β„Ž), if(((π·β€˜π‘—)β€˜β„Ž) ≀ π‘Œ, ((π·β€˜π‘—)β€˜β„Ž), π‘Œ)) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
3042553adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) ∈ V)
305302, 303, 147, 304fvmptd 6952 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
3063053expa 1118 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
307306adantllr 717 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
308307ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)))
309 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘˜ ∈ 𝑋 ∧ Β¬ π‘˜ = 𝐾) β†’ π‘˜ ∈ 𝑋)
310 neqne 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Β¬ π‘˜ = 𝐾 β†’ π‘˜ β‰  𝐾)
311 nelsn 4624 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ β‰  𝐾 β†’ Β¬ π‘˜ ∈ {𝐾})
312310, 311syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Β¬ π‘˜ = 𝐾 β†’ Β¬ π‘˜ ∈ {𝐾})
313312adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘˜ ∈ 𝑋 ∧ Β¬ π‘˜ = 𝐾) β†’ Β¬ π‘˜ ∈ {𝐾})
314309, 313eldifd 3919 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘˜ ∈ 𝑋 ∧ Β¬ π‘˜ = 𝐾) β†’ π‘˜ ∈ (𝑋 βˆ– {𝐾}))
315314iftrued 4492 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ ∈ 𝑋 ∧ Β¬ π‘˜ = 𝐾) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) = ((π·β€˜π‘—)β€˜π‘˜))
316315adantll 712 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), ((π·β€˜π‘—)β€˜π‘˜), if(((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ, ((π·β€˜π‘—)β€˜π‘˜), π‘Œ)) = ((π·β€˜π‘—)β€˜π‘˜))
317308, 316eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
318301, 317breqtrd 5129 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
319300, 318pm2.61dan 811 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
320150, 154, 182, 198, 319elicod 13268 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
321320ex 413 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘˜ ∈ 𝑋 β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
322145, 321ralrimi 3238 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
323140, 322jca 512 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
324171elixp 8800 . . . . . . . . . . . . . . 15 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
325323, 324sylibr 233 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
326325ex 413 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) β†’ (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
327134, 137, 138, 326syl21anc 836 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) β†’ (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
328327reximdva 3163 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ (βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
329133, 328mpd 15 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
330 eliun 4956 . . . . . . . . . 10 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
331329, 330sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
332331ralrimiva 3141 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘“ ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
333 dfss3 3930 . . . . . . . 8 ((𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)) ↔ βˆ€π‘“ ∈ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
334332, 333sylibr 233 . . . . . . 7 (πœ‘ β†’ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
335 eqidd 2738 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ (𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™))) = (𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™))))
336 2fveq3 6844 . . . . . . . . . . . . 13 (𝑙 = 𝑗 β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)) = ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))
337336adantl 482 . . . . . . . . . . . 12 ((𝑗 ∈ β„• ∧ 𝑙 = 𝑗) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)) = ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))
338 id 22 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•)
339 fvexd 6854 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)) ∈ V)
340335, 337, 338, 339fvmptd 6952 . . . . . . . . . . 11 (𝑗 ∈ β„• β†’ ((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—) = ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))
341340fveq1d 6841 . . . . . . . . . 10 (𝑗 ∈ β„• β†’ (((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
342341oveq2d 7367 . . . . . . . . 9 (𝑗 ∈ β„• β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
343342ixpeq2dv 8809 . . . . . . . 8 (𝑗 ∈ β„• β†’ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
344343iuneq2i 4973 . . . . . . 7 βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
345334, 344sseqtrrdi 3993 . . . . . 6 (πœ‘ β†’ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)))
34613, 15, 125, 345, 12ovnlecvr2 44752 . . . . 5 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))))
347340oveq2d 7367 . . . . . . . 8 (𝑗 ∈ β„• β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
348347mpteq2ia 5206 . . . . . . 7 (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—))) = (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
349348fveq2i 6842 . . . . . 6 (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))))
350349a1i 11 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))))
351346, 350breqtrd 5129 . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))))
35215ffvelcdmda 7031 . . . . . . . . . 10 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (πΆβ€˜π‘™) ∈ (ℝ ↑m 𝑋))
353 elmapi 8745 . . . . . . . . . 10 ((πΆβ€˜π‘™) ∈ (ℝ ↑m 𝑋) β†’ (πΆβ€˜π‘™):π‘‹βŸΆβ„)
354352, 353syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (πΆβ€˜π‘™):π‘‹βŸΆβ„)
35597, 109, 110, 354hoidifhspf 44760 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)):π‘‹βŸΆβ„)
356 elmapg 8736 . . . . . . . . . 10 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) ∈ (ℝ ↑m 𝑋) ↔ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)):π‘‹βŸΆβ„))
357120, 356syl 17 . . . . . . . . 9 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) ∈ (ℝ ↑m 𝑋) ↔ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)):π‘‹βŸΆβ„))
358357adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) ∈ (ℝ ↑m 𝑋) ↔ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)):π‘‹βŸΆβ„))
359355, 358mpbird 256 . . . . . . 7 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) ∈ (ℝ ↑m 𝑋))
360359fmpttd 7059 . . . . . 6 (πœ‘ β†’ (𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™))):β„•βŸΆ(ℝ ↑m 𝑋))
361 simpl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ πœ‘)
362 eldifi 4084 . . . . . . . . . . . 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 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)):π‘‹βŸΆβ„)
369368, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ∈ ℝ)
370369rexrd 11163 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ∈ ℝ*)
371370ad5ant135 1368 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ∈ ℝ*)
372187adantl3r 748 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
3731483expa 1118 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ)
3741863expa 1118 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
375 icossre 13299 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ ∧ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
376373, 374, 375syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
377376adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
378377, 195sseldd 3943 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
379378rexrd 11163 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
380379adantl3r 748 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
381383adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ π‘Œ ∈ ℝ)
382143adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ 𝑋 ∈ Fin)
38397, 381, 382, 146, 147hoidifhspval3 44761 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)))
384383ad5ant134 1367 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)))
385 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
386385adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
387384, 386eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
388387adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
389 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) = ((πΆβ€˜π‘—)β€˜π‘˜))
390389adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) = ((πΆβ€˜π‘—)β€˜π‘˜))
391197adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
392391ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
393390, 392eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) ≀ (π‘“β€˜π‘˜))
394 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) = π‘Œ)
395394adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) = π‘Œ)
396 simpl1 1191 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ (πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))))
397 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘˜ = 𝐾 ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜))
398 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (π‘˜ = 𝐾 β†’ (π‘“β€˜π‘˜) = (π‘“β€˜πΎ))
399398breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝐾 β†’ (π‘Œ ≀ (π‘“β€˜π‘˜) ↔ π‘Œ ≀ (π‘“β€˜πΎ)))
400399notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘˜ = 𝐾 β†’ (Β¬ π‘Œ ≀ (π‘“β€˜π‘˜) ↔ Β¬ π‘Œ ≀ (π‘“β€˜πΎ)))
401400adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘˜ = 𝐾 ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ (Β¬ π‘Œ ≀ (π‘“β€˜π‘˜) ↔ Β¬ π‘Œ ≀ (π‘“β€˜πΎ)))
402397, 401mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘˜ = 𝐾 ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Β¬ π‘Œ ≀ (π‘“β€˜πΎ))
4034023ad2antl3 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Β¬ π‘Œ ≀ (π‘“β€˜πΎ))
404398eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝐾 β†’ (π‘“β€˜πΎ) = (π‘“β€˜π‘˜))
4054043ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜πΎ) = (π‘“β€˜π‘˜))
406364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
407 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πœ‘ ∧ 𝑗 ∈ β„•))
408407ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((πœ‘ ∧ π‘˜ ∈ 𝑋) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (πœ‘ ∧ 𝑗 ∈ β„•))
409 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((πœ‘ ∧ π‘˜ ∈ 𝑋) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
410251ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((πœ‘ ∧ π‘˜ ∈ 𝑋) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ π‘˜ ∈ 𝑋)
411408, 409, 410, 378syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((πœ‘ ∧ π‘˜ ∈ 𝑋) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
412411rexlimdva2 3152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ ℝ))
413412adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋) β†’ (βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ ℝ))
414406, 413mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
4154143adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
416405, 415eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜πΎ) ∈ ℝ)
417416adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜πΎ) ∈ ℝ)
418396, 361, 373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ π‘Œ ∈ ℝ)
419417, 418ltnled 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ ((π‘“β€˜πΎ) < π‘Œ ↔ Β¬ π‘Œ ≀ (π‘“β€˜πΎ)))
420403, 419mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜πΎ) < π‘Œ)
421365, 364r19.29a 3157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ 𝑓 Fn 𝑋)
422421adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) β†’ 𝑓 Fn 𝑋)
423274a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ -∞ ∈ ℝ*)
424276ad4antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ π‘Œ ∈ ℝ*)
425414ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
426425mnfltd 12999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ -∞ < (π‘“β€˜π‘˜))
427398adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) = (π‘“β€˜πΎ))
428 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜πΎ) < π‘Œ)
429427, 428eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
430429ad4ant24 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
431423, 424, 425, 426, 430eliood 43637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)π‘Œ))
432155eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝐾 β†’ (-∞(,)π‘Œ) = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
433432adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (-∞(,)π‘Œ) = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
434431, 433eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
435414ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
436159eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Β¬ π‘˜ = 𝐾 β†’ ℝ = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
437436adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ ℝ = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
438435, 437eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
439434, 438pm2.61dan 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
440439ralrimiva 3141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
441422, 440jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ)))
442396, 420, 441syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ)))
443442, 172sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
444166eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (𝐾(π»β€˜π‘‹)π‘Œ))
445444ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (𝐾(π»β€˜π‘‹)π‘Œ))
4464453ad2antl1 1185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (𝐾(π»β€˜π‘‹)π‘Œ))
447443, 446eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
448 eldifn 4085 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ Β¬ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
449448adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ Β¬ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
4504493ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ Β¬ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
451450adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ (π‘“β€˜π‘˜)) β†’ Β¬ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ))
452447, 451condan 816 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ π‘Œ ≀ (π‘“β€˜π‘˜))
453452ad5ant145 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ π‘Œ ≀ (π‘“β€˜π‘˜))
454453adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ π‘Œ ≀ (π‘“β€˜π‘˜))
455395, 454eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜)) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) ≀ (π‘“β€˜π‘˜))
456393, 455pm2.61dan 811 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ) ≀ (π‘“β€˜π‘˜))
457388, 456eqbrtrd 5125 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
458383ad5ant124 1365 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)))
459 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = ((πΆβ€˜π‘—)β€˜π‘˜))
460459adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = ((πΆβ€˜π‘—)β€˜π‘˜))
461458, 460eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = ((πΆβ€˜π‘—)β€˜π‘˜))
462197adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
463461, 462eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
464463adantl4r 753 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
465457, 464pm2.61dan 811 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
466200adantl3r 748 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < ((π·β€˜π‘—)β€˜π‘˜))
467371, 372, 380, 465, 466elicod 13268 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
468467ex 413 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘˜ ∈ 𝑋 β†’ (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
469367, 468ralrimi 3238 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
470365, 469jca 512 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
471171elixp 8800 . . . . . . . . . . . . . 14 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
472470, 471sylibr 233 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
473 eqidd 2738 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ (𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™))) = (𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™))))
474 2fveq3 6844 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
475474adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ β„• ∧ 𝑙 = 𝑗) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
476 fvexd 6854 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)) ∈ V)
477473, 475, 338, 476fvmptd 6952 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ β„• β†’ ((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
478477fveq1d 6841 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• β†’ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜) = (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜))
479478oveq1d 7366 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„• β†’ ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) = ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
480479ixpeq2dv 8809 . . . . . . . . . . . . . . 15 (𝑗 ∈ β„• β†’ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) = Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
481480ad2antlr 725 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) = Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
482481eleq2d 2823 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
483472, 482mpbird 256 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
484483ex 413 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) β†’ (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
485484reximdva 3163 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ (βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
486364, 485mpd 15 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
487 eliun 4956 . . . . . . . . 9 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
488486, 487sylibr 233 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
489488ralrimiva 3141 . . . . . . 7 (πœ‘ β†’ βˆ€π‘“ ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
490 dfss3 3930 . . . . . . 7 ((𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ βˆ€π‘“ ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))𝑓 ∈ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
491489, 490sylibr 233 . . . . . 6 (πœ‘ β†’ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
49213, 360, 19, 491, 12ovnlecvr2 44752 . . . . 5 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
493477oveq1d 7366 . . . . . . . 8 (𝑗 ∈ β„• β†’ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))
494493mpteq2ia 5206 . . . . . . 7 (𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))
495494fveq2i 6842 . . . . . 6 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))
496495a1i 11 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
497492, 496breqtrd 5129 . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
4981, 2, 96, 108, 351, 497leadd12dd 43455 . . 3 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ≀ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
49914, 105, 38, 18, 22, 12, 36, 97hspmbllem1 44768 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))
500499mpteq2dva 5203 . . . . 5 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
501500fveq2d 6843 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
5028, 10, 41, 104sge0xadd 44577 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) +𝑒 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
50396, 108rexaddd 13107 . . . 4 (πœ‘ β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) +𝑒 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
504501, 502, 5033eqtrrd 2782 . . 3 (πœ‘ β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
505498, 504breqtrd 5129 . 2 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
5063, 35, 7, 505, 34letrd 11270 1 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ≀ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   βˆ– cdif 3905   βˆͺ cun 3906   ∩ cin 3907   βŠ† wss 3908  βˆ…c0 4280  ifcif 4484  {csn 4584  βˆͺ ciun 4952   class class class wbr 5103   ↦ cmpt 5186   Fn wfn 6488  βŸΆwf 6489  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353   ↑m cmap 8723  Xcixp 8793  Fincfn 8841  β„cr 11008  0cc0 11009   + caddc 11012  +∞cpnf 11144  -∞cmnf 11145  β„*cxr 11146   < clt 11147   ≀ cle 11148  β„•cn 12111  β„+crp 12869   +𝑒 cxad 12985  (,)cioo 13218  [,)cico 13220  [,]cicc 13221  βˆcprod 15748  volcvol 24779  Ξ£^csumge0 44504  voln*covoln 44678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-2o 8405  df-er 8606  df-map 8725  df-pm 8726  df-ixp 8794  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fi 9305  df-sup 9336  df-inf 9337  df-oi 9404  df-dju 9795  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-n0 12372  df-z 12458  df-uz 12722  df-q 12828  df-rp 12870  df-xneg 12987  df-xadd 12988  df-xmul 12989  df-ioo 13222  df-ico 13224  df-icc 13225  df-fz 13379  df-fzo 13522  df-fl 13651  df-seq 13861  df-exp 13922  df-hash 14185  df-cj 14944  df-re 14945  df-im 14946  df-sqrt 15080  df-abs 15081  df-clim 15330  df-rlim 15331  df-sum 15531  df-prod 15749  df-rest 17264  df-topgen 17285  df-psmet 20741  df-xmet 20742  df-met 20743  df-bl 20744  df-mopn 20745  df-top 22195  df-topon 22212  df-bases 22248  df-cmp 22690  df-ovol 24780  df-vol 24781  df-sumge0 44505  df-ovoln 44679
This theorem is referenced by:  hspmbllem3  44770
  Copyright terms: Public domain W3C validator