Step | Hyp | Ref
| Expression |
1 | | ioof 13179 |
. . . . . 6
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | | ffn 6600 |
. . . . . 6
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
3 | | ovelrn 7448 |
. . . . . 6
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑜 =
(𝑎(,)𝑏))) |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
⊢ (𝑜 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)) |
5 | | elxr 12852 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℝ*
↔ (𝑏 ∈ ℝ
∨ 𝑏 = +∞ ∨
𝑏 =
-∞)) |
6 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ 𝑏 ∈
ℝ) |
7 | | elioore 13109 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ) |
8 | 6, 7 | anim12ci 614 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ)) |
9 | | relowlssretop.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐼 = ([,) “ (ℝ ×
ℝ)) |
10 | 9 | icoreelrn 35532 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼) |
12 | 7 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
13 | 7 | leidd 11541 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ≤ 𝑥) |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ≤ 𝑥) |
15 | 6 | rexrd 11025 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ 𝑏 ∈
ℝ*) |
16 | | elioo1 13119 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
17 | 15, 16 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
18 | 17 | biimpa 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) |
19 | 18 | simp3d 1143 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 < 𝑏) |
20 | | rexr 11021 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
21 | 20 | 3anim1i 1151 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏)) |
22 | | rexr 11021 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℝ*) |
23 | | elico1 13122 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏))) |
24 | 20, 22, 23 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏))) |
25 | 24 | biimprd 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏))) |
26 | 8, 21, 25 | syl2im 40 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏))) |
27 | | icoreval 35524 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
28 | 8, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
29 | 28 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ (𝑥[,)𝑏) ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
30 | 26, 29 | sylibd 238 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
31 | 12, 14, 19, 30 | mp3and 1463 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
32 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) |
33 | | nfrab1 3317 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧{𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} |
34 | | nfcv 2907 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧(𝑎(,)𝑏) |
35 | | iooval 13103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎(,)𝑏) = {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)}) |
36 | 35 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)})) |
37 | 36 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ↔ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}))) |
38 | 37 | pm5.32i 575 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ (𝑥 ∈ {𝑥 ∈ ℝ*
∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}))) |
39 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ↔ (𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
40 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) |
41 | 39, 40 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ↔ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) |
42 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 ∈ ℝ) |
43 | 42 | rexrd 11025 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 ∈ ℝ*) |
44 | 43 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ ℝ*) |
45 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) → 𝑥 ∈ ℝ*) |
46 | 45, 43 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) → (𝑥 ∈ ℝ* ∧ 𝑧 ∈
ℝ*)) |
47 | 46 | anim2i 617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*))) |
48 | | 3anass 1094 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ↔ (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*))) |
49 | 47, 48 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 ∈ ℝ* ∧ 𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*)) |
50 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) → 𝑎 < 𝑥) |
51 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑥 ≤ 𝑧) |
52 | 50, 51 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) → (𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧)) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧)) |
54 | | xrltletr 12891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → ((𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧) → 𝑎 < 𝑧)) |
55 | 49, 53, 54 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑎 < 𝑧) |
56 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 < 𝑏) |
57 | 56 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 < 𝑏) |
58 | 55, 57 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)) |
59 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ* ∧ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏))) |
60 | 44, 58, 59 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
61 | 60 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
62 | | iooval 13103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
64 | 61, 63 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ (𝑎(,)𝑏)) |
65 | 41, 64 | sylan2b 594 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏)) |
66 | 38, 65 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏)) |
67 | 66 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → 𝑧 ∈ (𝑎(,)𝑏))) |
68 | 32, 33, 34, 67 | ssrd 3926 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)) |
69 | 22, 68 | sylanl2 678 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)) |
70 | | eleq2 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
71 | | sseq1 3946 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))) |
72 | 70, 71 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)))) |
73 | 72 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ (({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
74 | 11, 31, 69, 73 | syl12anc 834 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
75 | 74 | ancom1s 650 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
76 | 75 | expl 458 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℝ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
77 | 7 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
78 | | peano2re 11148 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
79 | 9 | icoreelrn 35532 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
{𝑧 ∈ ℝ ∣
(𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼) |
80 | 77, 78, 79 | syl2anc2 585 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼) |
81 | | elioore 13109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝑎(,)+∞) → 𝑥 ∈ ℝ) |
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈
ℝ) |
83 | 82 | leidd 11541 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ≤ 𝑥) |
84 | 82 | ltp1d 11905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 < (𝑥 + 1)) |
85 | 82, 83, 84 | jca32 516 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ ℝ ∧ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
86 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → (𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑥)) |
87 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → (𝑧 < (𝑥 + 1) ↔ 𝑥 < (𝑥 + 1))) |
88 | 86, 87 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → ((𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)) ↔ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
89 | 88 | elrab 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ↔ (𝑥 ∈ ℝ ∧ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
90 | 85, 89 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))}) |
91 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧(𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) |
92 | | nfrab1 3317 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧{𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} |
93 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧(𝑎(,)+∞) |
94 | | rabid 3310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ↔ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) |
95 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ) |
96 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 ∈ ℝ*) |
97 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ) |
98 | 97 | rexrd 11025 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ*) |
99 | 95 | rexrd 11025 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ*) |
100 | | elioopnf 13175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℝ*
→ (𝑥 ∈ (𝑎(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑎 < 𝑥))) |
101 | 100 | simplbda 500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑎 < 𝑥) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑥) |
103 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))) → 𝑥 ≤ 𝑧) |
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ≤ 𝑧) |
105 | 96, 98, 99, 102, 104 | xrltletrd 12895 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑧) |
106 | | elioopnf 13175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℝ*
→ (𝑧 ∈ (𝑎(,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝑎 < 𝑧))) |
107 | 106 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ ℝ*
→ ((𝑧 ∈ ℝ
∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
108 | 107 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
110 | 95, 105, 109 | mp2and 696 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ (𝑎(,)+∞)) |
111 | 110 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))) → 𝑧 ∈ (𝑎(,)+∞))) |
112 | 94, 111 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → 𝑧 ∈ (𝑎(,)+∞))) |
113 | 91, 92, 93, 112 | ssrd 3926 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)) |
114 | 90, 113 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))) |
115 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = +∞ → (𝑎(,)𝑏) = (𝑎(,)+∞)) |
116 | 115 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = +∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)+∞))) |
117 | 116 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) ↔ (𝑎 ∈ ℝ* ∧ 𝑥 ∈ (𝑎(,)+∞)))) |
118 | 115 | sseq2d 3953 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = +∞ → ({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))) |
119 | 118 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = +∞ → ((𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)))) |
120 | 117, 119 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = +∞ → (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) ↔ ((𝑎 ∈ ℝ* ∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))))) |
121 | 114, 120 | mpbiri 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))) |
122 | 121 | impl 456 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
123 | 122 | ancom1s 650 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
124 | | eleq2 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))})) |
125 | | sseq1 3946 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
126 | 124, 125 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))) |
127 | 126 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ (({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
128 | 80, 123, 127 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
129 | 128 | ancom1s 650 |
. . . . . . . . . . . 12
⊢ (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
130 | 129 | expl 458 |
. . . . . . . . . . 11
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
131 | 7 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
132 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = -∞ → (𝑎(,)𝑏) = (𝑎(,)-∞)) |
133 | 132 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = -∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞))) |
134 | 133 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) →
(𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞))) |
135 | 134 | pm5.32i 575 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)-∞))) |
136 | | nltmnf 12865 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 <
-∞) |
137 | 136 | intnand 489 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ¬ (𝑎 < 𝑥 ∧ 𝑥 < -∞)) |
138 | | eliooord 13138 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)-∞) → (𝑎 < 𝑥 ∧ 𝑥 < -∞)) |
139 | 137, 138 | nsyl 140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 ∈
(𝑎(,)-∞)) |
140 | 139 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑥 ∈ (𝑎(,)-∞) → ((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))))) |
141 | 140 | impd 411 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((𝑥 ∈ (𝑎(,)-∞) ∧ (𝑎 ∈ ℝ*
∧ 𝑏 = -∞)) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
142 | 141 | ancomsd 466 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ (((𝑎 ∈
ℝ* ∧ 𝑏
= -∞) ∧ 𝑥 ∈
(𝑎(,)-∞)) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
143 | 135, 142 | syl5bi 241 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (((𝑎 ∈
ℝ* ∧ 𝑏
= -∞) ∧ 𝑥 ∈
(𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
144 | 20, 143 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
145 | 131, 144 | mpcom 38 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
146 | 145 | ancom1s 650 |
. . . . . . . . . . . 12
⊢ (((𝑏 = -∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
147 | 146 | expl 458 |
. . . . . . . . . . 11
⊢ (𝑏 = -∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
148 | 76, 130, 147 | 3jaoi 1426 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞) → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
149 | 5, 148 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ*
→ ((𝑎 ∈
ℝ* ∧ 𝑥
∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
150 | 149 | expdimp 453 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℝ*
∧ 𝑎 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
151 | 150 | ancoms 459 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
152 | | eleq2 2827 |
. . . . . . . 8
⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏))) |
153 | | sseq2 3947 |
. . . . . . . . . 10
⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 ⊆ 𝑜 ↔ 𝑖 ⊆ (𝑎(,)𝑏))) |
154 | 153 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜) ↔ (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
155 | 154 | rexbidv 3226 |
. . . . . . . 8
⊢ (𝑜 = (𝑎(,)𝑏) → (∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜) ↔ ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
156 | 152, 155 | imbi12d 345 |
. . . . . . 7
⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) ↔ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))))) |
157 | 151, 156 | syl5ibrcom 246 |
. . . . . 6
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)))) |
158 | 157 | rexlimivv 3221 |
. . . . 5
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
159 | 4, 158 | sylbi 216 |
. . . 4
⊢ (𝑜 ∈ ran (,) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
160 | 159 | rgen 3074 |
. . 3
⊢
∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) |
161 | 160 | rgenw 3076 |
. 2
⊢
∀𝑥 ∈
ℝ ∀𝑜 ∈
ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) |
162 | | iooex 13102 |
. . . . 5
⊢ (,)
∈ V |
163 | 162 | rnex 7759 |
. . . 4
⊢ ran (,)
∈ V |
164 | | unirnioo 13181 |
. . . . 5
⊢ ℝ =
∪ ran (,) |
165 | 9 | icoreunrn 35530 |
. . . . 5
⊢ ℝ =
∪ 𝐼 |
166 | 164, 165 | eqtr3i 2768 |
. . . 4
⊢ ∪ ran (,) = ∪ 𝐼 |
167 | | tgss2 22137 |
. . . 4
⊢ ((ran (,)
∈ V ∧ ∪ ran (,) = ∪ 𝐼)
→ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)))) |
168 | 163, 166,
167 | mp2an 689 |
. . 3
⊢
((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
169 | 164 | raleqi 3346 |
. . 3
⊢
(∀𝑥 ∈
ℝ ∀𝑜 ∈
ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
170 | 168, 169 | bitr4i 277 |
. 2
⊢
((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ℝ ∀𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
171 | 161, 170 | mpbir 230 |
1
⊢
(topGen‘ran (,)) ⊆ (topGen‘𝐼) |