Proof of Theorem iunhoiioolem
| Step | Hyp | Ref
| Expression |
| 1 | | iunhoiioolem.K |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
| 2 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) = (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
| 3 | | iunhoiioolem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 4 | | ixpf 8960 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) → 𝐹:𝑋⟶∪
𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶∪
𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 6 | | ioossre 13448 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 7 | 6 | rgenw 3065 |
. . . . . . . . . . . 12
⊢
∀𝑘 ∈
𝑋 (𝐴(,)𝐵) ⊆ ℝ |
| 8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
| 9 | | iunss 5045 |
. . . . . . . . . . 11
⊢ (∪ 𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ ↔ ∀𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
| 10 | 8, 9 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ ℝ) |
| 11 | 5, 10 | fssd 6753 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
| 12 | 11 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ℝ) |
| 13 | | iunhoiioolem.a |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 14 | 12, 13 | resubcld 11691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ) |
| 15 | 13 | rexrd 11311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
| 16 | | iunhoiioolem.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 17 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 18 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 19 | | fvixp2 45204 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) |
| 21 | | ioogtlb 45508 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) → 𝐴 < (𝐹‘𝑘)) |
| 22 | 15, 16, 20, 21 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 < (𝐹‘𝑘)) |
| 23 | 13, 12 | posdifd 11850 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴 < (𝐹‘𝑘) ↔ 0 < ((𝐹‘𝑘) − 𝐴))) |
| 24 | 22, 23 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 0 < ((𝐹‘𝑘) − 𝐴)) |
| 25 | 14, 24 | elrpd 13074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈
ℝ+) |
| 26 | 1, 2, 25 | rnmptssd 45201 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆
ℝ+) |
| 27 | | iunhoiioolem.c |
. . . . . 6
⊢ 𝐶 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) |
| 28 | | ltso 11341 |
. . . . . . . 8
⊢ < Or
ℝ |
| 29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → < Or
ℝ) |
| 30 | | iunhoiioolem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 31 | 2 | rnmptfi 45176 |
. . . . . . . 8
⊢ (𝑋 ∈ Fin → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin) |
| 32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin) |
| 33 | | iunhoiioolem.n |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 34 | 1, 14, 2, 33 | rnmptn0 6264 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ≠ ∅) |
| 35 | 1, 2, 14 | rnmptssd 45201 |
. . . . . . 7
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ) |
| 36 | | fiinfcl 9541 |
. . . . . . 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 2845 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
| 39 | 26, 38 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 40 | | rpgtrecnn 45391 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ ∃𝑛 ∈
ℕ (1 / 𝑛) < 𝐶) |
| 41 | 39, 40 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐶) |
| 42 | 3 | elexd 3504 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
| 43 | 42 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 ∈ V) |
| 44 | 5 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 45 | 44 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 Fn 𝑋) |
| 46 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
| 47 | 1, 46 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
| 48 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(1 /
𝑛) |
| 49 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘
< |
| 50 | | nfmpt1 5250 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
| 51 | 50 | nfrn 5963 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘ran
(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) |
| 52 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘ℝ |
| 53 | 51, 52, 49 | nfinf 9522 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) |
| 54 | 27, 53 | nfcxfr 2903 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝐶 |
| 55 | 48, 49, 54 | nfbr 5190 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1 / 𝑛) < 𝐶 |
| 56 | 47, 55 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) |
| 57 | 13 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 58 | | nnrecre 12308 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 59 | 58 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
| 60 | 57, 59 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈ ℝ) |
| 61 | 60 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈
ℝ*) |
| 62 | 61 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ∈
ℝ*) |
| 63 | 16 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 64 | 63 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 65 | | ressxr 11305 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℝ*) |
| 67 | 11, 66 | fssd 6753 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑋⟶ℝ*) |
| 68 | 67 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹:𝑋⟶ℝ*) |
| 69 | 68 | ffvelcdmda 7104 |
. . . . . . . . . 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 3984 |
. . . . . . . . . . . . . 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 7466 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑋 → ((𝐹‘𝑘) − 𝐴) ∈ V) |
| 81 | 2 | elrnmpt1 5971 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐹‘𝑘) − 𝐴) ∈ V) → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
| 82 | 79, 80, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) |
| 84 | | infrefilb 12254 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
(𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ⊆ ℝ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)) ∈ Fin ∧ ((𝐹‘𝑘) − 𝐴) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴))) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ≤ ((𝐹‘𝑘) − 𝐴)) |
| 85 | 77, 78, 83, 84 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ≤ ((𝐹‘𝑘) − 𝐴)) |
| 86 | 27, 85 | eqbrtrid 5178 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐶 ≤ ((𝐹‘𝑘) − 𝐴)) |
| 87 | 86 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐶 ≤ ((𝐹‘𝑘) − 𝐴)) |
| 88 | 72, 74, 75, 76, 87 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) < ((𝐹‘𝑘) − 𝐴)) |
| 89 | 57 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 90 | 89, 72, 71 | ltaddsub2d 11864 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → ((𝐴 + (1 / 𝑛)) < (𝐹‘𝑘) ↔ (1 / 𝑛) < ((𝐹‘𝑘) − 𝐴))) |
| 91 | 88, 90 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) < (𝐹‘𝑘)) |
| 92 | 70, 71, 91 | ltled 11409 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐴 + (1 / 𝑛)) ≤ (𝐹‘𝑘)) |
| 93 | | iooltub 45523 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴(,)𝐵)) → (𝐹‘𝑘) < 𝐵) |
| 94 | 15, 16, 20, 93 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) < 𝐵) |
| 95 | 94 | ad4ant14 752 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) < 𝐵) |
| 96 | 62, 64, 69, 92, 95 | elicod 13437 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 97 | 96 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → (𝑘 ∈ 𝑋 → (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
| 98 | 56, 97 | ralrimi 3257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 99 | 43, 45, 98 | 3jca 1129 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
| 100 | | elixp2 8941 |
. . . . . 6
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ ((𝐴 + (1 / 𝑛))[,)𝐵))) |
| 101 | 99, 100 | sylibr 234 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (1 / 𝑛) < 𝐶) → 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 102 | 101 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) < 𝐶 → 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵))) |
| 103 | 102 | reximdva 3168 |
. . 3
⊢ (𝜑 → (∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐶 → ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵))) |
| 104 | 41, 103 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 105 | | eliun 4995 |
. 2
⊢ (𝐹 ∈ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ↔ ∃𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 106 | 104, 105 | sylibr 234 |
1
⊢ (𝜑 → 𝐹 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |