| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1191 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝐴 ∈
ℝ*) | 
| 2 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝐵 ∈
ℝ*) | 
| 3 |  | simprl 770 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 4 |  | iccleub 13443 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) | 
| 5 | 1, 2, 3, 4 | syl3anc 1372 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝑥 ≤ 𝐵) | 
| 6 |  | simpl3 1193 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝐶 ∈
ℝ*) | 
| 7 |  | simprr 772 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝑥 ∈ (𝐵[,]𝐶)) | 
| 8 |  | iccgelb 13444 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,]𝐶)) → 𝐵 ≤ 𝑥) | 
| 9 | 2, 6, 7, 8 | syl3anc 1372 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝐵 ≤ 𝑥) | 
| 10 |  | eliccxr 13476 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ*) | 
| 11 | 3, 10 | syl 17 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝑥 ∈ ℝ*) | 
| 12 | 11, 2 | jca 511 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → (𝑥 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 13 |  | xrletri3 13197 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 = 𝐵 ↔ (𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥))) | 
| 14 | 12, 13 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → (𝑥 = 𝐵 ↔ (𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥))) | 
| 15 | 5, 9, 14 | mpbir2and 713 | . . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) → 𝑥 = 𝐵) | 
| 16 | 15 | ex 412 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶)) → 𝑥 = 𝐵)) | 
| 17 | 16 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶)) → 𝑥 = 𝐵)) | 
| 18 |  | simpll1 1212 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝐴 ∈
ℝ*) | 
| 19 |  | simpll2 1213 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) | 
| 20 |  | simplrl 776 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝐴 ≤ 𝐵) | 
| 21 |  | simpr 484 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 22 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 23 |  | ubicc2 13506 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝑥 = 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 25 | 22, 24 | eqeltrd 2840 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 26 | 18, 19, 20, 21, 25 | syl31anc 1374 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 27 |  | simpll3 1214 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝐶 ∈
ℝ*) | 
| 28 |  | simplrr 777 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝐵 ≤ 𝐶) | 
| 29 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 30 |  | lbicc2 13505 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) ∧ 𝑥 = 𝐵) → 𝐵 ∈ (𝐵[,]𝐶)) | 
| 32 | 29, 31 | eqeltrd 2840 | . . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,]𝐶)) | 
| 33 | 19, 27, 28, 21, 32 | syl31anc 1374 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,]𝐶)) | 
| 34 | 26, 33 | jca 511 | . . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) ∧ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) | 
| 35 | 34 | ex 412 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → (𝑥 = 𝐵 → (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶)))) | 
| 36 | 17, 35 | impbid 212 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶)) ↔ 𝑥 = 𝐵)) | 
| 37 |  | elin 3966 | . . 3
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑥 ∈ (𝐵[,]𝐶))) | 
| 38 |  | velsn 4641 | . . 3
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) | 
| 39 | 36, 37, 38 | 3bitr4g 314 | . 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → (𝑥 ∈ ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) ↔ 𝑥 ∈ {𝐵})) | 
| 40 | 39 | eqrdv 2734 | 1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵}) |