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 44800
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 11180 . 2 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ∈ ℝ)
4 hspmbllem2.r . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜π΄) ∈ ℝ)
5 hspmbllem2.e . . . . 5 (πœ‘ β†’ 𝐸 ∈ ℝ+)
65rpred 12949 . . . 4 (πœ‘ β†’ 𝐸 ∈ ℝ)
74, 6readdcld 11180 . . 3 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸) ∈ ℝ)
8 nfv 1917 . . . 4 β„²π‘—πœ‘
9 nnex 12155 . . . . 5 β„• ∈ V
109a1i 11 . . . 4 (πœ‘ β†’ β„• ∈ V)
11 icossicc 13345 . . . . 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 8783 . . . . . . 7 ((πΆβ€˜π‘—) ∈ (ℝ ↑m 𝑋) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
1816, 17syl 17 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
19 hspmbllem2.d . . . . . . . 8 (πœ‘ β†’ 𝐷:β„•βŸΆ(ℝ ↑m 𝑋))
2019ffvelcdmda 7031 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—) ∈ (ℝ ↑m 𝑋))
21 elmapi 8783 . . . . . . 7 ((π·β€˜π‘—) ∈ (ℝ ↑m 𝑋) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
2220, 21syl 17 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
2312, 14, 18, 22hoidmvcl 44755 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,)+∞))
2411, 23sselid 3940 . . . 4 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,]+∞))
258, 10, 24sge0clmpt 44598 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ (0[,]+∞))
26 hspmbllem2.k . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ 𝑋)
27 ne0i 4292 . . . . . . . . 9 (𝐾 ∈ 𝑋 β†’ 𝑋 β‰  βˆ…)
2826, 27syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑋 β‰  βˆ…)
2928adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑋 β‰  βˆ…)
3012, 14, 29, 18, 22hoidmvn0val 44757 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
3130mpteq2dva 5203 . . . . 5 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))))
3231fveq2d 6843 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))))
33 hspmbllem2.g . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))) ≀ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸))
3432, 33eqbrtrd 5125 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π΄) + 𝐸))
357, 25, 34ge0lere 43702 . 2 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ ℝ)
36 hspmbllem2.t . . . . . . . . 9 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
37 hspmbllem2.y . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
3837adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ π‘Œ ∈ ℝ)
3936, 38, 14, 22hsphoif 44749 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)):π‘‹βŸΆβ„)
4012, 14, 18, 39hoidmvcl 44755 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ∈ (0[,)+∞))
4111, 40sselid 3940 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
428, 10, 41sge0clmpt 44598 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞))
43 oveq2 7361 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ (ℝ ↑m π‘₯) = (ℝ ↑m 𝑦))
44 eqeq1 2740 . . . . . . . . . . . 12 (π‘₯ = 𝑦 β†’ (π‘₯ = βˆ… ↔ 𝑦 = βˆ…))
45 prodeq1 15784 . . . . . . . . . . . 12 (π‘₯ = 𝑦 β†’ βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))) = βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))
4644, 45ifbieq2d 4510 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ if(π‘₯ = βˆ…, 0, βˆπ‘˜ ∈ π‘₯ (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜)))) = if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜)))))
4743, 43, 46mpoeq123dv 7428 . . . . . . . . . 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 2764 . . . . . . . 8 𝐿 = (𝑦 ∈ Fin ↦ (π‘Ž ∈ (ℝ ↑m 𝑦), 𝑏 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = βˆ…, 0, βˆπ‘˜ ∈ 𝑦 (volβ€˜((π‘Žβ€˜π‘˜)[,)(π‘β€˜π‘˜))))))
50 diffi 9119 . . . . . . . . . . 11 (𝑋 ∈ Fin β†’ (𝑋 βˆ– {𝐾}) ∈ Fin)
5113, 50syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 βˆ– {𝐾}) ∈ Fin)
52 snfi 8984 . . . . . . . . . . 11 {𝐾} ∈ Fin
5352a1i 11 . . . . . . . . . 10 (πœ‘ β†’ {𝐾} ∈ Fin)
54 unfi 9112 . . . . . . . . . 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 2736 . . . . . . . 8 ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})
65 eqid 2736 . . . . . . . 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 2776 . . . . . . . . . . 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 44759 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)))
7871fveq2d 6843 . . . . . . . . . 10 (πœ‘ β†’ (πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (πΏβ€˜π‘‹))
79 eqidd 2737 . . . . . . . . . 10 (πœ‘ β†’ (πΆβ€˜π‘—) = (πΆβ€˜π‘—))
8036a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))))
8171oveq2d 7369 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (ℝ ↑m 𝑋))
8271mpteq1d 5198 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))) = (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))
8381, 82mpteq12dv 5194 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))) = (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
8483eqcomd 2742 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))) = (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))
8584mpteq2dv 5205 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))))
8680, 85eqtr2d 2777 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦))))) = 𝑇)
8786fveq1d 6841 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ) = (π‘‡β€˜π‘Œ))
8887fveq1d 6841 . . . . . . . . . 10 (πœ‘ β†’ (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—)) = ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))
8978, 79, 88oveq123d 7374 . . . . . . . . 9 (πœ‘ β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
9089adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
9178adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) = (πΏβ€˜π‘‹))
9291oveqd 7370 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
9390, 92breq12d 5116 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})) ↦ (β„Ž ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) ↦ if(β„Ž ∈ (𝑋 βˆ– {𝐾}), (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ 𝑦, (π‘β€˜β„Ž), 𝑦)))))β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))(π·β€˜π‘—)) ↔ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))))
9477, 93mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
958, 10, 41, 24, 94sge0lempt 44583 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
9635, 42, 95ge0lere 43702 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) ∈ ℝ)
97 hspmbllem2.s . . . . . . . . . 10 𝑆 = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž = 𝐾, if(π‘₯ ≀ (π‘β€˜β„Ž), (π‘β€˜β„Ž), π‘₯), (π‘β€˜β„Ž)))))
9897, 38, 14, 18hoidifhspf 44791 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)):π‘‹βŸΆβ„)
9912, 14, 98, 22hoidmvcl 44755 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,)+∞))
10099fmpttd 7059 . . . . . . 7 (πœ‘ β†’ (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))):β„•βŸΆ(0[,)+∞))
10111a1i 11 . . . . . . 7 (πœ‘ β†’ (0[,)+∞) βŠ† (0[,]+∞))
102100, 101fssd 6683 . . . . . 6 (πœ‘ β†’ (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))):β„•βŸΆ(0[,]+∞))
10310, 102sge0cl 44554 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ∈ (0[,]+∞))
10411, 99sselid 3940 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ∈ (0[,]+∞))
10526adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝐾 ∈ 𝑋)
10612, 14, 18, 22, 105, 97, 38hoidifhspdmvle 44793 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))
1078, 10, 104, 24, 106sge0lempt 44583 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
10835, 103, 107ge0lere 43702 . . . 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 44749 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)):π‘‹βŸΆβ„)
118 reex 11138 . . . . . . . . . . . 12 ℝ ∈ V
119118a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ ℝ ∈ V)
120119, 13jca 512 . . . . . . . . . 10 (πœ‘ β†’ (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121120adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122 elmapg 8774 . . . . . . . . 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 8837 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) β†’ 𝑓 Fn 𝑋)
140139adantl 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 Fn 𝑋)
141 nfv 1917 . . . . . . . . . . . . . . . . . 18 β„²π‘˜((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•)
142 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜π‘“
143 nfixp1 8852 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))
144142, 143nfel 2919 . . . . . . . . . . . . . . . . . 18 β„²π‘˜ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))
145141, 144nfan 1902 . . . . . . . . . . . . . . . . 17 β„²π‘˜(((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
146183adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (πΆβ€˜π‘—):π‘‹βŸΆβ„)
147 simp3 1138 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
148146, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ)
149148rexrd 11201 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
150149ad5ant135 1368 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
151393adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)):π‘‹βŸΆβ„)
152151, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ)
153152rexrd 11201 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ*)
154153ad5ant135 1368 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜) ∈ ℝ*)
155 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (-∞(,)π‘Œ))
156 ioossre 13317 . . . . . . . . . . . . . . . . . . . . . . . . 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 44782 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11201 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
182181ad4ant14 750 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
183149ad4ant124 1173 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ*)
184223adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (π·β€˜π‘—):π‘‹βŸΆβ„)
185184, 147ffvelcdmd 7032 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ)
186185rexrd 11201 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
187186ad4ant124 1173 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
188171elixp 8838 . . . . . . . . . . . . . . . . . . . . . . . . . 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 13307 . . . . . . . . . . . . . . . . . . . . 21 ((((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
197183, 187, 195, 196syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
198197adantl3r 748 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ≀ (π‘“β€˜π‘˜))
199 icoltub 43678 . . . . . . . . . . . . . . . . . . . . . . . . 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 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ = 𝐾 β†’ ((π·β€˜π‘—)β€˜πΎ) = ((π·β€˜π‘—)β€˜π‘˜))
214213adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜πΎ) = ((π·β€˜π‘—)β€˜π‘˜))
215212, 214eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
2682673expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
2692683adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
270216, 269eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
271206, 207, 208, 270syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ = 𝐾 ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
272271ad5ant145 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
273202, 272breqtrd 5129 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
274 mnfxr 11208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -∞ ∈ ℝ*
275274a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ -∞ ∈ ℝ*)
27637rexrd 11201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ π‘Œ ∈ ℝ*)
277276adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) β†’ π‘Œ ∈ ℝ*)
2782773ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ π‘Œ ∈ ℝ*)
2791793adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
2801553ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ) = (-∞(,)π‘Œ))
281279, 280eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ π‘˜ ∈ 𝑋 ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)π‘Œ))
282 iooltub 43680 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = π‘Œ)
292290, 291eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘˜ = 𝐾 ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
293292adantll 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ π‘Œ = if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ))
294268adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
295294adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
296295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) ∧ Β¬ ((π·β€˜π‘—)β€˜π‘˜) ≀ π‘Œ) β†’ if(((π·β€˜π‘—)β€˜πΎ) ≀ π‘Œ, ((π·β€˜π‘—)β€˜πΎ), π‘Œ) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
297293, 296eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ ((π·β€˜π‘—)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
318301, 317breqtrd 5129 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
319300, 318pm2.61dan 811 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < (((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
320150, 154, 182, 198, 319elicod 13306 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
321320ex 413 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘˜ ∈ 𝑋 β†’ (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
322145, 321ralrimi 3238 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
323140, 322jca 512 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝐾(π»β€˜π‘‹)π‘Œ)) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))))
324171elixp 8838 . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . 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 7369 . . . . . . . . 9 (𝑗 ∈ β„• β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
343342ixpeq2dv 8847 . . . . . . . 8 (𝑗 ∈ β„• β†’ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜)))
344343iuneq2i 4973 . . . . . . 7 βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)) = βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))β€˜π‘˜))
345334, 344sseqtrrdi 3993 . . . . . 6 (πœ‘ β†’ (𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ)) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)(((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)β€˜π‘˜)))
34613, 15, 125, 345, 12ovnlecvr2 44783 . . . . 5 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))))
347340oveq2d 7369 . . . . . . . 8 (𝑗 ∈ β„• β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)) = ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
348347mpteq2ia 5206 . . . . . . 7 (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—))) = (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))
349348fveq2i 6842 . . . . . 6 (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—)))))
350349a1i 11 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((𝑙 ∈ β„• ↦ ((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘™)))β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))))
351346, 350breqtrd 5129 . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))))
35215ffvelcdmda 7031 . . . . . . . . . 10 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (πΆβ€˜π‘™) ∈ (ℝ ↑m 𝑋))
353 elmapi 8783 . . . . . . . . . 10 ((πΆβ€˜π‘™) ∈ (ℝ ↑m 𝑋) β†’ (πΆβ€˜π‘™):π‘‹βŸΆβ„)
354352, 353syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ (πΆβ€˜π‘™):π‘‹βŸΆβ„)
35597, 109, 110, 354hoidifhspf 44791 . . . . . . . 8 ((πœ‘ ∧ 𝑙 ∈ β„•) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)):π‘‹βŸΆβ„)
356 elmapg 8774 . . . . . . . . . 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 11201 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ∈ ℝ*)
371370ad5ant135 1368 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) ∈ ℝ*)
372187adantl3r 748 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
3731483expa 1118 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ ((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ)
3741863expa 1118 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*)
375 icossre 13337 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πΆβ€˜π‘—)β€˜π‘˜) ∈ ℝ ∧ ((π·β€˜π‘—)β€˜π‘˜) ∈ ℝ*) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
376373, 374, 375syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
377376adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) βŠ† ℝ)
378377, 195sseldd 3943 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
379378rexrd 11201 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
380379adantl3r 748 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ*)
381383adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ π‘Œ ∈ ℝ)
382143adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ 𝑋 ∈ Fin)
38397, 381, 382, 146, 147hoidifhspval3 44792 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ π‘˜ ∈ 𝑋) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)))
384383ad5ant134 1367 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)))
385 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝐾 β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
386385adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ), ((πΆβ€˜π‘—)β€˜π‘˜)) = if(π‘Œ ≀ ((πΆβ€˜π‘—)β€˜π‘˜), ((πΆβ€˜π‘—)β€˜π‘˜), π‘Œ))
387384, 386eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 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 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ -∞ < (π‘“β€˜π‘˜))
427398adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) = (π‘“β€˜πΎ))
428 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜πΎ) < π‘Œ)
429427, 428eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((π‘“β€˜πΎ) < π‘Œ ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
430429ad4ant24 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) < π‘Œ)
431423, 424, 425, 426, 430eliood 43668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)π‘Œ))
432155eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ = 𝐾 β†’ (-∞(,)π‘Œ) = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
433432adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (-∞(,)π‘Œ) = if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
434431, 433eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝐾, (-∞(,)π‘Œ), ℝ))
435414ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ (π‘“β€˜πΎ) < π‘Œ) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝐾) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
436159eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . . . . . . . . . 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 13306 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
468467ex 413 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (π‘˜ ∈ 𝑋 β†’ (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
469367, 468ralrimi 3238 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
470365, 469jca 512 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
471171elixp 8838 . . . . . . . . . . . . . 14 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))))
472470, 471sylibr 233 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ (𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ∧ 𝑗 ∈ β„•) ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 (((πΆβ€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
473 eqidd 2737 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ (𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™))) = (𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™))))
474 2fveq3 6844 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
475474adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ β„• ∧ 𝑙 = 𝑗) β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
476 fvexd 6854 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)) ∈ V)
477473, 475, 338, 476fvmptd 6952 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ β„• β†’ ((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—) = ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—)))
478477fveq1d 6841 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• β†’ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜) = (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜))
479478oveq1d 7368 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„• β†’ ((((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)) = ((((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))β€˜π‘˜)[,)((π·β€˜π‘—)β€˜π‘˜)))
480479ixpeq2dv 8847 . . . . . . . . . . . . . . 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 44783 . . . . 5 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
493477oveq1d 7368 . . . . . . . 8 (𝑗 ∈ β„• β†’ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))
494493mpteq2ia 5206 . . . . . . 7 (𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))
495494fveq2i 6842 . . . . . 6 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))
496495a1i 11 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((𝑙 ∈ β„• ↦ ((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘™)))β€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
497492, 496breqtrd 5129 . . . 4 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
4981, 2, 96, 108, 351, 497leadd12dd 43486 . . 3 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ≀ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
49914, 105, 38, 18, 22, 12, 36, 97hspmbllem1 44799 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)) = (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))
500499mpteq2dva 5203 . . . . 5 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—))) = (𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
501500fveq2d 6843 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
5028, 10, 41, 104sge0xadd 44608 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))) +𝑒 (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) +𝑒 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
50396, 108rexaddd 13145 . . . 4 (πœ‘ β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) +𝑒 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))))
504501, 502, 5033eqtrrd 2781 . . 3 (πœ‘ β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜(π·β€˜π‘—))))) + (Ξ£^β€˜(𝑗 ∈ β„• ↦ (((π‘†β€˜π‘Œ)β€˜(πΆβ€˜π‘—))(πΏβ€˜π‘‹)(π·β€˜π‘—))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
505498, 504breqtrd 5129 . 2 (πœ‘ β†’ (((voln*β€˜π‘‹)β€˜(𝐴 ∩ (𝐾(π»β€˜π‘‹)π‘Œ))) + ((voln*β€˜π‘‹)β€˜(𝐴 βˆ– (𝐾(π»β€˜π‘‹)π‘Œ)))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘‹)(π·β€˜π‘—)))))
5063, 35, 7, 505, 34letrd 11308 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 7353   ∈ cmpo 7355   ↑m cmap 8761  Xcixp 8831  Fincfn 8879  β„cr 11046  0cc0 11047   + caddc 11050  +∞cpnf 11182  -∞cmnf 11183  β„*cxr 11184   < clt 11185   ≀ cle 11186  β„•cn 12149  β„+crp 12907   +𝑒 cxad 13023  (,)cioo 13256  [,)cico 13258  [,]cicc 13259  βˆcprod 15780  volcvol 24811  Ξ£^csumge0 44535  voln*covoln 44709
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 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-inf2 9573  ax-cnex 11103  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123  ax-pre-mulgt0 11124  ax-pre-sup 11125
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  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 7309  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7613  df-om 7799  df-1st 7917  df-2nd 7918  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-2o 8409  df-er 8644  df-map 8763  df-pm 8764  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fi 9343  df-sup 9374  df-inf 9375  df-oi 9442  df-dju 9833  df-card 9871  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190  df-le 11191  df-sub 11383  df-neg 11384  df-div 11809  df-nn 12150  df-2 12212  df-3 12213  df-n0 12410  df-z 12496  df-uz 12760  df-q 12866  df-rp 12908  df-xneg 13025  df-xadd 13026  df-xmul 13027  df-ioo 13260  df-ico 13262  df-icc 13263  df-fz 13417  df-fzo 13560  df-fl 13689  df-seq 13899  df-exp 13960  df-hash 14223  df-cj 14976  df-re 14977  df-im 14978  df-sqrt 15112  df-abs 15113  df-clim 15362  df-rlim 15363  df-sum 15563  df-prod 15781  df-rest 17296  df-topgen 17317  df-psmet 20773  df-xmet 20774  df-met 20775  df-bl 20776  df-mopn 20777  df-top 22227  df-topon 22244  df-bases 22280  df-cmp 22722  df-ovol 24812  df-vol 24813  df-sumge0 44536  df-ovoln 44710
This theorem is referenced by:  hspmbllem3  44801
  Copyright terms: Public domain W3C validator