Metamath Proof Explorer

Theorem hspmbllem2

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)

Ref Expression
Hypotheses 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 hspmbllem2 ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝐸 ) )

Proof

Step Hyp Ref Expression
1 hspmbllem2.h ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
2 hspmbllem2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hspmbllem2.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
4 hspmbllem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5 hspmbllem2.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6 hspmbllem2.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
7 hspmbllem2.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
8 hspmbllem2.a ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
9 hspmbllem2.g ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝐸 ) )
10 hspmbllem2.r ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
11 hspmbllem2.i ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
12 hspmbllem2.f ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
13 hspmbllem2.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
14 hspmbllem2.t ⊢ 𝑇 = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
15 hspmbllem2.s ⊢ 𝑆 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ‘ ℎ ) , ( 𝑐 ‘ ℎ ) , 𝑥 ) , ( 𝑐 ‘ ℎ ) ) ) ) )
16 11 12 readdcld ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ∈ ℝ )
17 5 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
18 10 17 readdcld ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝐸 ) ∈ ℝ )
19 nfv ⊢ Ⅎ 𝑗 𝜑
20 nnex ⊢ ℕ ∈ V
21 20 a1i ⊢ ( 𝜑 → ℕ ∈ V )
22 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
24 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
25 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
27 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) )
28 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
30 13 23 26 29 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
31 22 30 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
32 19 21 31 sge0clmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ( 0 [,] +∞ ) )
33 ne0i ⊢ ( 𝐾 ∈ 𝑋 → 𝑋 ≠ ∅ )
34 3 33 syl ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑋 ≠ ∅ )
36 13 23 35 26 29 hoidmvn0val ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
37 36 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) )
38 37 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) )
39 38 9 eqbrtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝐸 ) )
40 18 32 39 ge0lere ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
41 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑌 ∈ ℝ )
42 14 41 23 29 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑋 ⟶ ℝ )
43 13 23 26 42 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
44 22 43 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
45 19 21 44 sge0clmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
46 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ℝ ↑m 𝑥 ) = ( ℝ ↑m 𝑦 ) )
47 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
48 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
49 47 48 ifbieq2d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
50 46 46 49 mpoeq123dv ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) = ( 𝑎 ∈ ( ℝ ↑m 𝑦 ) , 𝑏 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
51 50 cbvmptv ⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑦 ) , 𝑏 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
52 13 51 eqtri ⊢ 𝐿 = ( 𝑦 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑦 ) , 𝑏 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
53 diffi ⊢ ( 𝑋 ∈ Fin → ( 𝑋 ∖ { 𝐾 } ) ∈ Fin )
54 2 53 syl ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝐾 } ) ∈ Fin )
55 snfi ⊢ { 𝐾 } ∈ Fin
56 55 a1i ⊢ ( 𝜑 → { 𝐾 } ∈ Fin )
57 unfi ⊢ ( ( ( 𝑋 ∖ { 𝐾 } ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ Fin )
58 54 56 57 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ Fin )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ Fin )
60 snidg ⊢ ( 𝐾 ∈ 𝑋 → 𝐾 ∈ { 𝐾 } )
61 3 60 syl ⊢ ( 𝜑 → 𝐾 ∈ { 𝐾 } )
62 elun2 ⊢ ( 𝐾 ∈ { 𝐾 } → 𝐾 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
63 61 62 syl ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
64 neldifsnd ⊢ ( 𝜑 → ¬ 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) )
65 63 64 eldifd ⊢ ( 𝜑 → 𝐾 ∈ ( ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∖ ( 𝑋 ∖ { 𝐾 } ) ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐾 ∈ ( ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∖ ( 𝑋 ∖ { 𝐾 } ) ) )
67 eqid ⊢ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } )
68 eqid ⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
69 uncom ⊢ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) )
70 69 a1i ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) )
71 3 snssd ⊢ ( 𝜑 → { 𝐾 } ⊆ 𝑋 )
72 undif ⊢ ( { 𝐾 } ⊆ 𝑋 ↔ ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) = 𝑋 )
73 71 72 sylib ⊢ ( 𝜑 → ( { 𝐾 } ∪ ( 𝑋 ∖ { 𝐾 } ) ) = 𝑋 )
74 70 73 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑋 )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑋 )
76 75 feq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) : ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ⟶ ℝ ↔ ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ ) )
77 26 76 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ⟶ ℝ )
78 75 feq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑗 ) : ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ⟶ ℝ ↔ ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ ) )
79 29 78 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ⟶ ℝ )
80 52 59 66 67 41 68 77 79 hsphoidmvle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( 𝐷 ‘ 𝑗 ) ) )
81 74 fveq2d ⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) = ( 𝐿 ‘ 𝑋 ) )
82 eqidd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝑗 ) )
83 14 a1i ⊢ ( 𝜑 → 𝑇 = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) )
84 74 oveq2d ⊢ ( 𝜑 → ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) = ( ℝ ↑m 𝑋 ) )
85 74 mpteq1d ⊢ ( 𝜑 → ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) )
86 84 85 mpteq12dv ⊢ ( 𝜑 → ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
87 86 eqcomd ⊢ ( 𝜑 → ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
88 87 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) )
89 83 88 eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) = 𝑇 )
90 89 fveq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) = ( 𝑇 ‘ 𝑌 ) )
91 90 fveq1d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
92 81 82 91 oveq123d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
94 81 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) = ( 𝐿 ‘ 𝑋 ) )
95 94 oveqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) )
96 93 95 breq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ↦ ( ℎ ∈ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ ( ( 𝑋 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ( 𝐷 ‘ 𝑗 ) ) ↔ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) )
97 80 96 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) )
98 19 21 44 31 97 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
99 40 45 98 ge0lere ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
100 15 41 23 26 hoidifhspf ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) : 𝑋 ⟶ ℝ )
101 13 23 100 29 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
102 101 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
103 22 a1i ⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
104 102 103 fssd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
105 21 104 sge0cl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ( 0 [,] +∞ ) )
106 22 101 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
107 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐾 ∈ 𝑋 )
108 13 23 26 29 107 15 41 hoidifhspdmvle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) )
109 19 21 106 31 108 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
110 40 105 109 ge0lere ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
111 4 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → 𝑌 ∈ ℝ )
112 2 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → 𝑋 ∈ Fin )
113 eleq1w ⊢ ( 𝑗 = 𝑙 → ( 𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ ) )
114 113 anbi2d ⊢ ( 𝑗 = 𝑙 → ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑙 ∈ ℕ ) ) )
115 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑙 ) )
116 115 feq1d ⊢ ( 𝑗 = 𝑙 → ( ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ ↔ ( 𝐷 ‘ 𝑙 ) : 𝑋 ⟶ ℝ ) )
117 114 116 imbi12d ⊢ ( 𝑗 = 𝑙 → ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐷 ‘ 𝑙 ) : 𝑋 ⟶ ℝ ) ) )
118 117 29 chvarvv ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐷 ‘ 𝑙 ) : 𝑋 ⟶ ℝ )
119 14 111 112 118 hsphoif ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ )
120 reex ⊢ ℝ ∈ V
121 120 a1i ⊢ ( 𝜑 → ℝ ∈ V )
122 121 2 jca ⊢ ( 𝜑 → ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) )
124 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ ) )
125 123 124 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ ) )
126 119 125 mpbird ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) )
127 126 fmpttd ⊢ ( 𝜑 → ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
128 simpl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝜑 )
129 elinel1 ⊢ ( 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑓 ∈ 𝐴 )
130 129 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 ∈ 𝐴 )
131 8 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
132 eliun ⊢ ( 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
133 131 132 sylib ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
134 128 130 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
135 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) → 𝜑 )
136 elinel2 ⊢ ( 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
137 136 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
138 137 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) → 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
139 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
140 ixpfn ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → 𝑓 Fn 𝑋 )
141 140 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 Fn 𝑋 )
142 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ )
143 nfcv ⊢ Ⅎ 𝑘 𝑓
144 nfixp1 ⊢ Ⅎ 𝑘 X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
145 143 144 nfel ⊢ Ⅎ 𝑘 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
146 142 145 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
147 26 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
148 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
149 147 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
150 149 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
151 150 ad5ant135 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
152 42 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑋 ⟶ ℝ )
153 152 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ )
154 153 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ* )
155 154 ad5ant135 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ* )
156 iftrue ⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( -∞ (,) 𝑌 ) )
157 ioossre ⊢ ( -∞ (,) 𝑌 ) ⊆ ℝ
158 157 a1i ⊢ ( 𝑘 = 𝐾 → ( -∞ (,) 𝑌 ) ⊆ ℝ )
159 156 158 eqsstrd ⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ )
160 iffalse ⊢ ( ¬ 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ℝ )
161 ssid ⊢ ℝ ⊆ ℝ
162 161 a1i ⊢ ( ¬ 𝑘 = 𝐾 → ℝ ⊆ ℝ )
163 160 162 eqsstrd ⊢ ( ¬ 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ )
164 159 163 pm2.61i ⊢ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ⊆ ℝ
165 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
166 1 2 3 4 hspval ⊢ ( 𝜑 → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
168 165 167 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
169 168 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
170 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
171 vex ⊢ 𝑓 ∈ V
172 171 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ) )
173 172 biimpi ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ) )
174 173 simprd ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
175 174 adantr ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
176 simpr ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
177 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
178 175 176 177 syl2anc ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
179 169 170 178 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
180 164 179 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
181 180 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ* )
182 181 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ* )
183 150 ad4ant124 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
184 29 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑗 ) : 𝑋 ⟶ ℝ )
185 184 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
186 185 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
187 186 ad4ant124 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
188 171 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
189 188 biimpi ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
190 189 simprd ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
191 190 adantr ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
192 simpr ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
193 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
194 191 192 193 syl2anc ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
195 194 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
196 icogelb ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
197 183 187 195 196 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
198 197 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
199 icoltub ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
200 183 187 195 199 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
201 200 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
202 201 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
203 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) → 𝜑 )
204 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
205 203 204 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝜑 ∧ 𝑗 ∈ ℕ ) )
206 205 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝜑 ∧ 𝑗 ∈ ℕ ) )
207 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → 𝑘 = 𝐾 )
208 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 )
209 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) )
210 209 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ↔ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 ) )
211 210 biimpa ⊢ ( ( 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 )
212 211 iftrued ⊢ ( ( 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) )
213 209 eqcomd ⊢ ( 𝑘 = 𝐾 → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
214 213 adantr ⊢ ( ( 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
215 212 214 eqtrd ⊢ ( ( 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
216 215 3adant1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
217 breq2 ⊢ ( 𝑦 = 𝑌 → ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 ↔ ( 𝑐 ‘ ℎ ) ≤ 𝑌 ) )
218 id ⊢ ( 𝑦 = 𝑌 → 𝑦 = 𝑌 )
219 217 218 ifbieq2d ⊢ ( 𝑦 = 𝑌 → if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) = if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) )
220 219 ifeq2d ⊢ ( 𝑦 = 𝑌 → if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) = if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) )
221 220 mpteq2dv ⊢ ( 𝑦 = 𝑌 → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) )
222 221 mpteq2dv ⊢ ( 𝑦 = 𝑌 → ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) ) )
223 ovex ⊢ ( ℝ ↑m 𝑋 ) ∈ V
224 223 mptex ⊢ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) ) ∈ V
225 224 a1i ⊢ ( 𝜑 → ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) ) ∈ V )
226 14 222 4 225 fvmptd3 ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑌 ) = ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) ) )
227 226 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑌 ) = ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) ) )
228 fveq1 ⊢ ( 𝑐 = ( 𝐷 ‘ 𝑗 ) → ( 𝑐 ‘ ℎ ) = ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) )
229 228 breq1d ⊢ ( 𝑐 = ( 𝐷 ‘ 𝑗 ) → ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 ↔ ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 ) )
230 229 228 ifbieq1d ⊢ ( 𝑐 = ( 𝐷 ‘ 𝑗 ) → if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) )
231 228 230 ifeq12d ⊢ ( 𝑐 = ( 𝐷 ‘ 𝑗 ) → if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) = if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) )
232 231 mpteq2dv ⊢ ( 𝑐 = ( 𝐷 ‘ 𝑗 ) → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) )
233 232 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑐 = ( 𝐷 ‘ 𝑗 ) ) → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑌 , ( 𝑐 ‘ ℎ ) , 𝑌 ) ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) )
234 mptexg ⊢ ( 𝑋 ∈ Fin → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ∈ V )
235 2 234 syl ⊢ ( 𝜑 → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ∈ V )
236 235 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ∈ V )
237 227 233 27 236 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) )
238 237 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) )
239 238 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) )
240 simpl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → 𝜑 )
241 simpr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
242 240 3 syl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → 𝐾 ∈ 𝑋 )
243 241 242 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → 𝑘 ∈ 𝑋 )
244 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) )
245 eleq1w ⊢ ( ℎ = 𝑘 → ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) ↔ 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ) )
246 fveq2 ⊢ ( ℎ = 𝑘 → ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
247 246 breq1d ⊢ ( ℎ = 𝑘 → ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 ↔ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) )
248 247 246 ifbieq1d ⊢ ( ℎ = 𝑘 → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) )
249 245 246 248 ifbieq12d ⊢ ( ℎ = 𝑘 → if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
250 249 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ ℎ = 𝑘 ) → if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
251 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
252 fvexd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ V )
253 252 4 ifexd ⊢ ( 𝜑 → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ∈ V )
254 252 253 ifexd ⊢ ( 𝜑 → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) ∈ V )
255 254 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) ∈ V )
256 244 250 251 255 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
257 240 243 256 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
258 eleq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) ↔ 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) ) )
259 210 209 ifbieq1d ⊢ ( 𝑘 = 𝐾 → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) )
260 258 209 259 ifbieq12d ⊢ ( 𝑘 = 𝐾 → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) = if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) )
261 260 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) = if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) )
262 257 261 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) = if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) )
263 262 3adant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾 ) → ( ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) ‘ 𝑘 ) = if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) )
264 neldifsnd ⊢ ( 𝑘 = 𝐾 → ¬ 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) )
265 264 iffalsed ⊢ ( 𝑘 = 𝐾 → if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) )
266 265 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾 ) → if ( 𝐾 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) ) = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) )
267 239 263 266 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
268 267 3expa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
269 268 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
270 216 269 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
271 206 207 208 270 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 = 𝐾 ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
272 271 ad5ant145 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
273 202 272 breqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
274 mnfxr ⊢ -∞ ∈ ℝ*
275 274 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → -∞ ∈ ℝ* )
276 4 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
277 276 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑌 ∈ ℝ* )
278 277 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → 𝑌 ∈ ℝ* )
279 179 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
280 156 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( -∞ (,) 𝑌 ) )
281 279 280 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) 𝑌 ) )
282 iooltub ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) 𝑌 ) ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
283 275 278 281 282 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
284 283 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
285 284 ad4ant123 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
286 simpr ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 )
287 210 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ↔ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 ) )
288 287 adantr ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ↔ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 ) )
289 286 288 mpbid ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 )
290 289 iffalsed ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = 𝑌 )
291 eqidd ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → 𝑌 = 𝑌 )
292 290 291 eqtr2d ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → 𝑌 = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) )
293 292 adantll ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → 𝑌 = if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) )
294 268 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
295 294 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
296 295 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝐾 ) , 𝑌 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
297 293 296 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → 𝑌 = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
298 285 297 breqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
299 298 adantl3r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
300 273 299 pm2.61dan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
301 201 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
302 237 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) ) )
303 249 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) ∧ ℎ = 𝑘 ) → if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ ℎ ) , 𝑌 ) ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
304 255 3adant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) ∈ V )
305 302 303 148 304 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
306 305 3expa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
307 306 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
308 307 ad4ant13 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) )
309 simpl ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾 ) → 𝑘 ∈ 𝑋 )
310 neqne ⊢ ( ¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾 )
311 nelsn ⊢ ( 𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ { 𝐾 } )
312 310 311 syl ⊢ ( ¬ 𝑘 = 𝐾 → ¬ 𝑘 ∈ { 𝐾 } )
313 312 adantl ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾 ) → ¬ 𝑘 ∈ { 𝐾 } )
314 309 313 eldifd ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾 ) → 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) )
315 314 iftrued ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾 ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
316 315 adantll ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → if ( 𝑘 ∈ ( 𝑋 ∖ { 𝐾 } ) , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ≤ 𝑌 , ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
317 308 316 eqtr2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
318 301 317 breqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
319 300 318 pm2.61dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) < ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
320 151 155 182 198 319 elicod ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
321 320 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ 𝑋 → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
322 146 321 ralrimi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
323 141 322 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
324 171 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
325 323 324 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
326 325 ex ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
327 135 138 139 326 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
328 327 reximdva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ( ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
329 134 328 mpd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
330 eliun ⊢ ( 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
331 329 330 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
332 331 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
333 dfss3 ⊢ ( ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ↔ ∀ 𝑓 ∈ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
334 332 333 sylibr ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
335 eqidd ⊢ ( 𝑗 ∈ ℕ → ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) = ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) )
336 2fveq3 ⊢ ( 𝑙 = 𝑗 → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
337 336 adantl ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑙 = 𝑗 ) → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) = ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
338 id ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
339 fvexd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ∈ V )
340 335 337 338 339 fvmptd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) = ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
341 340 fveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
342 341 oveq2d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
343 342 ixpeq2dv ⊢ ( 𝑗 ∈ ℕ → X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
344 343 iuneq2i ⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ‘ 𝑘 ) )
345 334 344 sseqtrrdi ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) ) )
346 2 6 127 345 13 ovnlecvr2 ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ) ) ) )
347 340 oveq2d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
348 347 mpteq2ia ⊢ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
349 348 fveq2i ⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
350 349 a1i ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
351 346 350 breqtrd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
352 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐶 ‘ 𝑙 ) ∈ ( ℝ ↑m 𝑋 ) )
353 elmapi ⊢ ( ( 𝐶 ‘ 𝑙 ) ∈ ( ℝ ↑m 𝑋 ) → ( 𝐶 ‘ 𝑙 ) : 𝑋 ⟶ ℝ )
354 352 353 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐶 ‘ 𝑙 ) : 𝑋 ⟶ ℝ )
355 15 111 112 354 hoidifhspf ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ )
356 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ Fin ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ ) )
357 122 356 syl ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ ) )
358 357 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) : 𝑋 ⟶ ℝ ) )
359 355 358 mpbird ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ∈ ( ℝ ↑m 𝑋 ) )
360 359 fmpttd ⊢ ( 𝜑 → ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) )
361 simpl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝜑 )
362 eldifi ⊢ ( 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → 𝑓 ∈ 𝐴 )
363 362 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 ∈ 𝐴 )
364 361 363 133 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
365 140 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 Fn 𝑋 )
366 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ )
367 366 145 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
368 100 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) : 𝑋 ⟶ ℝ )
369 368 148 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ )
370 369 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ* )
371 370 ad5ant135 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℝ* )
372 187 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
373 149 3expa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ )
374 186 3expa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* )
375 icossre ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ∈ ℝ* ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
376 373 374 375 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
377 376 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ⊆ ℝ )
378 377 195 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
379 378 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ* )
380 379 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ* )
381 41 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → 𝑌 ∈ ℝ )
382 23 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → 𝑋 ∈ Fin )
383 15 381 382 147 148 hoidifhspval3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) )
384 383 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) )
385 iftrue ⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) = if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) )
386 385 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) = if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) )
387 384 386 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) )
388 387 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) )
389 iftrue ⊢ ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
390 389 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
391 197 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
392 391 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
393 390 392 eqbrtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ≤ ( 𝑓 ‘ 𝑘 ) )
394 iffalse ⊢ ( ¬ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) = 𝑌 )
395 394 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) = 𝑌 )
396 simpl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) )
397 simpr ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) )
398 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝐾 ) )
399 398 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ↔ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) ) )
400 399 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ↔ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) ) )
401 400 adantr ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ↔ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) ) )
402 397 401 mpbid ⊢ ( ( 𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ¬ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) )
403 402 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ¬ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) )
404 398 eqcomd ⊢ ( 𝑘 = 𝐾 → ( 𝑓 ‘ 𝐾 ) = ( 𝑓 ‘ 𝑘 ) )
405 404 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝐾 ) = ( 𝑓 ‘ 𝑘 ) )
406 364 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
407 id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝜑 ∧ 𝑗 ∈ ℕ ) )
408 407 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝜑 ∧ 𝑗 ∈ ℕ ) )
409 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
410 251 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ 𝑋 )
411 408 409 410 378 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
412 411 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ ) )
413 412 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ ) )
414 406 413 mpd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
415 414 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
416 405 415 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝐾 ) ∈ ℝ )
417 416 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝐾 ) ∈ ℝ )
418 396 361 4 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → 𝑌 ∈ ℝ )
419 417 418 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑓 ‘ 𝐾 ) < 𝑌 ↔ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝐾 ) ) )
420 403 419 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝐾 ) < 𝑌 )
421 365 364 r19.29a ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 Fn 𝑋 )
422 421 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) → 𝑓 Fn 𝑋 )
423 274 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → -∞ ∈ ℝ* )
424 276 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → 𝑌 ∈ ℝ* )
425 414 ad4ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
426 425 mnfltd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → -∞ < ( 𝑓 ‘ 𝑘 ) )
427 398 adantl ⊢ ( ( ( 𝑓 ‘ 𝐾 ) < 𝑌 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝐾 ) )
428 simpl ⊢ ( ( ( 𝑓 ‘ 𝐾 ) < 𝑌 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝐾 ) < 𝑌 )
429 427 428 eqbrtrd ⊢ ( ( ( 𝑓 ‘ 𝐾 ) < 𝑌 ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
430 429 ad4ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) < 𝑌 )
431 423 424 425 426 430 eliood ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) 𝑌 ) )
432 156 eqcomd ⊢ ( 𝑘 = 𝐾 → ( -∞ (,) 𝑌 ) = if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
433 432 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( -∞ (,) 𝑌 ) = if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
434 431 433 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
435 414 ad4ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
436 160 eqcomd ⊢ ( ¬ 𝑘 = 𝐾 → ℝ = if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
437 436 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ℝ = if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
438 435 437 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
439 434 438 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
440 439 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
441 422 440 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ( 𝑓 ‘ 𝐾 ) < 𝑌 ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ) )
442 396 420 441 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) ) )
443 442 172 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) )
444 166 eqcomd ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
445 444 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
446 445 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐾 , ( -∞ (,) 𝑌 ) , ℝ ) = ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
447 443 446 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
448 eldifn ⊢ ( 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) → ¬ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
449 448 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ¬ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
450 449 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → ¬ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
451 450 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) ) → ¬ 𝑓 ∈ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) )
452 447 451 condan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾 ) → 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) )
453 452 ad5ant145 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) )
454 453 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → 𝑌 ≤ ( 𝑓 ‘ 𝑘 ) )
455 395 454 eqbrtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) ∧ ¬ 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ≤ ( 𝑓 ‘ 𝑘 ) )
456 393 455 pm2.61dan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) ≤ ( 𝑓 ‘ 𝑘 ) )
457 388 456 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
458 383 ad5ant124 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) )
459 iffalse ⊢ ( ¬ 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
460 459 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) , 𝑌 ) , ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
461 458 460 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) )
462 197 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
463 461 462 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
464 463 adantl4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
465 457 464 pm2.61dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) ≤ ( 𝑓 ‘ 𝑘 ) )
466 200 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) < ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) )
467 371 372 380 465 466 elicod ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
468 467 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ 𝑋 → ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
469 367 468 ralrimi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
470 365 469 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
471 171 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
472 470 471 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
473 eqidd ⊢ ( 𝑗 ∈ ℕ → ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) = ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) )
474 2fveq3 ⊢ ( 𝑙 = 𝑗 → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) = ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) )
475 474 adantl ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑙 = 𝑗 ) → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) = ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) )
476 fvexd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ V )
477 473 475 338 476 fvmptd ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) )
478 477 fveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) )
479 478 oveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
480 479 ixpeq2dv ⊢ ( 𝑗 ∈ ℕ → X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
481 480 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
482 481 eleq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
483 472 482 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
484 483 ex ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
485 484 reximdva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ( ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
486 364 485 mpd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
487 eliun ⊢ ( 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
488 486 487 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
489 488 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
490 dfss3 ⊢ ( ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ↔ ∀ 𝑓 ∈ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
491 489 490 sylibr ⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
492 2 360 7 491 13 ovnlecvr2 ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
493 477 oveq1d ⊢ ( 𝑗 ∈ ℕ → ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) )
494 493 mpteq2ia ⊢ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) )
495 494 fveq2i ⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) )
496 495 a1i ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑙 ∈ ℕ ↦ ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
497 492 496 breqtrd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
498 11 12 99 110 351 497 leadd12dd ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
499 23 107 41 26 29 13 14 15 hspmbllem1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) )
500 499 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
501 500 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
502 19 21 44 106 sge0xadd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) +𝑒 ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
503 99 110 rexaddd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
504 501 502 503 3eqtrrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑇 ‘ 𝑌 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑆 ‘ 𝑌 ) ‘ ( 𝐶 ‘ 𝑗 ) ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
505 498 504 breqtrd ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑋 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
506 16 40 18 505 39 letrd ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝐸 ) )