Proof of Theorem difdifdirss
Step | Hyp | Ref
| Expression |
1 | | dif32 3390 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
2 | | invdif 3369 |
. . . . 5
⊢ ((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
3 | 1, 2 | eqtr4i 2194 |
. . . 4
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) |
4 | | un0 3447 |
. . . 4
⊢ (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ∅) = ((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) |
5 | 3, 4 | eqtr4i 2194 |
. . 3
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ∅) |
6 | | indi 3374 |
. . . 4
⊢ ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) = (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ((𝐴 ∖ 𝐶) ∩ 𝐶)) |
7 | | disjdif 3486 |
. . . . . 6
⊢ (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅ |
8 | | incom 3319 |
. . . . . 6
⊢ (𝐶 ∩ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) ∩ 𝐶) |
9 | 7, 8 | eqtr3i 2193 |
. . . . 5
⊢ ∅ =
((𝐴 ∖ 𝐶) ∩ 𝐶) |
10 | 9 | uneq2i 3278 |
. . . 4
⊢ (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ∅) = (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ((𝐴 ∖ 𝐶) ∩ 𝐶)) |
11 | 6, 10 | eqtr4i 2194 |
. . 3
⊢ ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) = (((𝐴 ∖ 𝐶) ∩ (V ∖ 𝐵)) ∪ ∅) |
12 | 5, 11 | eqtr4i 2194 |
. 2
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) |
13 | | ddifss 3365 |
. . . . . 6
⊢ 𝐶 ⊆ (V ∖ (V ∖
𝐶)) |
14 | | unss2 3298 |
. . . . . 6
⊢ (𝐶 ⊆ (V ∖ (V ∖
𝐶)) → ((V ∖
𝐵) ∪ 𝐶) ⊆ ((V ∖ 𝐵) ∪ (V ∖ (V ∖ 𝐶)))) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
⊢ ((V
∖ 𝐵) ∪ 𝐶) ⊆ ((V ∖ 𝐵) ∪ (V ∖ (V ∖
𝐶))) |
16 | | indmss 3386 |
. . . . . 6
⊢ ((V
∖ 𝐵) ∪ (V ∖
(V ∖ 𝐶))) ⊆ (V
∖ (𝐵 ∩ (V ∖
𝐶))) |
17 | | invdif 3369 |
. . . . . . 7
⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) |
18 | 17 | difeq2i 3242 |
. . . . . 6
⊢ (V
∖ (𝐵 ∩ (V ∖
𝐶))) = (V ∖ (𝐵 ∖ 𝐶)) |
19 | 16, 18 | sseqtri 3181 |
. . . . 5
⊢ ((V
∖ 𝐵) ∪ (V ∖
(V ∖ 𝐶))) ⊆ (V
∖ (𝐵 ∖ 𝐶)) |
20 | 15, 19 | sstri 3156 |
. . . 4
⊢ ((V
∖ 𝐵) ∪ 𝐶) ⊆ (V ∖ (𝐵 ∖ 𝐶)) |
21 | | sslin 3353 |
. . . 4
⊢ (((V
∖ 𝐵) ∪ 𝐶) ⊆ (V ∖ (𝐵 ∖ 𝐶)) → ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) ⊆ ((𝐴 ∖ 𝐶) ∩ (V ∖ (𝐵 ∖ 𝐶)))) |
22 | 20, 21 | ax-mp 5 |
. . 3
⊢ ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) ⊆ ((𝐴 ∖ 𝐶) ∩ (V ∖ (𝐵 ∖ 𝐶))) |
23 | | invdif 3369 |
. . 3
⊢ ((𝐴 ∖ 𝐶) ∩ (V ∖ (𝐵 ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) |
24 | 22, 23 | sseqtri 3181 |
. 2
⊢ ((𝐴 ∖ 𝐶) ∩ ((V ∖ 𝐵) ∪ 𝐶)) ⊆ ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) |
25 | 12, 24 | eqsstri 3179 |
1
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) ⊆ ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) |