Proof of Theorem iunhoiioolem
Step | Hyp | Ref
| Expression |
1 | | iunhoiioolem.K |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
2 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) = (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
3 | | iunhoiioolem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
4 | | ixpf 8601 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) → 𝐹:𝑋⟶∪
𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶∪
𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
6 | | ioossre 12996 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℝ |
7 | 6 | rgenw 3073 |
. . . . . . . . . . . 12
⊢
∀𝑘 ∈
𝑋 (𝐴(,)𝐵) ⊆ ℝ |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
9 | | iunss 4954 |
. . . . . . . . . . 11
⊢ (∪ 𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ ↔ ∀𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
10 | 8, 9 | sylibr 237 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
11 | 5, 10 | fssd 6563 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
12 | 11 | ffvelrnda 6904 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ℝ) |
13 | | iunhoiioolem.a |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
14 | 12, 13 | resubcld 11260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ) |
15 | 13 | rexrd 10883 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
16 | | iunhoiioolem.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
17 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
18 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
19 | | fvixp2 42411 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) |
20 | 17, 18, 19 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) |
21 | | ioogtlb 42708 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) → 𝐴 < (𝐹‘𝑘)) |
22 | 15, 16, 20, 21 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 < (𝐹‘𝑘)) |
23 | 13, 12 | posdifd 11419 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴 < (𝐹‘𝑘) ↔ 0 < ((𝐹‘𝑘) − 𝐴))) |
24 | 22, 23 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 0 < ((𝐹‘𝑘) − 𝐴)) |
25 | 14, 24 | elrpd 12625 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈
ℝ+) |
26 | 1, 2, 25 | rnmptssd 42408 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆
ℝ+) |
27 | | iunhoiioolem.c |
. . . . . 6
⊢ 𝐶 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) |
28 | | ltso 10913 |
. . . . . . . 8
⊢ < Or
ℝ |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → < Or
ℝ) |
30 | | iunhoiioolem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
31 | 2 | rnmptfi 42380 |
. . . . . . . 8
⊢ (𝑋 ∈ Fin → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin) |
33 | | iunhoiioolem.n |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ ∅) |
34 | 1, 14, 2, 33 | rnmptn0 6107 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ≠ ∅) |
35 | 1, 2, 14 | rnmptssd 42408 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ) |
36 | | fiinfcl 9117 |
. . . . . . 7
⊢ (( <
Or ℝ ∧ (ran (𝑘
∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ≠ ∅ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ)) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
37 | 29, 32, 34, 35, 36 | syl13anc 1374 |
. . . . . 6
⊢ (𝜑 → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
38 | 27, 37 | eqeltrid 2842 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
39 | 26, 38 | sseldd 3902 |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
40 | | rpgtrecnn 42592 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ ∃𝑛 ∈
ℕ (1 / 𝑛) < 𝐶) |
41 | 39, 40 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐶) |
42 | 3 | elexd 3428 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
43 | 42 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 ∈ V) |
44 | 5 | ffnd 6546 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
45 | 44 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 Fn 𝑋) |
46 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
47 | 1, 46 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
48 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(1 /
𝑛) |
49 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑘
< |
50 | | nfmpt1 5153 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
51 | 50 | nfrn 5821 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘ran
(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
52 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘ℝ |
53 | 51, 52, 49 | nfinf 9098 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) |
54 | 27, 53 | nfcxfr 2902 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝐶 |
55 | 48, 49, 54 | nfbr 5100 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1 / 𝑛) < 𝐶 |
56 | 47, 55 | nfan 1907 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) |
57 | 13 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
58 | | nnrecre 11872 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
59 | 58 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
60 | 57, 59 | readdcld 10862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈ ℝ) |
61 | 60 | rexrd 10883 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈
ℝ*) |
62 | 61 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈
ℝ*) |
63 | 16 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
64 | 63 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
65 | | ressxr 10877 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℝ*) |
67 | 11, 66 | fssd 6563 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑋⟶ℝ*) |
68 | 67 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹:𝑋⟶ℝ*) |
69 | 68 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈
ℝ*) |
70 | 60 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈ ℝ) |
71 | 12 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ℝ) |
72 | 59 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
73 | 35, 38 | sseldd 3902 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ ℝ) |
74 | 73 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐶 ∈ ℝ) |
75 | 14 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ) |
76 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) < 𝐶) |
77 | 35 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ) |
78 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin) |
79 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋) |
80 | | ovexd 7248 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑋 → ((𝐹‘𝑘) − 𝐴) ∈ V) |
81 | 2 | elrnmpt1 5827 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐹‘𝑘) − 𝐴) ∈ V) → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
82 | 79, 80, 81 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
83 | 82 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
84 | | infrefilb 11818 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin ∧ ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ≤ ((𝐹‘𝑘) − 𝐴)) |
85 | 77, 78, 83, 84 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ≤ ((𝐹‘𝑘) − 𝐴)) |
86 | 27, 85 | eqbrtrid 5088 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐶 ≤ ((𝐹‘𝑘) − 𝐴)) |
87 | 86 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐶 ≤ ((𝐹‘𝑘) − 𝐴)) |
88 | 72, 74, 75, 76, 87 | ltletrd 10992 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) < ((𝐹‘𝑘) − 𝐴)) |
89 | 57 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
90 | 89, 72, 71 | ltaddsub2d 11433 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → ((𝐴 + (1 / 𝑛)) < (𝐹‘𝑘) ↔ (1 / 𝑛) < ((𝐹‘𝑘) − 𝐴))) |
91 | 88, 90 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) < (𝐹‘𝑘)) |
92 | 70, 71, 91 | ltled 10980 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ≤ (𝐹‘𝑘)) |
93 | | iooltub 42723 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) → (𝐹‘𝑘) < 𝐵) |
94 | 15, 16, 20, 93 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) < 𝐵) |
95 | 94 | ad4ant14 752 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) < 𝐵) |
96 | 62, 64, 69, 92, 95 | elicod 12985 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
97 | 96 | ex 416 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → (𝑘 ∈ 𝑋 → (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
98 | 56, 97 | ralrimi 3137 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
99 | 43, 45, 98 | 3jca 1130 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
100 | | elixp2 8582 |
. . . . . 6
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
101 | 99, 100 | sylibr 237 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
102 | 101 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < 𝐶 → 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵))) |
103 | 102 | reximdva 3193 |
. . 3
⊢ (𝜑 → (∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐶 → ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵))) |
104 | 41, 103 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
105 | | eliun 4908 |
. 2
⊢ (𝐹 ∈ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ↔ ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
106 | 104, 105 | sylibr 237 |
1
⊢ (𝜑 → 𝐹 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |