Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((topGen‘ran (,))
↾t 𝐴)
∈ Con) |
2 | | retopon 22377 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
3 | 2 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (topGen‘ran (,)) ∈
(TopOn‘ℝ)) |
4 | | simplll 794 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ℝ) |
5 | | iooretop 22379 |
. . . . . . 7
⊢
(-∞(,)𝑧)
∈ (topGen‘ran (,)) |
6 | 5 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (-∞(,)𝑧) ∈ (topGen‘ran
(,))) |
7 | | iooretop 22379 |
. . . . . . 7
⊢ (𝑧(,)+∞) ∈
(topGen‘ran (,)) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧(,)+∞) ∈ (topGen‘ran
(,))) |
9 | | simplrl 796 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ∈ 𝐴) |
10 | 4, 9 | sseldd 3569 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ∈ ℝ) |
11 | | mnflt 11833 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ → -∞
< 𝑋) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ < 𝑋) |
13 | | eldifn 3695 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → ¬ 𝑧 ∈ 𝐴) |
14 | 13 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑧 ∈ 𝐴) |
15 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑋 = 𝑧 → (𝑋 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
16 | 9, 15 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 = 𝑧 → 𝑧 ∈ 𝐴)) |
17 | 14, 16 | mtod 188 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑋 = 𝑧) |
18 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → 𝑧 ∈ (𝑋[,]𝑌)) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ (𝑋[,]𝑌)) |
20 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 ∈ 𝐴) |
21 | 4, 20 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 ∈ ℝ) |
22 | | elicc2 12109 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑧 ∈ (𝑋[,]𝑌) ↔ (𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌))) |
23 | 10, 21, 22 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ (𝑋[,]𝑌) ↔ (𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌))) |
24 | 19, 23 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌)) |
25 | 24 | simp2d 1067 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ≤ 𝑧) |
26 | 24 | simp1d 1066 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ ℝ) |
27 | 10, 26 | leloed 10059 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 ≤ 𝑧 ↔ (𝑋 < 𝑧 ∨ 𝑋 = 𝑧))) |
28 | 25, 27 | mpbid 221 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 < 𝑧 ∨ 𝑋 = 𝑧)) |
29 | 28 | ord 391 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (¬ 𝑋 < 𝑧 → 𝑋 = 𝑧)) |
30 | 17, 29 | mt3d 139 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 < 𝑧) |
31 | | mnfxr 9975 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
32 | 26 | rexrd 9968 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ ℝ*) |
33 | | elioo2 12087 |
. . . . . . . . 9
⊢
((-∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (𝑋 ∈ (-∞(,)𝑧) ↔ (𝑋 ∈ ℝ ∧ -∞ < 𝑋 ∧ 𝑋 < 𝑧))) |
34 | 31, 32, 33 | sylancr 694 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 ∈ (-∞(,)𝑧) ↔ (𝑋 ∈ ℝ ∧ -∞ < 𝑋 ∧ 𝑋 < 𝑧))) |
35 | 10, 12, 30, 34 | mpbir3and 1238 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ∈ (-∞(,)𝑧)) |
36 | | inelcm 3984 |
. . . . . . 7
⊢ ((𝑋 ∈ (-∞(,)𝑧) ∧ 𝑋 ∈ 𝐴) → ((-∞(,)𝑧) ∩ 𝐴) ≠ ∅) |
37 | 35, 9, 36 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((-∞(,)𝑧) ∩ 𝐴) ≠ ∅) |
38 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑌 → (𝑧 ∈ 𝐴 ↔ 𝑌 ∈ 𝐴)) |
39 | 20, 38 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 = 𝑌 → 𝑧 ∈ 𝐴)) |
40 | 14, 39 | mtod 188 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑧 = 𝑌) |
41 | 24 | simp3d 1068 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ≤ 𝑌) |
42 | 26, 21 | leloed 10059 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ≤ 𝑌 ↔ (𝑧 < 𝑌 ∨ 𝑧 = 𝑌))) |
43 | 41, 42 | mpbid 221 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 < 𝑌 ∨ 𝑧 = 𝑌)) |
44 | 43 | ord 391 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (¬ 𝑧 < 𝑌 → 𝑧 = 𝑌)) |
45 | 40, 44 | mt3d 139 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 < 𝑌) |
46 | | ltpnf 11830 |
. . . . . . . . 9
⊢ (𝑌 ∈ ℝ → 𝑌 < +∞) |
47 | 21, 46 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 < +∞) |
48 | | pnfxr 9971 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
49 | | elioo2 12087 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑌 ∈ (𝑧(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑧 < 𝑌 ∧ 𝑌 < +∞))) |
50 | 32, 48, 49 | sylancl 693 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑌 ∈ (𝑧(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑧 < 𝑌 ∧ 𝑌 < +∞))) |
51 | 21, 45, 47, 50 | mpbir3and 1238 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 ∈ (𝑧(,)+∞)) |
52 | | inelcm 3984 |
. . . . . . 7
⊢ ((𝑌 ∈ (𝑧(,)+∞) ∧ 𝑌 ∈ 𝐴) → ((𝑧(,)+∞) ∩ 𝐴) ≠ ∅) |
53 | 51, 20, 52 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((𝑧(,)+∞) ∩ 𝐴) ≠ ∅) |
54 | | inss1 3795 |
. . . . . . 7
⊢
(((-∞(,)𝑧)
∩ (𝑧(,)+∞)) ∩
𝐴) ⊆
((-∞(,)𝑧) ∩
(𝑧(,)+∞)) |
55 | 32, 31 | jctil 558 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (-∞ ∈
ℝ* ∧ 𝑧
∈ ℝ*)) |
56 | 32, 48 | jctir 559 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ ℝ* ∧ +∞
∈ ℝ*)) |
57 | 26 | leidd 10473 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ≤ 𝑧) |
58 | | ioodisj 12173 |
. . . . . . . 8
⊢
((((-∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ*) ∧ (𝑧 ∈ ℝ*
∧ +∞ ∈ ℝ*)) ∧ 𝑧 ≤ 𝑧) → ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) = ∅) |
59 | 55, 56, 57, 58 | syl21anc 1317 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) = ∅) |
60 | | sseq0 3927 |
. . . . . . 7
⊢
(((((-∞(,)𝑧)
∩ (𝑧(,)+∞)) ∩
𝐴) ⊆
((-∞(,)𝑧) ∩
(𝑧(,)+∞)) ∧
((-∞(,)𝑧) ∩
(𝑧(,)+∞)) = ∅)
→ (((-∞(,)𝑧)
∩ (𝑧(,)+∞)) ∩
𝐴) =
∅) |
61 | 54, 59, 60 | sylancr 694 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∩ 𝐴) = ∅) |
62 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ ∈
ℝ*) |
63 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → +∞ ∈
ℝ*) |
64 | | mnflt 11833 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ → -∞
< 𝑧) |
65 | 26, 64 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ < 𝑧) |
66 | | ltpnf 11830 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ → 𝑧 < +∞) |
67 | 26, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 < +∞) |
68 | | ioojoin 12174 |
. . . . . . . . . 10
⊢
(((-∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < 𝑧 ∧ 𝑧 < +∞)) → (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) =
(-∞(,)+∞)) |
69 | 62, 32, 63, 65, 67, 68 | syl32anc 1326 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) =
(-∞(,)+∞)) |
70 | | unass 3732 |
. . . . . . . . . 10
⊢
(((-∞(,)𝑧)
∪ {𝑧}) ∪ (𝑧(,)+∞)) =
((-∞(,)𝑧) ∪
({𝑧} ∪ (𝑧(,)+∞))) |
71 | | un12 3733 |
. . . . . . . . . 10
⊢
((-∞(,)𝑧)
∪ ({𝑧} ∪ (𝑧(,)+∞))) = ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) |
72 | 70, 71 | eqtri 2632 |
. . . . . . . . 9
⊢
(((-∞(,)𝑧)
∪ {𝑧}) ∪ (𝑧(,)+∞)) = ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) |
73 | | ioomax 12119 |
. . . . . . . . 9
⊢
(-∞(,)+∞) = ℝ |
74 | 69, 72, 73 | 3eqtr3g 2667 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) = ℝ) |
75 | 4, 74 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))) |
76 | | disjsn 4192 |
. . . . . . . . 9
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
77 | 14, 76 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝐴 ∩ {𝑧}) = ∅) |
78 | | disjssun 3988 |
. . . . . . . 8
⊢ ((𝐴 ∩ {𝑧}) = ∅ → (𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) ↔ 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) ↔ 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))) |
80 | 75, 79 | mpbid 221 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) |
81 | 3, 4, 6, 8, 37, 53, 61, 80 | nconsubb 21036 |
. . . . 5
⊢ ((((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ ((topGen‘ran (,))
↾t 𝐴)
∈ Con) |
82 | 81 | ex 449 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → ¬ ((topGen‘ran (,))
↾t 𝐴)
∈ Con)) |
83 | 1, 82 | mt2d 130 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ¬ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) |
84 | 83 | eq0rdv 3931 |
. 2
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝑋[,]𝑌) ∖ 𝐴) = ∅) |
85 | | ssdif0 3896 |
. 2
⊢ ((𝑋[,]𝑌) ⊆ 𝐴 ↔ ((𝑋[,]𝑌) ∖ 𝐴) = ∅) |
86 | 84, 85 | sylibr 223 |
1
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴) |