Step | Hyp | Ref
| Expression |
1 | | hspmbllem2.i |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
2 | | hspmbllem2.f |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) |
3 | 1, 2 | readdcld 10069 |
. 2
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ) |
4 | | hspmbllem2.r |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) |
5 | | hspmbllem2.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
6 | 5 | rpred 11872 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ℝ) |
7 | 4, 6 | readdcld 10069 |
. . 3
⊢ (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ) |
8 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑗𝜑 |
9 | | nnex 11026 |
. . . . 5
⊢ ℕ
∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
11 | | icossicc 12260 |
. . . . 5
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
12 | | hspmbllem2.l |
. . . . . 6
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
13 | | hspmbllem2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ Fin) |
14 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
15 | | hspmbllem2.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑋)) |
16 | 15 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
17 | | elmapi 7879 |
. . . . . . 7
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐶‘𝑗):𝑋⟶ℝ) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
19 | | hspmbllem2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑋)) |
20 | 19 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
21 | | elmapi 7879 |
. . . . . . 7
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐷‘𝑗):𝑋⟶ℝ) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
23 | 12, 14, 18, 22 | hoidmvcl 40796 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
24 | 11, 23 | sseldi 3601 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
25 | 8, 10, 24 | sge0clmpt 40642 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞)) |
26 | | hspmbllem2.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ 𝑋) |
27 | | ne0i 3921 |
. . . . . . . . 9
⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ ∅) |
29 | 28 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅) |
30 | 12, 14, 29, 18, 22 | hoidmvn0val 40798 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
31 | 30 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) |
32 | 31 | fveq2d 6195 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
33 | | hspmbllem2.g |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) |
34 | 32, 33 | eqbrtrd 4675 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) |
35 | 7, 25, 34 | ge0lere 39759 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ) |
36 | | hspmbllem2.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) |
37 | | hspmbllem2.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
38 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ ℝ) |
39 | 36, 38, 14, 22 | hsphoif 40790 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ) |
40 | 12, 14, 18, 39 | hoidmvcl 40796 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
41 | 11, 40 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
42 | 8, 10, 41 | sge0clmpt 40642 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ (0[,]+∞)) |
43 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (ℝ ↑𝑚
𝑥) = (ℝ
↑𝑚 𝑦)) |
44 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
45 | | prodeq1 14639 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) |
46 | 44, 45 | ifbieq2d 4111 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) |
47 | 43, 43, 46 | mpt2eq123dv 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚
𝑦), 𝑏 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
48 | 47 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑦), 𝑏 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
49 | 12, 48 | eqtri 2644 |
. . . . . . . 8
⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑦), 𝑏 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
50 | | diffi 8192 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin) |
51 | 13, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin) |
52 | | snfi 8038 |
. . . . . . . . . . 11
⊢ {𝐾} ∈ Fin |
53 | 52 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐾} ∈ Fin) |
54 | | unfi 8227 |
. . . . . . . . . 10
⊢ (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin) |
55 | 51, 53, 54 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin) |
56 | 55 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin) |
57 | | snidg 4206 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ {𝐾}) |
58 | 26, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ {𝐾}) |
59 | | elun2 3781 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})) |
61 | | neldifsnd 4322 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾})) |
62 | 60, 61 | eldifd 3585 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾}))) |
63 | 62 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾}))) |
64 | | eqid 2622 |
. . . . . . . 8
⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾}) |
65 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) |
66 | | uncom 3757 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})) |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))) |
68 | 26 | snssd 4340 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐾} ⊆ 𝑋) |
69 | | undif 4049 |
. . . . . . . . . . . . 13
⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋) |
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋) |
71 | 67, 70 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋) |
72 | 71 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋) |
73 | 72 | feq2d 6031 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶‘𝑗):𝑋⟶ℝ)) |
74 | 18, 73 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ) |
75 | 72 | feq2d 6031 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷‘𝑗):𝑋⟶ℝ)) |
76 | 22, 75 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ) |
77 | 49, 56, 63, 64, 38, 65, 74, 76 | hsphoidmvle 40800 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗))) |
78 | 71 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋)) |
79 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘𝑗) = (𝐶‘𝑗)) |
80 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))) |
81 | 71 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ
↑𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑𝑚
𝑋)) |
82 | 71 | mpteq1d 4738 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) |
83 | 81, 82 | mpteq12dv 4733 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) |
84 | 83 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) |
85 | 84 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))) |
86 | 80, 85 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = 𝑇) |
87 | 86 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌) = (𝑇‘𝑌)) |
88 | 87 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗)) = ((𝑇‘𝑌)‘(𝐷‘𝑗))) |
89 | 78, 79, 88 | oveq123d 6671 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))) |
90 | 89 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))) |
91 | 78 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋)) |
92 | 91 | oveqd 6667 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) |
93 | 90, 92 | breq12d 4666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) ↔ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) |
94 | 77, 93 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) |
95 | 8, 10, 41, 24, 94 | sge0lempt 40627 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
96 | 35, 42, 95 | ge0lere 39759 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ ℝ) |
97 | | hspmbllem2.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) |
98 | 97, 38, 14, 18 | hoidifhspf 40832 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ) |
99 | 12, 14, 98, 22 | hoidmvcl 40796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
100 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))) |
101 | 99, 100 | fmptd 6385 |
. . . . . . 7
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞)) |
102 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) |
103 | 101, 102 | fssd 6057 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞)) |
104 | 10, 103 | sge0cl 40598 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞)) |
105 | 11, 99 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
106 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ 𝑋) |
107 | 12, 14, 18, 22, 106, 97, 38 | hoidifhspdmvle 40834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) |
108 | 8, 10, 105, 24, 107 | sge0lempt 40627 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
109 | 35, 104, 108 | ge0lere 39759 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ) |
110 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑌 ∈ ℝ) |
111 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑋 ∈ Fin) |
112 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ)) |
113 | 112 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑙 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑙 ∈ ℕ))) |
114 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙)) |
115 | 114 | feq1d 6030 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑙 → ((𝐷‘𝑗):𝑋⟶ℝ ↔ (𝐷‘𝑙):𝑋⟶ℝ)) |
116 | 113, 115 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) ↔ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ))) |
117 | 116, 22 | chvarv 2263 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ) |
118 | 36, 110, 111, 117 | hsphoif 40790 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ) |
119 | | reex 10027 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
120 | 119 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ∈
V) |
121 | 120, 13 | jca 554 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ ∈ V ∧
𝑋 ∈
Fin)) |
122 | 121 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (ℝ ∈ V
∧ 𝑋 ∈
Fin)) |
123 | | elmapg 7870 |
. . . . . . . . 9
⊢ ((ℝ
∈ V ∧ 𝑋 ∈
Fin) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑𝑚
𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)) |
124 | 122, 123 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑𝑚
𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)) |
125 | 118, 124 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑𝑚
𝑋)) |
126 | | eqid 2622 |
. . . . . . 7
⊢ (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) |
127 | 125, 126 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))):ℕ⟶(ℝ
↑𝑚 𝑋)) |
128 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑) |
129 | | elinel1 3799 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴) |
130 | 129 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴) |
131 | | hspmbllem2.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
132 | 131 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
133 | | eliun 4524 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
134 | 132, 133 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
135 | 128, 130,
134 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
136 | 128 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑) |
137 | | elinel2 3800 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
138 | 137 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
139 | 138 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
140 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
141 | | ixpfn 7914 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 Fn 𝑋) |
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋) |
143 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) |
144 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘𝑓 |
145 | | nfixp1 7928 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) |
146 | 144, 145 | nfel 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) |
147 | 143, 146 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
148 | 18 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ) |
149 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
150 | 148, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ) |
151 | 150 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈
ℝ*) |
152 | 151 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈
ℝ*) |
153 | 39 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ) |
154 | 153, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ) |
155 | 154 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈
ℝ*) |
156 | 155 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈
ℝ*) |
157 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌)) |
158 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(-∞(,)𝑌)
⊆ ℝ |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ) |
160 | 157, 159 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆
ℝ) |
161 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ) |
162 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℝ
⊆ ℝ |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑘 = 𝐾 → ℝ ⊆
ℝ) |
164 | 161, 163 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆
ℝ) |
165 | 160, 164 | pm2.61i 176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ |
166 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
167 | | hspmbllem2.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) |
168 | 167, 13, 26, 37 | hspval 40823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
169 | 168 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
170 | 166, 169 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
171 | 170 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
172 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
173 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑓 ∈ V |
174 | 173 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))) |
175 | 174 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))) |
176 | 175 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
177 | 176 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
178 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
179 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((∀𝑘 ∈
𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
180 | 177, 178,
179 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
181 | 171, 172,
180 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
182 | 165, 181 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ) |
183 | 182 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈
ℝ*) |
184 | 183 | ad4ant14 1293 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈
ℝ*) |
185 | 151 | ad4ant124 1295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈
ℝ*) |
186 | 22 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ) |
187 | 186, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ) |
188 | 187 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
189 | 188 | ad4ant124 1295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
190 | 173 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
191 | 190 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
192 | 191 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
193 | 192 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
194 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
195 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑘 ∈
𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
196 | 193, 194,
195 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
197 | 196 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
198 | | icogelb 12225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
199 | 185, 189,
197, 198 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
200 | 199 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
201 | | icoltub 39732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
202 | 185, 189,
197, 201 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
203 | 202 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
204 | 203 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
205 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑) |
206 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
207 | 205, 206 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
208 | 207 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
209 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾) |
210 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) |
211 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝐾)) |
212 | 211 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝐾 → (((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)) |
213 | 212 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) ≤ 𝑌) |
214 | 213 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝐾)) |
215 | 211 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘)) |
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘)) |
217 | 214, 216 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘)) |
218 | 217 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘)) |
219 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 = 𝑌 → ((𝑐‘ℎ) ≤ 𝑦 ↔ (𝑐‘ℎ) ≤ 𝑌)) |
220 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌) |
221 | 219, 220 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = 𝑌 → if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦) = if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) |
222 | 221 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 = 𝑌 → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) |
223 | 222 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = 𝑌 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) |
224 | 223 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))) |
225 | 224 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑦 = 𝑌) → (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))) |
226 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℝ
↑𝑚 𝑋) ∈ V |
227 | 226 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 ∈ (ℝ
↑𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V) |
229 | 80, 225, 37, 228 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))) |
230 | 229 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))) |
231 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = (𝐷‘𝑗) → (𝑐‘ℎ) = ((𝐷‘𝑗)‘ℎ)) |
232 | 231 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = (𝐷‘𝑗) → ((𝑐‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘ℎ) ≤ 𝑌)) |
233 | 232, 231 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = (𝐷‘𝑗) → if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) |
234 | 231, 233 | ifeq12d 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = (𝐷‘𝑗) → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) |
235 | 234 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = (𝐷‘𝑗) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))) |
236 | 235 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷‘𝑗)) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))) |
237 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑋 ∈ Fin → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V) |
238 | 13, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V) |
239 | 238 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V) |
240 | 230, 236,
20, 239 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))) |
241 | 240 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘)) |
242 | 241 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘)) |
243 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝜑) |
244 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
245 | 243, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝐾 ∈ 𝑋) |
246 | 244, 245 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋) |
247 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))) |
248 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ = 𝑘 → (ℎ ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾}))) |
249 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ = 𝑘 → ((𝐷‘𝑗)‘ℎ) = ((𝐷‘𝑗)‘𝑘)) |
250 | 249 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (ℎ = 𝑘 → (((𝐷‘𝑗)‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)) |
251 | 250, 249 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ = 𝑘 → if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) |
252 | 248, 249,
251 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ℎ = 𝑘 → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
253 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
254 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
255 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((𝐷‘𝑗)‘𝑘) ∈ V) |
256 | | ifexg 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐷‘𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V) |
257 | 255, 37, 256 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V) |
258 | | ifexg 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝐷‘𝑗)‘𝑘) ∈ V ∧ if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V) |
259 | 255, 257,
258 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V) |
260 | 259 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V) |
261 | 247, 253,
254, 260 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
262 | 243, 246,
261 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
263 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾}))) |
264 | 212, 211 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 𝐾 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) |
265 | 263, 211,
264 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))) |
266 | 265 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))) |
267 | 262, 266 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))) |
268 | 267 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))) |
269 | | neldifsnd 4322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾})) |
270 | 269 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) |
271 | 270 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) |
272 | 242, 268,
271 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
273 | 272 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
274 | 273 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
275 | 218, 274 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
276 | 208, 209,
210, 275 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
277 | 276 | ad5ant145 1315 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
278 | 204, 277 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
279 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -∞
∈ ℝ* |
280 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → -∞ ∈
ℝ*) |
281 | 37 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
282 | 281 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑌 ∈
ℝ*) |
283 | 282 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ∈
ℝ*) |
284 | 181 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
285 | 157 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌)) |
286 | 284, 285 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌)) |
287 | | iooltub 39735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((-∞ ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ (𝑓‘𝑘) ∈ (-∞(,)𝑌)) → (𝑓‘𝑘) < 𝑌) |
288 | 280, 283,
286, 287 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌) |
289 | 288 | 3adant1r 1319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌) |
290 | 289 | ad4ant123 1294 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < 𝑌) |
291 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) |
292 | 212 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝐾 → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)) |
293 | 292 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)) |
294 | 291, 293 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌) |
295 | 294 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = 𝑌) |
296 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌) |
297 | 295, 296 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) |
298 | 297 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) |
299 | 273 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
300 | 299 | adantlllr 39199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
301 | 300 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
302 | 298, 301 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
303 | 290, 302 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
304 | 303 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
305 | 278, 304 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
306 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
307 | 240 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))) |
308 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
309 | 260 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V) |
310 | 307, 308,
149, 309 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
311 | 310 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
312 | 311 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
313 | 312 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))) |
314 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋) |
315 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑘 = 𝐾 → 𝑘 ≠ 𝐾) |
316 | | nelsn 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ {𝐾}) |
317 | 315, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾}) |
318 | 317 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾}) |
319 | 314, 318 | eldifd 3585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾})) |
320 | 319 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘)) |
321 | 320 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘)) |
322 | 313, 321 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
323 | 306, 322 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
324 | 305, 323 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
325 | 152, 156,
184, 200, 324 | elicod 12224 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
326 | 325 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
327 | 147, 326 | ralrimi 2957 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
328 | 142, 327 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
329 | 173 | elixp 7915 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
330 | 328, 329 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
331 | 330 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
332 | 136, 139,
140, 331 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
333 | 332 | reximdva 3017 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))) |
334 | 135, 333 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
335 | | eliun 4524 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
336 | 334, 335 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
337 | 336 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
338 | | dfss3 3592 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
339 | 337, 338 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
340 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))) |
341 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑗 → (𝐷‘𝑙) = (𝐷‘𝑗)) |
342 | 341 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑗 → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗))) |
343 | 342 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗))) |
344 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
345 | | fvexd 6203 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((𝑇‘𝑌)‘(𝐷‘𝑗)) ∈ V) |
346 | 340, 343,
344, 345 | fvmptd 6288 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗) = ((𝑇‘𝑌)‘(𝐷‘𝑗))) |
347 | 346 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
348 | 347 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
349 | 348 | ixpeq2dv 7924 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))) |
350 | 349 | iuneq2i 4539 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) |
351 | 339, 350 | syl6sseqr 3652 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘))) |
352 | 13, 15, 127, 351, 12 | ovnlecvr2 40824 |
. . . . 5
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))))) |
353 | 346 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))) |
354 | 353 | mpteq2ia 4740 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))) |
355 | 354 | fveq2i 6194 |
. . . . . 6
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) |
356 | 355 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))) |
357 | 352, 356 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))) |
358 | 15 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙) ∈ (ℝ ↑𝑚
𝑋)) |
359 | | elmapi 7879 |
. . . . . . . . . 10
⊢ ((𝐶‘𝑙) ∈ (ℝ ↑𝑚
𝑋) → (𝐶‘𝑙):𝑋⟶ℝ) |
360 | 358, 359 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙):𝑋⟶ℝ) |
361 | 97, 110, 111, 360 | hoidifhspf 40832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ) |
362 | | elmapg 7870 |
. . . . . . . . . 10
⊢ ((ℝ
∈ V ∧ 𝑋 ∈
Fin) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑𝑚
𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)) |
363 | 121, 362 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑𝑚
𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)) |
364 | 363 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑𝑚
𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)) |
365 | 361, 364 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑𝑚
𝑋)) |
366 | | eqid 2622 |
. . . . . . 7
⊢ (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) |
367 | 365, 366 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))):ℕ⟶(ℝ
↑𝑚 𝑋)) |
368 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑) |
369 | | eldifi 3732 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴) |
370 | 369 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴) |
371 | 368, 370,
134 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
372 | 141 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋) |
373 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) |
374 | 373, 146 | nfan 1828 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
375 | 98 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ) |
376 | 375, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ) |
377 | 376 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈
ℝ*) |
378 | 377 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈
ℝ*) |
379 | 189 | adantl3r 786 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
380 | 150 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ) |
381 | 188 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
382 | | icossre 12254 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
383 | 380, 381,
382 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
384 | 383 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
385 | 384, 197 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ) |
386 | 385 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈
ℝ*) |
387 | 386 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈
ℝ*) |
388 | 38 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑌 ∈ ℝ) |
389 | 14 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin) |
390 | 97, 388, 389, 148, 149 | hoidifhspval3 40833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘))) |
391 | 390 | ad5ant134 1313 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘))) |
392 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌)) |
393 | 392 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌)) |
394 | 391, 393 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌)) |
395 | 394 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌)) |
396 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘)) |
397 | 396 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘)) |
398 | 199 | adantl3r 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
399 | 398 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
400 | 397, 399 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘)) |
401 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌) |
402 | 401 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌) |
403 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) |
404 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝑘)) |
405 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 = 𝐾 → (𝑓‘𝑘) = (𝑓‘𝐾)) |
406 | 405 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 𝐾 → (𝑌 ≤ (𝑓‘𝑘) ↔ 𝑌 ≤ (𝑓‘𝐾))) |
407 | 406 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾))) |
408 | 407 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾))) |
409 | 404, 408 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾)) |
410 | 409 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾)) |
411 | 405 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 𝐾 → (𝑓‘𝐾) = (𝑓‘𝑘)) |
412 | 411 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) = (𝑓‘𝑘)) |
413 | 371 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
414 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
415 | 414 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
416 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
417 | 254 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑘 ∈ 𝑋) |
418 | 415, 416,
417, 385 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) ∈ ℝ) |
419 | 418 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ)) |
420 | 419 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ)) |
421 | 420 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ)) |
422 | 413, 421 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ) |
423 | 422 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ) |
424 | 412, 423 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) ∈ ℝ) |
425 | 424 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) ∈ ℝ) |
426 | 403, 368,
37 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑌 ∈ ℝ) |
427 | 425, 426 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ((𝑓‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓‘𝐾))) |
428 | 410, 427 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) < 𝑌) |
429 | 372, 371 | r19.29a 3078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 Fn 𝑋) |
430 | 429 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → 𝑓 Fn 𝑋) |
431 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈
ℝ*) |
432 | 281 | ad4antr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈
ℝ*) |
433 | 422 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ) |
434 | 433 | mnfltd 11958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓‘𝑘)) |
435 | 405 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) = (𝑓‘𝐾)) |
436 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) < 𝑌) |
437 | 435, 436 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌) |
438 | 437 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌) |
439 | 431, 432,
433, 434, 438 | eliood 39720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌)) |
440 | 157 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
441 | 440 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
442 | 439, 441 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
443 | 422 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ) |
444 | 161 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (¬
𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
445 | 444 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
446 | 443, 445 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
447 | 442, 446 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
448 | 447 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
449 | 430, 448 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))) |
450 | 403, 428,
449 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))) |
451 | 450, 174 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)) |
452 | 168 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → X𝑘 ∈
𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌)) |
453 | 452 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌)) |
454 | 453 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌)) |
455 | 451, 454 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
456 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
457 | 456 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
458 | 457 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
459 | 458 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) |
460 | 455, 459 | condan 835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘)) |
461 | 460 | ad5ant145 1315 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘)) |
462 | 461 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → 𝑌 ≤ (𝑓‘𝑘)) |
463 | 402, 462 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘)) |
464 | 400, 463 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘)) |
465 | 395, 464 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘)) |
466 | 390 | ad5ant124 1311 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘))) |
467 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘)) |
468 | 467 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘)) |
469 | 466, 468 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
470 | 199 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘)) |
471 | 469, 470 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘)) |
472 | 471 | adantl4r 787 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘)) |
473 | 465, 472 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘)) |
474 | 202 | adantl3r 786 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘)) |
475 | 378, 379,
387, 473, 474 | elicod 12224 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
476 | 475 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
477 | 374, 476 | ralrimi 2957 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
478 | 372, 477 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
479 | 173 | elixp 7915 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
480 | 478, 479 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
481 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))) |
482 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗)) |
483 | 482 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑗 → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗))) |
484 | 483 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗))) |
485 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → ((𝑆‘𝑌)‘(𝐶‘𝑗)) ∈ V) |
486 | 481, 484,
344, 485 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗) = ((𝑆‘𝑌)‘(𝐶‘𝑗))) |
487 | 486 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘) = (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)) |
488 | 487 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
489 | 488 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → X𝑘 ∈
𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
490 | 489 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
491 | 490 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
492 | 480, 491 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
493 | 492 | ex 450 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
494 | 493 | reximdva 3017 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
495 | 371, 494 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
496 | | eliun 4524 |
. . . . . . . . 9
⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
497 | 495, 496 | sylibr 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
498 | 497 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
499 | | dfss3 3592 |
. . . . . . 7
⊢ ((𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
500 | 498, 499 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
501 | 13, 367, 19, 500, 12 | ovnlecvr2 40824 |
. . . . 5
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
502 | 486 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))) |
503 | 502 | mpteq2ia 4740 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))) |
504 | 503 | fveq2i 6194 |
. . . . . 6
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) |
505 | 504 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) |
506 | 501, 505 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) |
507 | 1, 2, 96, 109, 357, 506 | leadd12dd 39532 |
. . 3
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))) |
508 | 14, 106, 38, 18, 22, 12, 36, 97 | hspmbllem1 40840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) |
509 | 508 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) |
510 | 509 | fveq2d 6195 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))) |
511 | 8, 10, 41, 105 | sge0xadd 40652 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))) |
512 | 96, 109 | rexaddd 12065 |
. . . 4
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))) |
513 | 510, 511,
512 | 3eqtrrd 2661 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
514 | 507, 513 | breqtrd 4679 |
. 2
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
515 | 3, 35, 7, 514, 34 | letrd 10194 |
1
⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) |