Step | Hyp | Ref
| Expression |
1 | | reex 10027 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | | mapdm0 7872 |
. . . . . . 7
⊢ (ℝ
∈ V → (ℝ ↑𝑚 ∅) =
{∅}) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ (ℝ
↑𝑚 ∅) = {∅} |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 ∅) = {∅}) |
5 | | oveq2 6658 |
. . . . 5
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 𝑋) = (ℝ ↑𝑚
∅)) |
6 | | ixpeq1 7919 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) = X𝑖 ∈ ∅ (([,) ∘
(𝐼‘𝑗))‘𝑖)) |
7 | 6 | iuneq2d 4547 |
. . . . . 6
⊢ (𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) = ∪ 𝑗 ∈ ℕ X𝑖 ∈
∅ (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
8 | | ixp0x 7936 |
. . . . . . . . . 10
⊢ X𝑖 ∈
∅ (([,) ∘ (𝐼‘𝑗))‘𝑖) = {∅} |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → X𝑖 ∈
∅ (([,) ∘ (𝐼‘𝑗))‘𝑖) = {∅}) |
10 | 9 | iuneq2i 4539 |
. . . . . . . 8
⊢ ∪ 𝑗 ∈ ℕ X𝑖 ∈ ∅ (([,) ∘
(𝐼‘𝑗))‘𝑖) = ∪ 𝑗 ∈ ℕ
{∅} |
11 | | 1nn 11031 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
12 | 11 | ne0ii 3923 |
. . . . . . . . 9
⊢ ℕ
≠ ∅ |
13 | | iunconst 4529 |
. . . . . . . . 9
⊢ (ℕ
≠ ∅ → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ 𝑗 ∈ ℕ {∅} =
{∅} |
15 | 10, 14 | eqtri 2644 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ ℕ X𝑖 ∈ ∅ (([,) ∘
(𝐼‘𝑗))‘𝑖) = {∅} |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X𝑖 ∈ ∅ (([,) ∘
(𝐼‘𝑗))‘𝑖) = {∅}) |
17 | 7, 16 | eqtrd 2656 |
. . . . 5
⊢ (𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) = {∅}) |
18 | 4, 5, 17 | 3eqtr4d 2666 |
. . . 4
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 𝑋) = ∪
𝑗 ∈ ℕ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
19 | | eqimss 3657 |
. . . 4
⊢ ((ℝ
↑𝑚 𝑋) = ∪
𝑗 ∈ ℕ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) → (ℝ ↑𝑚
𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
21 | 20 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
22 | | simpll 790 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝜑) |
23 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑓 ∈ (ℝ
↑𝑚 𝑋)) |
24 | | simplr 792 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → ¬ 𝑋 = ∅) |
25 | | rncoss 5386 |
. . . . . . . . . . 11
⊢ ran (abs
∘ 𝑓) ⊆ ran
abs |
26 | | absf 14077 |
. . . . . . . . . . . 12
⊢
abs:ℂ⟶ℝ |
27 | | frn 6053 |
. . . . . . . . . . . 12
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran abs
⊆ ℝ |
29 | 25, 28 | sstri 3612 |
. . . . . . . . . 10
⊢ ran (abs
∘ 𝑓) ⊆
ℝ |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → ran (abs
∘ 𝑓) ⊆
ℝ) |
31 | | ltso 10118 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → < Or
ℝ) |
33 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) →
abs:ℂ⟶ℝ) |
34 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → 𝑓:𝑋⟶ℝ) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑓:𝑋⟶ℝ) |
36 | | ax-resscn 9993 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → ℝ ⊆
ℂ) |
38 | 35, 37 | fssd 6057 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑓:𝑋⟶ℂ) |
39 | | fco 6058 |
. . . . . . . . . . . . 13
⊢
((abs:ℂ⟶ℝ ∧ 𝑓:𝑋⟶ℂ) → (abs ∘ 𝑓):𝑋⟶ℝ) |
40 | 33, 38, 39 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → (abs ∘
𝑓):𝑋⟶ℝ) |
41 | | hoicvr.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ Fin) |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑋 ∈ Fin) |
43 | | rnffi 39356 |
. . . . . . . . . . . 12
⊢ (((abs
∘ 𝑓):𝑋⟶ℝ ∧ 𝑋 ∈ Fin) → ran (abs
∘ 𝑓) ∈
Fin) |
44 | 40, 42, 43 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → ran (abs ∘
𝑓) ∈
Fin) |
45 | 44 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → ran (abs
∘ 𝑓) ∈
Fin) |
46 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:𝑋⟶ℝ → ran 𝑓 ⊆
ℝ) |
47 | 34, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → ran 𝑓 ⊆ ℝ) |
48 | 26 | fdmi 6052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom abs =
ℂ |
49 | 48 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ =
dom abs |
50 | 36, 49 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℝ
⊆ dom abs |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → ℝ ⊆ dom
abs) |
52 | 47, 51 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → ran 𝑓 ⊆ dom abs) |
53 | | dmcosseq 5387 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑓 ⊆ dom abs →
dom (abs ∘ 𝑓) = dom
𝑓) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → dom (abs ∘ 𝑓) = dom 𝑓) |
55 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:𝑋⟶ℝ → dom 𝑓 = 𝑋) |
56 | 34, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → dom 𝑓 = 𝑋) |
57 | 54, 56 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → dom (abs ∘ 𝑓) = 𝑋) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → dom (abs ∘ 𝑓) = 𝑋) |
59 | | neqne 2802 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
61 | 58, 60 | eqnetrd 2861 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → dom (abs ∘ 𝑓) ≠ ∅) |
62 | 61 | neneqd 2799 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → ¬ dom (abs ∘
𝑓) =
∅) |
63 | | dm0rn0 5342 |
. . . . . . . . . . . . 13
⊢ (dom (abs
∘ 𝑓) = ∅ ↔
ran (abs ∘ 𝑓) =
∅) |
64 | 62, 63 | sylnib 318 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → ¬ ran (abs ∘
𝑓) =
∅) |
65 | 64 | neqned 2801 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ ¬ 𝑋 = ∅) → ran (abs ∘ 𝑓) ≠ ∅) |
66 | 65 | adantll 750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → ran (abs
∘ 𝑓) ≠
∅) |
67 | | fisupcl 8375 |
. . . . . . . . . 10
⊢ (( <
Or ℝ ∧ (ran (abs ∘ 𝑓) ∈ Fin ∧ ran (abs ∘ 𝑓) ≠ ∅ ∧ ran (abs
∘ 𝑓) ⊆
ℝ)) → sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ran (abs ∘
𝑓)) |
68 | 32, 45, 66, 30, 67 | syl13anc 1328 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → sup(ran (abs
∘ 𝑓), ℝ, < )
∈ ran (abs ∘ 𝑓)) |
69 | 30, 68 | sseldd 3604 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → sup(ran (abs
∘ 𝑓), ℝ, < )
∈ ℝ) |
70 | | arch 11289 |
. . . . . . . 8
⊢ (sup(ran
(abs ∘ 𝑓), ℝ,
< ) ∈ ℝ → ∃𝑗 ∈ ℕ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → ∃𝑗 ∈ ℕ sup(ran (abs
∘ 𝑓), ℝ, < )
< 𝑗) |
72 | 35 | ffnd 6046 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑓 Fn 𝑋) |
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) ∧ sup(ran (abs
∘ 𝑓), ℝ, < )
< 𝑗) → 𝑓 Fn 𝑋) |
74 | 73 | adantlr 751 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → 𝑓 Fn 𝑋) |
75 | | simplll 798 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋))) |
76 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
77 | 76 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ ℕ) |
78 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) |
79 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
80 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) → 𝑗 ∈
ℕ) |
81 | | zssre 11384 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℤ
⊆ ℝ |
82 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℝ
⊆ ℝ* |
83 | 81, 82 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℤ
⊆ ℝ* |
84 | | nnnegz 11380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℤ) |
85 | 83, 84 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℝ*) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → -𝑗 ∈ ℝ*) |
87 | 80, 86 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -𝑗 ∈ ℝ*) |
88 | 76 | nnxrd 39201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ*) |
89 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ ℝ*) |
90 | 80, 89 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ ℝ*) |
91 | 34 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑗 ∈ ℕ ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → 𝑓:𝑋⟶ℝ) |
92 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑗 ∈ ℕ ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → ℝ ⊆
ℝ*) |
93 | 91, 92 | fssd 6057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑗 ∈ ℕ ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → 𝑓:𝑋⟶ℝ*) |
94 | 93 | 3adant1l 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) → 𝑓:𝑋⟶ℝ*) |
95 | 94 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈
ℝ*) |
96 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
97 | 96 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ ℝ) |
98 | 97 | 3ad2antl2 1224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → 𝑗 ∈ ℝ) |
99 | 98 | renegcld 10457 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -𝑗 ∈ ℝ) |
100 | 35 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
101 | 100 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
102 | 101 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ∈ ℝ) |
103 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝜑) |
104 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (ℝ ↑𝑚
𝑋)) |
105 | | n0i 3920 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ 𝑋 → ¬ 𝑋 = ∅) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑋 = ∅) |
107 | 103, 104,
106, 69 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → sup(ran (abs ∘ 𝑓), ℝ, < ) ∈
ℝ) |
108 | 107 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → sup(ran (abs ∘ 𝑓), ℝ, < ) ∈
ℝ) |
109 | 34 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
110 | 36, 109 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℂ) |
111 | 110 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ℝ) |
112 | 111 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ℝ) |
113 | 112 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ℝ) |
114 | 109 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ∈ ℝ) |
115 | 114 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ≤ (abs‘-(𝑓‘𝑖))) |
116 | 110 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (abs‘-(𝑓‘𝑖)) = (abs‘(𝑓‘𝑖))) |
117 | 115, 116 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ≤ (abs‘(𝑓‘𝑖))) |
118 | 117 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ≤ (abs‘(𝑓‘𝑖))) |
119 | 118 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ≤ (abs‘(𝑓‘𝑖))) |
120 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → ran (abs ∘ 𝑓) ⊆ ℝ) |
121 | 106, 66 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ran (abs ∘ 𝑓) ≠ ∅) |
122 | 121 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → ran (abs ∘ 𝑓) ≠ ∅) |
123 | | fimaxre2 10969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ran
(abs ∘ 𝑓) ⊆
ℝ ∧ ran (abs ∘ 𝑓) ∈ Fin) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (abs ∘ 𝑓)𝑧 ≤ 𝑦) |
124 | 29, 44, 123 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (abs ∘ 𝑓)𝑧 ≤ 𝑦) |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (abs ∘ 𝑓)𝑧 ≤ 𝑦) |
126 | 125 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (abs ∘ 𝑓)𝑧 ≤ 𝑦) |
127 | | elmapfun 7881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → Fun 𝑓) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → Fun 𝑓) |
129 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
130 | 56 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → 𝑋 = dom 𝑓) |
131 | 130 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑋 = dom 𝑓) |
132 | 129, 131 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ dom 𝑓) |
133 | | fvco 6274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
𝑓 ∧ 𝑖 ∈ dom 𝑓) → ((abs ∘ 𝑓)‘𝑖) = (abs‘(𝑓‘𝑖))) |
134 | 128, 132,
133 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → ((abs ∘ 𝑓)‘𝑖) = (abs‘(𝑓‘𝑖))) |
135 | 134 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) = ((abs ∘ 𝑓)‘𝑖)) |
136 | | absfun 39566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ Fun
abs |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → Fun abs) |
138 | | funco 5928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun abs
∧ Fun 𝑓) → Fun
(abs ∘ 𝑓)) |
139 | 137, 127,
138 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝑋) → Fun (abs ∘ 𝑓)) |
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → Fun (abs ∘ 𝑓)) |
141 | 110, 49 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ dom abs) |
142 | | dmfco 6272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
𝑓 ∧ 𝑖 ∈ dom 𝑓) → (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (𝑓‘𝑖) ∈ dom abs)) |
143 | 128, 132,
142 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (𝑓‘𝑖) ∈ dom abs)) |
144 | 141, 143 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ dom (abs ∘ 𝑓)) |
145 | | fvelrn 6352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
(abs ∘ 𝑓) ∧ 𝑖 ∈ dom (abs ∘ 𝑓)) → ((abs ∘ 𝑓)‘𝑖) ∈ ran (abs ∘ 𝑓)) |
146 | 140, 144,
145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → ((abs ∘ 𝑓)‘𝑖) ∈ ran (abs ∘ 𝑓)) |
147 | 135, 146 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ran (abs ∘ 𝑓)) |
148 | 147 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ran (abs ∘ 𝑓)) |
149 | 148 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ∈ ran (abs ∘ 𝑓)) |
150 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ran
(abs ∘ 𝑓) ⊆
ℝ ∧ ran (abs ∘ 𝑓) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (abs ∘ 𝑓)𝑧 ≤ 𝑦) ∧ (abs‘(𝑓‘𝑖)) ∈ ran (abs ∘ 𝑓)) → (abs‘(𝑓‘𝑖)) ≤ sup(ran (abs ∘ 𝑓), ℝ, <
)) |
151 | 120, 122,
126, 149, 150 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (abs‘(𝑓‘𝑖)) ≤ sup(ran (abs ∘ 𝑓), ℝ, <
)) |
152 | 102, 113,
108, 119, 151 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) ≤ sup(ran (abs ∘ 𝑓), ℝ, <
)) |
153 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) |
154 | 102, 108,
98, 152, 153 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -(𝑓‘𝑖) < 𝑗) |
155 | 102, 98 | ltnegd 10605 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (-(𝑓‘𝑖) < 𝑗 ↔ -𝑗 < --(𝑓‘𝑖))) |
156 | 154, 155 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -𝑗 < --(𝑓‘𝑖)) |
157 | 36, 101 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℂ) |
158 | 157 | negnegd 10383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → --(𝑓‘𝑖) = (𝑓‘𝑖)) |
159 | 156, 158 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -𝑗 < (𝑓‘𝑖)) |
160 | 99, 101, 159 | ltled 10185 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → -𝑗 ≤ (𝑓‘𝑖)) |
161 | 101 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ≤ (abs‘(𝑓‘𝑖))) |
162 | 101, 113,
108, 161, 151 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ≤ sup(ran (abs ∘ 𝑓), ℝ, <
)) |
163 | 101, 108,
98, 162, 153 | lelttrd 10195 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < 𝑗) |
164 | 87, 90, 95, 160, 163 | elicod 12224 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-𝑗[,)𝑗)) |
165 | 75, 77, 78, 79, 164 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-𝑗[,)𝑗)) |
166 | 165 | adantlllr 39199 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-𝑗[,)𝑗)) |
167 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
168 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∈ Fin → (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) |
169 | 41, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) |
171 | | hoicvr.2 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
172 | 171 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℕ ∧ (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) → (𝐼‘𝑗) = (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
173 | 167, 170,
172 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
174 | 173 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑗)‘𝑖) = ((𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑖)) |
175 | 174 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → ((𝐼‘𝑗)‘𝑖) = ((𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑖)) |
176 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝑋 → (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
177 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈-𝑗, 𝑗〉 = 〈-𝑗, 𝑗〉 |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑋 ∧ 𝑥 = 𝑖) → 〈-𝑗, 𝑗〉 = 〈-𝑗, 𝑗〉) |
179 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ 𝑋) |
180 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈-𝑗, 𝑗〉 ∈ V |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝑋 → 〈-𝑗, 𝑗〉 ∈ V) |
182 | 176, 178,
179, 181 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝑋 → ((𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑖) = 〈-𝑗, 𝑗〉) |
183 | 182 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑖) = 〈-𝑗, 𝑗〉) |
184 | 175, 183 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → ((𝐼‘𝑗)‘𝑖) = 〈-𝑗, 𝑗〉) |
185 | 184 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (1st ‘((𝐼‘𝑗)‘𝑖)) = (1st ‘〈-𝑗, 𝑗〉)) |
186 | | negex 10279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -𝑗 ∈ V |
187 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑗 ∈ V |
188 | 186, 187 | op1st 7176 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1st ‘〈-𝑗, 𝑗〉) = -𝑗 |
189 | 188 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (1st ‘〈-𝑗, 𝑗〉) = -𝑗) |
190 | 185, 189 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (1st ‘((𝐼‘𝑗)‘𝑖)) = -𝑗) |
191 | 184 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (2nd ‘((𝐼‘𝑗)‘𝑖)) = (2nd ‘〈-𝑗, 𝑗〉)) |
192 | 186, 187 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈-𝑗, 𝑗〉) = 𝑗 |
193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (2nd ‘〈-𝑗, 𝑗〉) = 𝑗) |
194 | 191, 193 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (2nd ‘((𝐼‘𝑗)‘𝑖)) = 𝑗) |
195 | 190, 194 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖))) = (-𝑗[,)𝑗)) |
196 | 195 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (-𝑗[,)𝑗) = ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖)))) |
197 | 196 | 3adant1r 1319 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋) → (-𝑗[,)𝑗) = ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖)))) |
198 | 197 | ad5ant135 1314 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (-𝑗[,)𝑗) = ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖)))) |
199 | 166, 198 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖)))) |
200 | 81, 84 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℝ) |
201 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
202 | 200, 96, 201 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
203 | 202 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ 𝑋) → 〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
204 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
205 | 203, 204 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ)) |
206 | 173 | feq1d 6030 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑗):𝑋⟶(ℝ × ℝ) ↔
(𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
207 | 205, 206 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
208 | 207 | ad4ant14 1293 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
209 | 208 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
210 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
211 | 209, 210 | fvovco 39381 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (([,) ∘ (𝐼‘𝑗))‘𝑖) = ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖)))) |
212 | 211 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → ((1st ‘((𝐼‘𝑗)‘𝑖))[,)(2nd ‘((𝐼‘𝑗)‘𝑖))) = (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
213 | 199, 212 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
214 | 213 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
215 | 74, 214 | jca 554 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ (([,) ∘ (𝐼‘𝑗))‘𝑖))) |
216 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
217 | 216 | elixp 7915 |
. . . . . . . . . 10
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ (([,) ∘ (𝐼‘𝑗))‘𝑖))) |
218 | 215, 217 | sylibr 224 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑓 ∈ (ℝ
↑𝑚 𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) ∧ sup(ran (abs ∘
𝑓), ℝ, < ) <
𝑗) → 𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
219 | 218 | ex 450 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ ℕ) → (sup(ran
(abs ∘ 𝑓), ℝ,
< ) < 𝑗 → 𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖))) |
220 | 219 | reximdva 3017 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → (∃𝑗 ∈ ℕ sup(ran (abs
∘ 𝑓), ℝ, < )
< 𝑗 → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖))) |
221 | 71, 220 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) ∧ ¬ 𝑋 = ∅) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
222 | 22, 23, 24, 221 | syl21anc 1325 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
223 | | eliun 4524 |
. . . . 5
⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
224 | 222, 223 | sylibr 224 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋)) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
225 | 224 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∀𝑓 ∈ (ℝ
↑𝑚 𝑋)𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
226 | | dfss3 3592 |
. . 3
⊢ ((ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖) ↔ ∀𝑓 ∈ (ℝ ↑𝑚
𝑋)𝑓 ∈ ∪
𝑗 ∈ ℕ X𝑖 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
227 | 225, 226 | sylibr 224 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |
228 | 21, 227 | pm2.61dan 832 |
1
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) |