Step | Hyp | Ref
| Expression |
1 | | difssd 3700 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝐴}) ⊆ (𝐴(,)𝐵)) |
2 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
3 | | lbioo 12077 |
. . . . . . . . . . . . . 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 | | lptioo1.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
19 | 18 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
20 | | lptioo1.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
21 | 19, 20 | jca 553 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
22 | 21 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
23 | | iooin 12080 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
24 | 16, 17, 22, 23 | syl21anc 1317 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
25 | | elioo3g 12075 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑎(,)𝑏) ↔ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) ∧ (𝑎 < 𝐴 ∧ 𝐴 < 𝑏))) |
26 | 25 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑎(,)𝑏) → ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) ∧ (𝑎 < 𝐴 ∧ 𝐴 < 𝑏))) |
27 | 26 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝐴 ∈
ℝ*)) |
28 | 27 | simp1d 1066 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 ∈ ℝ*) |
29 | 27 | simp3d 1068 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝐴 ∈
ℝ*) |
30 | 26 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑎(,)𝑏) → (𝑎 < 𝐴 ∧ 𝐴 < 𝑏)) |
31 | 30 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 < 𝐴) |
32 | 28, 29, 31 | xrltled 38427 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝑎 ≤ 𝐴) |
33 | 32 | iftrued 4044 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑎(,)𝑏) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
34 | 33 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝐴) |
35 | 30 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑎(,)𝑏) → 𝐴 < 𝑏) |
36 | 35 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝐴 < 𝑏) |
37 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝑏) |
38 | 37 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝑏 ≤ 𝐵 → 𝑏 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
39 | 38 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝑏 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
40 | 36, 39 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
41 | | lptioo1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
42 | 41 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐴 < 𝐵) |
43 | | iffalse 4045 |
. . . . . . . . . . . 12
⊢ (¬
𝑏 ≤ 𝐵 → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) = 𝐵) |
44 | 43 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (¬
𝑏 ≤ 𝐵 → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐵 = if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
46 | 42, 45 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
47 | 40, 46 | pm2.61dan 828 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → 𝐴 < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
48 | 34, 47 | eqbrtrd 4605 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) |
49 | 19 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑎 ≤ 𝐴) → 𝐴 ∈
ℝ*) |
50 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑎 ≤ 𝐴) → 𝑎 ∈ ℝ*) |
51 | 49, 50 | ifclda 4070 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈
ℝ*) |
52 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ 𝑏 ≤ 𝐵) → 𝑏 ∈ ℝ*) |
53 | 20 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) ∧ ¬ 𝑏 ≤ 𝐵) → 𝐵 ∈
ℝ*) |
54 | 52, 53 | ifclda 4070 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈
ℝ*) |
55 | | ioon0 12072 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎) ∈ ℝ* ∧ if(𝑏 ≤ 𝐵, 𝑏, 𝐵) ∈ ℝ*) →
((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
56 | 51, 54, 55 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅ ↔ if(𝑎 ≤ 𝐴, 𝐴, 𝑎) < if(𝑏 ≤ 𝐵, 𝑏, 𝐵))) |
57 | 48, 56 | mpbird 246 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(𝑏 ≤ 𝐵, 𝑏, 𝐵)) ≠ ∅) |
58 | 24, 57 | eqnetrd 2849 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴(,)𝐵)) ≠ ∅) |
59 | 15, 58 | eqnetrd 2849 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
∧ 𝐴 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅) |
60 | 59 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
→ (𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅)) |
61 | 60 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅)) |
62 | | lptioo1.1 |
. . 3
⊢ 𝐽 = (topGen‘ran
(,)) |
63 | | ioossre 12106 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℝ |
64 | 63 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
65 | 62, 64, 18 | islptre 38686 |
. 2
⊢ (𝜑 → (𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐴 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝐴(,)𝐵) ∖ {𝐴})) ≠ ∅))) |
66 | 61, 65 | mpbird 246 |
1
⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) |