Step | Hyp | Ref
| Expression |
1 | | ioof 12142 |
. . . . . 6
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | | ffn 5958 |
. . . . . 6
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
3 | | ovelrn 6708 |
. . . . . 6
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑜 =
(𝑎(,)𝑏))) |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
⊢ (𝑜 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)) |
5 | | elxr 11826 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℝ*
↔ (𝑏 ∈ ℝ
∨ 𝑏 = +∞ ∨
𝑏 =
-∞)) |
6 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ 𝑏 ∈
ℝ) |
7 | | elioore 12076 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ) |
8 | 6, 7 | anim12ci 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ)) |
9 | | relowlssretop.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐼 = ([,) “ (ℝ ×
ℝ)) |
10 | 9 | icoreelrn 32385 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼) |
12 | 7 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
13 | 7 | leidd 10473 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ≤ 𝑥) |
14 | 13 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ≤ 𝑥) |
15 | 6 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ 𝑏 ∈
ℝ*) |
16 | | elioo1 12086 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
17 | 15, 16 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
→ (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
18 | 17 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) |
19 | 18 | simp3d 1068 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 < 𝑏) |
20 | | rexr 9964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
21 | 20 | 3anim1i 1241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏)) |
22 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℝ*) |
23 | | elico1 12089 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏))) |
24 | 20, 22, 23 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏))) |
25 | 24 | biimprd 237 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏))) |
26 | 8, 21, 25 | syl2im 39 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏))) |
27 | | icoreval 32377 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
28 | 8, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
29 | 28 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ (𝑥[,)𝑏) ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
30 | 26, 29 | sylibd 228 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
31 | 12, 14, 19, 30 | mp3and 1419 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) |
32 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) |
33 | | nfrab1 3099 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧{𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} |
34 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧(𝑎(,)𝑏) |
35 | | iooval 12070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎(,)𝑏) = {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)}) |
36 | 35 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)})) |
37 | 36 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ↔ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}))) |
38 | 37 | pm5.32i 667 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ (𝑥 ∈ {𝑥 ∈ ℝ*
∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}))) |
39 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ↔ (𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏))) |
40 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) |
41 | 39, 40 | anbi12i 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ↔ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) |
42 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 ∈ ℝ) |
43 | 42 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 ∈ ℝ*) |
44 | 43 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ ℝ*) |
45 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) → 𝑥 ∈ ℝ*) |
46 | 45, 43 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) → (𝑥 ∈ ℝ* ∧ 𝑧 ∈
ℝ*)) |
47 | 46 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*))) |
48 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ↔ (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*))) |
49 | 47, 48 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 ∈ ℝ* ∧ 𝑥 ∈ ℝ*
∧ 𝑧 ∈
ℝ*)) |
50 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) → 𝑎 < 𝑥) |
51 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑥 ≤ 𝑧) |
52 | 50, 51 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ ℝ*
∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏))) → (𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧)) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧)) |
54 | | xrltletr 11864 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → ((𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧) → 𝑎 < 𝑧)) |
55 | 49, 53, 54 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑎 < 𝑧) |
56 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)) → 𝑧 < 𝑏) |
57 | 56 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 < 𝑏) |
58 | 55, 57 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)) |
59 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ* ∧ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏))) |
60 | 44, 58, 59 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ ((𝑥 ∈
ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
61 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
62 | | iooval 12070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧 ∧ 𝑧 < 𝑏)}) |
64 | 61, 63 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)))) → 𝑧 ∈ (𝑎(,)𝑏)) |
65 | 41, 64 | sylan2b 491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏)) |
66 | 38, 65 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏)) |
67 | 66 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → 𝑧 ∈ (𝑎(,)𝑏))) |
68 | 32, 33, 34, 67 | ssrd 3573 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)) |
69 | 22, 68 | sylanl2 681 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)) |
70 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)})) |
71 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))) |
72 | 70, 71 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)))) |
73 | 72 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
74 | 11, 31, 69, 73 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈ ℝ)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
75 | 74 | ancom1s 843 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
76 | 75 | expl 646 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℝ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
77 | 7 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
78 | | peano2re 10088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 + 1) ∈ ℝ) |
80 | 9 | icoreelrn 32385 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
{𝑧 ∈ ℝ ∣
(𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼) |
81 | 77, 79, 80 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼) |
82 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝑎(,)+∞) → 𝑥 ∈ ℝ) |
83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈
ℝ) |
84 | 83 | leidd 10473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ≤ 𝑥) |
85 | 83 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 < (𝑥 + 1)) |
86 | 83, 84, 85 | jca32 556 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ ℝ ∧ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
87 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → (𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑥)) |
88 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → (𝑧 < (𝑥 + 1) ↔ 𝑥 < (𝑥 + 1))) |
89 | 87, 88 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → ((𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)) ↔ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
90 | 89 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ↔ (𝑥 ∈ ℝ ∧ (𝑥 ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)))) |
91 | 86, 90 | sylibr 223 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))}) |
92 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧(𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) |
93 | | nfrab1 3099 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧{𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} |
94 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑧(𝑎(,)+∞) |
95 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ↔ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) |
96 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ) |
97 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 ∈ ℝ*) |
98 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ) |
99 | 98 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ*) |
100 | 96 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ*) |
101 | | elioopnf 12138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℝ*
→ (𝑥 ∈ (𝑎(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑎 < 𝑥))) |
102 | 101 | simplbda 652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → 𝑎 < 𝑥) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑥) |
104 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))) → 𝑥 ≤ 𝑧) |
105 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑥 ≤ 𝑧) |
106 | 97, 99, 100, 103, 105 | xrltletrd 11868 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑧) |
107 | | elioopnf 12138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℝ*
→ (𝑧 ∈ (𝑎(,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝑎 < 𝑧))) |
108 | 107 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ ℝ*
→ ((𝑧 ∈ ℝ
∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞))) |
111 | 96, 106, 110 | mp2and 711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1)))) → 𝑧 ∈ (𝑎(,)+∞)) |
112 | 111 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))) → 𝑧 ∈ (𝑎(,)+∞))) |
113 | 95, 112 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → 𝑧 ∈ (𝑎(,)+∞))) |
114 | 92, 93, 94, 113 | ssrd 3573 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)) |
115 | 91, 114 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))) |
116 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = +∞ → (𝑎(,)𝑏) = (𝑎(,)+∞)) |
117 | 116 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = +∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)+∞))) |
118 | 117 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) ↔ (𝑎 ∈ ℝ* ∧ 𝑥 ∈ (𝑎(,)+∞)))) |
119 | 116 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = +∞ → ({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))) |
120 | 119 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = +∞ → ((𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)))) |
121 | 118, 120 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = +∞ → (((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) ↔ ((𝑎 ∈ ℝ* ∧ 𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))))) |
122 | 115, 121 | mpbiri 247 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))) |
123 | 122 | impl 648 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
124 | 123 | ancom1s 843 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
125 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → (𝑥 ∈ 𝑖 ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))})) |
126 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) |
127 | 125, 126 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))) |
128 | 127 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (({𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
129 | 81, 124, 128 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = +∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
130 | 129 | ancom1s 843 |
. . . . . . . . . . . 12
⊢ (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
131 | 130 | expl 646 |
. . . . . . . . . . 11
⊢ (𝑏 = +∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
132 | 7 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ) |
133 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = -∞ → (𝑎(,)𝑏) = (𝑎(,)-∞)) |
134 | 133 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = -∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞))) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) →
(𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞))) |
136 | 135 | pm5.32i 667 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)-∞))) |
137 | | nltmnf 11839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 <
-∞) |
138 | 137 | intnand 953 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ*
→ ¬ (𝑎 < 𝑥 ∧ 𝑥 < -∞)) |
139 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑎(,)-∞) → (𝑎 < 𝑥 ∧ 𝑥 < -∞)) |
140 | 138, 139 | nsyl 134 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 ∈
(𝑎(,)-∞)) |
141 | 140 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ (𝑥 ∈ (𝑎(,)-∞) → ((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))))) |
142 | 141 | impd 446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ((𝑥 ∈ (𝑎(,)-∞) ∧ (𝑎 ∈ ℝ*
∧ 𝑏 = -∞)) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
143 | 142 | ancomsd 469 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ*
→ (((𝑎 ∈
ℝ* ∧ 𝑏
= -∞) ∧ 𝑥 ∈
(𝑎(,)-∞)) →
∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
144 | 136, 143 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ (((𝑎 ∈
ℝ* ∧ 𝑏
= -∞) ∧ 𝑥 ∈
(𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
145 | 20, 144 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
146 | 132, 145 | mpcom 37 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 = -∞) ∧
𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
147 | 146 | ancom1s 843 |
. . . . . . . . . . . 12
⊢ (((𝑏 = -∞ ∧ 𝑎 ∈ ℝ*)
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))) |
148 | 147 | expl 646 |
. . . . . . . . . . 11
⊢ (𝑏 = -∞ → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
149 | 76, 131, 148 | 3jaoi 1383 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞) → ((𝑎 ∈ ℝ*
∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
150 | 5, 149 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ*
→ ((𝑎 ∈
ℝ* ∧ 𝑥
∈ (𝑎(,)𝑏)) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
151 | 150 | expdimp 452 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℝ*
∧ 𝑎 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
152 | 151 | ancoms 468 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
153 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 ↔ 𝑥 ∈ (𝑎(,)𝑏))) |
154 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑜 = (𝑎(,)𝑏) → (𝑖 ⊆ 𝑜 ↔ 𝑖 ⊆ (𝑎(,)𝑏))) |
155 | 154 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜) ↔ (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
156 | 155 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑜 = (𝑎(,)𝑏) → (∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜) ↔ ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏)))) |
157 | 153, 156 | imbi12d 333 |
. . . . . . 7
⊢ (𝑜 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) ↔ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ (𝑎(,)𝑏))))) |
158 | 152, 157 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)))) |
159 | 158 | rexlimivv 3018 |
. . . . 5
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
160 | 4, 159 | sylbi 206 |
. . . 4
⊢ (𝑜 ∈ ran (,) → (𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
161 | 160 | rgen 2906 |
. . 3
⊢
∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) |
162 | 161 | rgenw 2908 |
. 2
⊢
∀𝑥 ∈
ℝ ∀𝑜 ∈
ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) |
163 | | iooex 12069 |
. . . . 5
⊢ (,)
∈ V |
164 | 163 | rnex 6992 |
. . . 4
⊢ ran (,)
∈ V |
165 | | unirnioo 12144 |
. . . . 5
⊢ ℝ =
∪ ran (,) |
166 | 9 | icoreunrn 32383 |
. . . . 5
⊢ ℝ =
∪ 𝐼 |
167 | 165, 166 | eqtr3i 2634 |
. . . 4
⊢ ∪ ran (,) = ∪ 𝐼 |
168 | | tgss2 20602 |
. . . 4
⊢ ((ran (,)
∈ V ∧ ∪ ran (,) = ∪ 𝐼)
→ ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)))) |
169 | 164, 167,
168 | mp2an 704 |
. . 3
⊢
((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
170 | 165 | raleqi 3119 |
. . 3
⊢
(∀𝑥 ∈
ℝ ∀𝑜 ∈
ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜)) ↔ ∀𝑥 ∈ ∪ ran
(,)∀𝑜 ∈ ran
(,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
171 | 169, 170 | bitr4i 266 |
. 2
⊢
((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ℝ ∀𝑜 ∈ ran (,)(𝑥 ∈ 𝑜 → ∃𝑖 ∈ 𝐼 (𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜))) |
172 | 162, 171 | mpbir 220 |
1
⊢
(topGen‘ran (,)) ⊆ (topGen‘𝐼) |