Step | Hyp | Ref
| Expression |
1 | | icossicc 12131 |
. . . . . . 7
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)) |
3 | 2 | sselda 3568 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
4 | | elico1 12089 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵))) |
5 | 4 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)) |
6 | 5 | simp1d 1066 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ ℝ*) |
7 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝐵 ∈
ℝ*) |
8 | 5 | simp3d 1068 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 < 𝐵) |
9 | | xrltne 11870 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
< 𝐵) → 𝐵 ≠ 𝑥) |
10 | 6, 7, 8, 9 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝐵 ≠ 𝑥) |
11 | 10 | necomd 2837 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ≠ 𝐵) |
12 | 11 | neneqd 2787 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → ¬ 𝑥 = 𝐵) |
13 | | velsn 4141 |
. . . . . 6
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
14 | 12, 13 | sylnibr 318 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → ¬ 𝑥 ∈ {𝐵}) |
15 | 3, 14 | eldifd 3551 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) |
16 | 15 | ex 449 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,)𝐵) → 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}))) |
17 | 16 | ssrdv 3574 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) ⊆ ((𝐴[,]𝐵) ∖ {𝐵})) |
18 | | simpll 786 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐴 ∈
ℝ*) |
19 | | simplr 788 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐵 ∈
ℝ*) |
20 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ∈ (𝐴[,]𝐵)) |
21 | | eliccxr 38584 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ*) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ∈ ℝ*) |
23 | 22 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ ℝ*) |
24 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ (𝐴[,]𝐵)) |
25 | | elicc1 12090 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
27 | 24, 26 | mpbid 221 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
28 | 27 | simp2d 1067 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐴 ≤ 𝑥) |
29 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ≠ 𝐵) |
30 | 29 | necomd 2837 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝐵 ≠ 𝑥) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐵 ≠ 𝑥) |
32 | 27 | simp3d 1068 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ≤ 𝐵) |
33 | | xrleltne 11854 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
≤ 𝐵) → (𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥)) |
34 | 23, 19, 32, 33 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥)) |
35 | 31, 34 | mpbird 246 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 < 𝐵) |
36 | 18, 19, 23, 28, 35 | elicod 12095 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ (𝐴[,)𝐵)) |
37 | 36 | ex 449 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ∈ (𝐴[,)𝐵))) |
38 | 37 | ssrdv 3574 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,]𝐵) ∖ {𝐵}) ⊆ (𝐴[,)𝐵)) |
39 | 17, 38 | eqssd 3585 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵})) |