Step | Hyp | Ref
| Expression |
1 | | df-in 3547 |
. . . . . 6
⊢ ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝑥 ∣ (𝑥 ∈ (𝐴(,]𝐵) ∧ 𝑥 ∈ (𝐵[,)𝐶))} |
2 | | elioc1 12088 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
3 | 2 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
4 | | 3simpb 1052 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵)) |
5 | 3, 4 | syl6bi 242 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝑥 ∈ (𝐴(,]𝐵) → (𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵))) |
6 | | elico1 12089 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝑥 ∈ (𝐵[,)𝐶) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶))) |
7 | 6 | 3adant1 1072 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝑥 ∈ (𝐵[,)𝐶) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶))) |
8 | | 3simpa 1051 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶) → (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)) |
9 | 7, 8 | syl6bi 242 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝑥 ∈ (𝐵[,)𝐶) → (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥))) |
10 | 5, 9 | anim12d 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝑥 ∈ (𝐴(,]𝐵) ∧ 𝑥 ∈ (𝐵[,)𝐶)) → ((𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵) ∧ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)))) |
11 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) ∧ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)) → 𝑥 ∈ ℝ*) |
12 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) ∧ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)) → 𝐵 ≤ 𝑥) |
13 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) ∧ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)) → 𝑥 ≤ 𝐵) |
14 | 11, 12, 13 | 3jca 1235 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) ∧ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥)) → (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
15 | 10, 14 | syl6 34 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝑥 ∈ (𝐴(,]𝐵) ∧ 𝑥 ∈ (𝐵[,)𝐶)) → (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
16 | | elicc1 12090 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐵[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
17 | 16 | anidms 675 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝑥 ∈ (𝐵[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝑥 ∈ (𝐵[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
19 | 15, 18 | sylibrd 248 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝑥 ∈ (𝐴(,]𝐵) ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ (𝐵[,]𝐵))) |
20 | 19 | ss2abdv 3638 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → {𝑥 ∣ (𝑥 ∈ (𝐴(,]𝐵) ∧ 𝑥 ∈ (𝐵[,)𝐶))} ⊆ {𝑥 ∣ 𝑥 ∈ (𝐵[,]𝐵)}) |
21 | 1, 20 | syl5eqss 3612 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) ⊆ {𝑥 ∣ 𝑥 ∈ (𝐵[,]𝐵)}) |
22 | | abid2 2732 |
. . . . 5
⊢ {𝑥 ∣ 𝑥 ∈ (𝐵[,]𝐵)} = (𝐵[,]𝐵) |
23 | 21, 22 | syl6sseq 3614 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) ⊆ (𝐵[,]𝐵)) |
24 | 23 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) ⊆ (𝐵[,]𝐵)) |
25 | | iccid 12091 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (𝐵[,]𝐵) = {𝐵}) |
26 | 25 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐵[,]𝐵) = {𝐵}) |
27 | 26 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐵[,]𝐵) = {𝐵}) |
28 | 24, 27 | sseqtrd 3604 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) ⊆ {𝐵}) |
29 | | simpl2 1058 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈
ℝ*) |
30 | | simprl 790 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐴 < 𝐵) |
31 | | xrleid 11859 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤ 𝐵) |
32 | 29, 31 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ≤ 𝐵) |
33 | | elioc1 12088 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐵 ∈ (𝐴(,]𝐵) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵))) |
34 | 33 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐵 ∈ (𝐴(,]𝐵) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵))) |
35 | 34 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐵 ∈ (𝐴(,]𝐵) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵))) |
36 | 29, 30, 32, 35 | mpbir3and 1238 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ (𝐴(,]𝐵)) |
37 | | simprr 792 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 < 𝐶) |
38 | | elico1 12089 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 ∈ (𝐵[,)𝐶) ↔ (𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶))) |
39 | 38 | 3adant1 1072 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐵 ∈ (𝐵[,)𝐶) ↔ (𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶))) |
40 | 39 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐵 ∈ (𝐵[,)𝐶) ↔ (𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶))) |
41 | 29, 32, 37, 40 | mpbir3and 1238 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ (𝐵[,)𝐶)) |
42 | 36, 41 | elind 3760 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶))) |
43 | 42 | snssd 4281 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → {𝐵} ⊆ ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶))) |
44 | 28, 43 | eqssd 3585 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) |