Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  difdifdirss GIF version

 Description: Distributive law for class difference. In classical logic, as in Exercise 4.8 of [Stoll] p. 16, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
Assertion
Ref Expression
difdifdirss ((AB) ∖ 𝐶) ⊆ ((A𝐶) ∖ (B𝐶))

StepHypRef Expression
1 dif32 3194 . . . . 5 ((AB) ∖ 𝐶) = ((A𝐶) ∖ B)
2 invdif 3173 . . . . 5 ((A𝐶) ∩ (V ∖ B)) = ((A𝐶) ∖ B)
31, 2eqtr4i 2060 . . . 4 ((AB) ∖ 𝐶) = ((A𝐶) ∩ (V ∖ B))
4 un0 3245 . . . 4 (((A𝐶) ∩ (V ∖ B)) ∪ ∅) = ((A𝐶) ∩ (V ∖ B))
53, 4eqtr4i 2060 . . 3 ((AB) ∖ 𝐶) = (((A𝐶) ∩ (V ∖ B)) ∪ ∅)
6 indi 3178 . . . 4 ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶)) = (((A𝐶) ∩ (V ∖ B)) ∪ ((A𝐶) ∩ 𝐶))
7 disjdif 3290 . . . . . 6 (𝐶 ∩ (A𝐶)) = ∅
8 incom 3123 . . . . . 6 (𝐶 ∩ (A𝐶)) = ((A𝐶) ∩ 𝐶)
97, 8eqtr3i 2059 . . . . 5 ∅ = ((A𝐶) ∩ 𝐶)
109uneq2i 3088 . . . 4 (((A𝐶) ∩ (V ∖ B)) ∪ ∅) = (((A𝐶) ∩ (V ∖ B)) ∪ ((A𝐶) ∩ 𝐶))
116, 10eqtr4i 2060 . . 3 ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶)) = (((A𝐶) ∩ (V ∖ B)) ∪ ∅)
125, 11eqtr4i 2060 . 2 ((AB) ∖ 𝐶) = ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶))
13 ddifss 3169 . . . . . 6 𝐶 ⊆ (V ∖ (V ∖ 𝐶))
14 unss2 3108 . . . . . 6 (𝐶 ⊆ (V ∖ (V ∖ 𝐶)) → ((V ∖ B) ∪ 𝐶) ⊆ ((V ∖ B) ∪ (V ∖ (V ∖ 𝐶))))
1513, 14ax-mp 7 . . . . 5 ((V ∖ B) ∪ 𝐶) ⊆ ((V ∖ B) ∪ (V ∖ (V ∖ 𝐶)))
16 indmss 3190 . . . . . 6 ((V ∖ B) ∪ (V ∖ (V ∖ 𝐶))) ⊆ (V ∖ (B ∩ (V ∖ 𝐶)))
17 invdif 3173 . . . . . . 7 (B ∩ (V ∖ 𝐶)) = (B𝐶)
1817difeq2i 3053 . . . . . 6 (V ∖ (B ∩ (V ∖ 𝐶))) = (V ∖ (B𝐶))
1916, 18sseqtri 2971 . . . . 5 ((V ∖ B) ∪ (V ∖ (V ∖ 𝐶))) ⊆ (V ∖ (B𝐶))
2015, 19sstri 2948 . . . 4 ((V ∖ B) ∪ 𝐶) ⊆ (V ∖ (B𝐶))
21 sslin 3157 . . . 4 (((V ∖ B) ∪ 𝐶) ⊆ (V ∖ (B𝐶)) → ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶)) ⊆ ((A𝐶) ∩ (V ∖ (B𝐶))))
2220, 21ax-mp 7 . . 3 ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶)) ⊆ ((A𝐶) ∩ (V ∖ (B𝐶)))
23 invdif 3173 . . 3 ((A𝐶) ∩ (V ∖ (B𝐶))) = ((A𝐶) ∖ (B𝐶))
2422, 23sseqtri 2971 . 2 ((A𝐶) ∩ ((V ∖ B) ∪ 𝐶)) ⊆ ((A𝐶) ∖ (B𝐶))
2512, 24eqsstri 2969 1 ((AB) ∖ 𝐶) ⊆ ((A𝐶) ∖ (B𝐶))
 Colors of variables: wff set class Syntax hints:  Vcvv 2551   ∖ cdif 2908   ∪ cun 2909   ∩ cin 2910   ⊆ wss 2911  ∅c0 3218 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rab 2309  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator