Step | Hyp | Ref
| Expression |
1 | | difssd 4072 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐵}) ⊆ (𝐴(,)𝐵)) |
2 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
3 | | ubioo 13122 |
. . . . . . . . . . . 12
⊢ ¬
𝐵 ∈ (𝐴(,)𝐵) |
4 | | eleq1 2828 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴(,)𝐵) ↔ 𝐵 ∈ (𝐴(,)𝐵))) |
5 | 4 | biimpcd 248 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝑥 = 𝐵 → 𝐵 ∈ (𝐴(,)𝐵))) |
6 | 3, 5 | mtoi 198 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐵) |
8 | | velsn 4583 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
9 | 7, 8 | sylnibr 329 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 ∈ {𝐵}) |
10 | 2, 9 | eldifd 3903 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ((𝐴(,)𝐵) ∖ {𝐵})) |
11 | 1, 10 | eqelssd 3947 |
. . . . . . 7
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐵}) = (𝐴(,)𝐵)) |
12 | 11 | ineq2d 4152 |
. . . . . 6
⊢ (𝜑 → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) |
13 | 12 | ad2antrr 723 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵))) |
14 | | simplrl 774 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ ℝ*) |
15 | | simplrr 775 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ ℝ*) |
16 | | lptioo2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
17 | 16 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐴 ∈
ℝ*) |
18 | | elioo3g 13119 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝑎 < 𝐵 ∧ 𝐵 < 𝑏))) |
19 | 18 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝑎 < 𝐵 ∧ 𝐵 < 𝑏))) |
20 | 19 | simpld 495 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐵 ∈
ℝ*)) |
21 | 20 | simp3d 1143 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 ∈
ℝ*) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐵 ∈
ℝ*) |
23 | | iooin 13124 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
24 | 14, 15, 17, 22, 23 | syl22anc 836 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
25 | | iftrue 4471 |
. . . . . . . . . . 11
⊢ (𝑎 ≤ 𝐴 → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
26 | 25 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
27 | | lptioo2.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
28 | 27 | ad3antrrr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → 𝐴 < 𝐵) |
29 | 26, 28 | eqbrtrd 5101 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
30 | | iffalse 4474 |
. . . . . . . . . . 11
⊢ (¬
𝑎 ≤ 𝐴 → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
31 | 30 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
32 | 19 | simprd 496 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝑎 < 𝐵 ∧ 𝐵 < 𝑏)) |
33 | 32 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝑎 < 𝐵) |
34 | 33 | ad2antlr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → 𝑎 < 𝐵) |
35 | 31, 34 | eqbrtrd 5101 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
36 | 29, 35 | pm2.61dan 810 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < 𝐵) |
37 | 32 | simprd 496 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 < 𝑏) |
38 | 20 | simp2d 1142 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝑏 ∈ ℝ*) |
39 | | xrltnle 11053 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵)) |
40 | 21, 38, 39 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑎(,)𝑏) → (𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵)) |
41 | 37, 40 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → ¬ 𝑏 ≤ 𝐵) |
42 | | iffalse 4474 |
. . . . . . . . . . 11
⊢ (¬
𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) |
44 | 43 | eqcomd 2746 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
45 | 44 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
46 | 36, 45 | breqtrd 5105 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
47 | 17, 14 | ifcld 4511 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈
ℝ*) |
48 | 45, 22 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈
ℝ*) |
49 | | ioon0 13116 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈ ℝ*) →
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
50 | 47, 48, 49 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
51 | 46, 50 | mpbird 256 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅) |
52 | 24, 51 | eqnetrd 3013 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) ≠ ∅) |
53 | 13, 52 | eqnetrd 3013 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅) |
54 | 53 | ex 413 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
→ (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅)) |
55 | 54 | ralrimivva 3117 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅)) |
56 | | lptioo2.1 |
. . 3
⊢ 𝐽 = (topGen‘ran
(,)) |
57 | | ioossre 13151 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℝ |
58 | 57 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
59 | | lptioo2.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
60 | 56, 58, 59 | islptre 43142 |
. 2
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐵})) ≠ ∅))) |
61 | 55, 60 | mpbird 256 |
1
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) |