Step | Hyp | Ref
| Expression |
1 | | difssd 3700 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐵}) ⊆ (𝐴(,)𝐵)) |
2 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
3 | | ubioo 12078 |
. . . . . . . . . . . . . 14
⊢ ¬
𝐵 ∈ (𝐴(,)𝐵) |
4 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴(,)𝐵) ↔ 𝐵 ∈ (𝐴(,)𝐵))) |
5 | 4 | biimpcd 238 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝑥 = 𝐵 → 𝐵 ∈ (𝐴(,)𝐵))) |
6 | 3, 5 | mtoi 189 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵) |
7 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐵) |
8 | | velsn 4141 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
9 | 7, 8 | sylnibr 318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 ∈ {𝐵}) |
10 | 2, 9 | eldifd 3551 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ((𝐴(,)𝐵) ∖ {𝐵})) |
11 | 10 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∖ {𝐵}))) |
12 | 11 | ssrdv 3574 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∖ {𝐵})) |
13 | 1, 12 | eqssd 3585 |
. . . . . . 7
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐵}) = (𝐴(,)𝐵)) |
14 | 13 | ineq2d 3776 |
. . . . . 6
⊢ (𝜑 → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) |
15 | 14 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) |
16 | | simplrl 796 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ ℝ*) |
17 | | simplrr 797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ ℝ*) |
18 | | lptioo2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
19 | 18 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐴 ∈
ℝ*) |
20 | | elioo3g 12075 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝑎 < 𝐵 ∧ 𝐵 < 𝑏))) |
21 | 20 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝑎 < 𝐵 ∧ 𝐵 < 𝑏))) |
22 | 21 | simpld 474 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*)) |
23 | 22 | simp3d 1068 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 ∈
ℝ*) |
24 | 23 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐵 ∈
ℝ*) |
25 | | iooin 12080 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
26 | 16, 17, 19, 24, 25 | syl22anc 1319 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
27 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑎 ≤ 𝐴 → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
28 | 27 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
29 | | lptioo2.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
30 | 29 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → 𝐴 < 𝐵) |
31 | 28, 30 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
32 | | iffalse 4045 |
. . . . . . . . . . 11
⊢ (¬
𝑎 ≤ 𝐴 → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
33 | 32 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
34 | 21 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝑎 < 𝐵 ∧ 𝐵 < 𝑏)) |
35 | 34 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝑎 < 𝐵) |
36 | 35 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → 𝑎 < 𝐵) |
37 | 33, 36 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
38 | 31, 37 | pm2.61dan 828 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
39 | 34 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 < 𝑏) |
40 | 22 | simp2d 1067 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝑏 ∈ ℝ*) |
41 | | xrltnle 9984 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵)) |
42 | 23, 40, 41 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵)) |
43 | 39, 42 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → ¬ 𝑏 ≤ 𝐵) |
44 | | iffalse 4045 |
. . . . . . . . . . 11
⊢ (¬
𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) |
46 | 45 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
48 | 38, 47 | breqtrd 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
49 | 19, 16 | ifcld 4081 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈
ℝ*) |
50 | 47, 24 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈
ℝ*) |
51 | | ioon0 12072 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈ ℝ*) →
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
52 | 49, 50, 51 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
53 | 48, 52 | mpbird 246 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅) |
54 | 26, 53 | eqnetrd 2849 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) ≠ ∅) |
55 | 15, 54 | eqnetrd 2849 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅) |
56 | 55 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
→ (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅)) |
57 | 56 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅)) |
58 | | lptioo2.1 |
. . 3
⊢ 𝐽 = (topGen‘ran
(,)) |
59 | | ioossre 12106 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℝ |
60 | 59 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
61 | | lptioo2.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
62 | 58, 60, 61 | islptre 38686 |
. 2
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅))) |
63 | 57, 62 | mpbird 246 |
1
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) |