| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iccdificc.b | . . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 2 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 ∈
ℝ*) | 
| 3 |  | iccdificc.c | . . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) | 
| 4 | 3 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐶 ∈
ℝ*) | 
| 5 |  | iccssxr 13471 | . . . . . . 7
⊢ (𝐴[,]𝐶) ⊆
ℝ* | 
| 6 |  | eldifi 4130 | . . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐶)) | 
| 7 | 5, 6 | sselid 3980 | . . . . . 6
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ*) | 
| 8 | 7 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ ℝ*) | 
| 9 |  | iccdificc.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 10 | 9 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ∈
ℝ*) | 
| 11 | 2 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐵 ∈
ℝ*) | 
| 12 | 8 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) | 
| 13 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ∈
ℝ*) | 
| 14 | 6 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐴[,]𝐶)) | 
| 15 |  | iccgelb 13444 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝐴 ≤ 𝑥) | 
| 16 | 13, 4, 14, 15 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐴 ≤ 𝑥) | 
| 17 | 16 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝐴 ≤ 𝑥) | 
| 18 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝐵 < 𝑥) | 
| 19 | 8, 2 | xrlenltd 11328 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → (𝑥 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑥)) | 
| 21 | 18, 20 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ≤ 𝐵) | 
| 22 | 10, 11, 12, 17, 21 | eliccxrd 45545 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 23 |  | eldifn 4131 | . . . . . . 7
⊢ (𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) | 
| 24 | 23 | ad2antlr 727 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) ∧ ¬ 𝐵 < 𝑥) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) | 
| 25 | 22, 24 | condan 817 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝐵 < 𝑥) | 
| 26 |  | iccleub 13443 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐶)) → 𝑥 ≤ 𝐶) | 
| 27 | 13, 4, 14, 26 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ≤ 𝐶) | 
| 28 | 2, 4, 8, 25, 27 | eliocd 45525 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) → 𝑥 ∈ (𝐵(,]𝐶)) | 
| 29 | 28 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) | 
| 30 |  | dfss3 3971 | . . 3
⊢ (((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶) ↔ ∀𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))𝑥 ∈ (𝐵(,]𝐶)) | 
| 31 | 29, 30 | sylibr 234 | . 2
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) ⊆ (𝐵(,]𝐶)) | 
| 32 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ∈
ℝ*) | 
| 33 | 3 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) | 
| 34 |  | iocssxr 13472 | . . . . . 6
⊢ (𝐵(,]𝐶) ⊆
ℝ* | 
| 35 |  | id 22 | . . . . . 6
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) | 
| 36 | 34, 35 | sselid 3980 | . . . . 5
⊢ (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ℝ*) | 
| 37 | 36 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ*) | 
| 38 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) | 
| 39 |  | iccdificc.4 | . . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 40 | 39 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝐵) | 
| 41 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) | 
| 42 |  | iocgtlb 45520 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) | 
| 43 | 38, 33, 41, 42 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) | 
| 44 | 32, 38, 37, 40, 43 | xrlelttrd 13203 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 < 𝑥) | 
| 45 | 32, 37, 44 | xrltled 13193 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐴 ≤ 𝑥) | 
| 46 |  | iocleub 45521 | . . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) | 
| 47 | 38, 33, 41, 46 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) | 
| 48 | 32, 33, 37, 45, 47 | eliccxrd 45545 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐴[,]𝐶)) | 
| 49 | 32, 38, 37, 43 | xrgtnelicc 45556 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) | 
| 50 | 48, 49 | eldifd 3961 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵))) | 
| 51 | 31, 50 | eqelssd 4004 | 1
⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶)) |