New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nnsucelrlem3 GIF version

Theorem nnsucelrlem3 4426
 Description: Lemma for nnsucelr 4428. Rearrange union and difference for a particular group of classes. (Contributed by SF, 15-Jan-2015.)
Hypothesis
Ref Expression
nnsucelrlem3.1 X V
Assertion
Ref Expression
nnsucelrlem3 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → B = ((A {Y}) ∪ {X}))

Proof of Theorem nnsucelrlem3
StepHypRef Expression
1 indir 3503 . . . . 5 ((B ∪ {Y}) ∩ ∼ {Y}) = ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y}))
2 df-dif 3215 . . . . . . . 8 (B {Y}) = (B ∩ ∼ {Y})
32eqcomi 2357 . . . . . . 7 (B ∩ ∼ {Y}) = (B {Y})
4 incompl 4073 . . . . . . 7 ({Y} ∩ ∼ {Y}) =
53, 4uneq12i 3416 . . . . . 6 ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y})) = ((B {Y}) ∪ )
6 un0 3575 . . . . . 6 ((B {Y}) ∪ ) = (B {Y})
75, 6eqtri 2373 . . . . 5 ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y})) = (B {Y})
81, 7eqtri 2373 . . . 4 ((B ∪ {Y}) ∩ ∼ {Y}) = (B {Y})
9 difsn 3845 . . . . 5 Y B → (B {Y}) = B)
1093ad2ant3 978 . . . 4 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → (B {Y}) = B)
118, 10syl5req 2398 . . 3 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → B = ((B ∪ {Y}) ∩ ∼ {Y}))
12 simp2 956 . . . 4 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → (A ∪ {X}) = (B ∪ {Y}))
13 df-ne 2518 . . . . . . . 8 (XY ↔ ¬ X = Y)
1413biimpi 186 . . . . . . 7 (XY → ¬ X = Y)
15143ad2ant1 976 . . . . . 6 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → ¬ X = Y)
16 nnsucelrlem3.1 . . . . . . . . 9 X V
1716elcompl 3225 . . . . . . . 8 (X ∼ {Y} ↔ ¬ X {Y})
1816elsnc 3756 . . . . . . . 8 (X {Y} ↔ X = Y)
1917, 18xchbinx 301 . . . . . . 7 (X ∼ {Y} ↔ ¬ X = Y)
2016snss 3838 . . . . . . 7 (X ∼ {Y} ↔ {X} ∼ {Y})
2119, 20bitr3i 242 . . . . . 6 X = Y ↔ {X} ∼ {Y})
2215, 21sylib 188 . . . . 5 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → {X} ∼ {Y})
23 ssequn2 3436 . . . . 5 ({X} ∼ {Y} ↔ ( ∼ {Y} ∪ {X}) = ∼ {Y})
2422, 23sylib 188 . . . 4 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → ( ∼ {Y} ∪ {X}) = ∼ {Y})
2512, 24ineq12d 3458 . . 3 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X})) = ((B ∪ {Y}) ∩ ∼ {Y}))
2611, 25eqtr4d 2388 . 2 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → B = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X})))
27 df-dif 3215 . . . 4 (A {Y}) = (A ∩ ∼ {Y})
2827uneq1i 3414 . . 3 ((A {Y}) ∪ {X}) = ((A ∩ ∼ {Y}) ∪ {X})
29 undir 3504 . . 3 ((A ∩ ∼ {Y}) ∪ {X}) = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X}))
3028, 29eqtri 2373 . 2 ((A {Y}) ∪ {X}) = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X}))
3126, 30syl6eqr 2403 1 ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → B = ((A {Y}) ∪ {X}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊆ wss 3257  ∅c0 3550  {csn 3737 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741 This theorem is referenced by:  nnsucelr  4428
 Copyright terms: Public domain W3C validator