| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | icossicc 13476 | . . . . . . 7
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 2 | 1 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)) | 
| 3 | 2 | sselda 3983 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 4 |  | elico1 13430 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵))) | 
| 5 | 4 | biimpa 476 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)) | 
| 6 | 5 | simp1d 1143 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ ℝ*) | 
| 7 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 8 | 5 | simp3d 1145 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 < 𝐵) | 
| 9 |  | xrltne 13205 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
< 𝐵) → 𝐵 ≠ 𝑥) | 
| 10 | 6, 7, 8, 9 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝐵 ≠ 𝑥) | 
| 11 | 10 | necomd 2996 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ≠ 𝐵) | 
| 12 | 11 | neneqd 2945 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → ¬ 𝑥 = 𝐵) | 
| 13 |  | velsn 4642 | . . . . . 6
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) | 
| 14 | 12, 13 | sylnibr 329 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → ¬ 𝑥 ∈ {𝐵}) | 
| 15 | 3, 14 | eldifd 3962 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ (𝐴[,)𝐵)) → 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) | 
| 16 | 15 | ex 412 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,)𝐵) → 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}))) | 
| 17 | 16 | ssrdv 3989 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) ⊆ ((𝐴[,]𝐵) ∖ {𝐵})) | 
| 18 |  | simpll 767 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐴 ∈
ℝ*) | 
| 19 |  | simplr 769 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐵 ∈
ℝ*) | 
| 20 |  | eldifi 4131 | . . . . 5
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 21 |  | eliccxr 13475 | . . . . 5
⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ*) | 
| 22 | 20, 21 | syl 17 | . . . 4
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ∈ ℝ*) | 
| 23 | 22 | adantl 481 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ ℝ*) | 
| 24 | 20 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 25 |  | elicc1 13431 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 26 | 25 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | 
| 27 | 24, 26 | mpbid 232 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) | 
| 28 | 27 | simp2d 1144 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐴 ≤ 𝑥) | 
| 29 |  | eldifsni 4790 | . . . . . 6
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝑥 ≠ 𝐵) | 
| 30 | 29 | necomd 2996 | . . . . 5
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵}) → 𝐵 ≠ 𝑥) | 
| 31 | 30 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝐵 ≠ 𝑥) | 
| 32 | 27 | simp3d 1145 | . . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ≤ 𝐵) | 
| 33 |  | xrleltne 13187 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
≤ 𝐵) → (𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥)) | 
| 34 | 23, 19, 32, 33 | syl3anc 1373 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → (𝑥 < 𝐵 ↔ 𝐵 ≠ 𝑥)) | 
| 35 | 31, 34 | mpbird 257 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 < 𝐵) | 
| 36 | 18, 19, 23, 28, 35 | elicod 13437 | . 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∖ {𝐵})) → 𝑥 ∈ (𝐴[,)𝐵)) | 
| 37 | 17, 36 | eqelssd 4005 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵})) |