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

 Description: Lemma for enadj 6060. Calculate equality of differences. (Contributed by SF, 25-Feb-2015.)
Assertion
Ref Expression
enadjlem1 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (A {Y}) = (B {X}))

Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 elsni 3757 . . . . . . . . 9 (x {Y} → x = Y)
21necon3ai 2556 . . . . . . . 8 (xY → ¬ x {Y})
32ad2antll 709 . . . . . . 7 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → ¬ x {Y})
4 ssun1 3426 . . . . . . . . . . 11 A (A ∪ {X})
54sseli 3269 . . . . . . . . . 10 (x Ax (A ∪ {X}))
65ad2antrl 708 . . . . . . . . 9 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → x (A ∪ {X}))
7 simpl1 958 . . . . . . . . 9 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → (A ∪ {X}) = (B ∪ {Y}))
86, 7eleqtrd 2429 . . . . . . . 8 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → x (B ∪ {Y}))
9 elun 3220 . . . . . . . 8 (x (B ∪ {Y}) ↔ (x B x {Y}))
108, 9sylib 188 . . . . . . 7 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → (x B x {Y}))
11 orel2 372 . . . . . . 7 x {Y} → ((x B x {Y}) → x B))
123, 10, 11sylc 56 . . . . . 6 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x A xY)) → x B)
1312ex 423 . . . . 5 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x A xY) → x B))
14 simp2l 981 . . . . . . . 8 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ¬ X A)
15 eleq1 2413 . . . . . . . . 9 (x = X → (x AX A))
1615notbid 285 . . . . . . . 8 (x = X → (¬ x A ↔ ¬ X A))
1714, 16syl5ibrcom 213 . . . . . . 7 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x = X → ¬ x A))
1817necon2ad 2564 . . . . . 6 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x AxX))
1918adantrd 454 . . . . 5 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x A xY) → xX))
2013, 19jcad 519 . . . 4 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x A xY) → (x B xX)))
21 eldifsn 3839 . . . 4 (x (A {Y}) ↔ (x A xY))
22 eldifsn 3839 . . . 4 (x (B {X}) ↔ (x B xX))
2320, 21, 223imtr4g 261 . . 3 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x (A {Y}) → x (B {X})))
2423ssrdv 3278 . 2 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (A {Y}) (B {X}))
25 elsni 3757 . . . . . . . . 9 (x {X} → x = X)
2625necon3ai 2556 . . . . . . . 8 (xX → ¬ x {X})
2726ad2antll 709 . . . . . . 7 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → ¬ x {X})
28 ssun1 3426 . . . . . . . . . . 11 B (B ∪ {Y})
2928sseli 3269 . . . . . . . . . 10 (x Bx (B ∪ {Y}))
3029ad2antrl 708 . . . . . . . . 9 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → x (B ∪ {Y}))
31 simpl1 958 . . . . . . . . 9 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → (A ∪ {X}) = (B ∪ {Y}))
3230, 31eleqtrrd 2430 . . . . . . . 8 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → x (A ∪ {X}))
33 elun 3220 . . . . . . . 8 (x (A ∪ {X}) ↔ (x A x {X}))
3432, 33sylib 188 . . . . . . 7 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → (x A x {X}))
35 orel2 372 . . . . . . 7 x {X} → ((x A x {X}) → x A))
3627, 34, 35sylc 56 . . . . . 6 ((((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) (x B xX)) → x A)
3736ex 423 . . . . 5 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x B xX) → x A))
38 simp2r 982 . . . . . . . 8 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ¬ Y B)
39 eleq1 2413 . . . . . . . . 9 (x = Y → (x BY B))
4039notbid 285 . . . . . . . 8 (x = Y → (¬ x B ↔ ¬ Y B))
4138, 40syl5ibrcom 213 . . . . . . 7 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x = Y → ¬ x B))
4241necon2ad 2564 . . . . . 6 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x BxY))
4342adantrd 454 . . . . 5 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x B xX) → xY))
4437, 43jcad 519 . . . 4 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → ((x B xX) → (x A xY)))
4544, 22, 213imtr4g 261 . . 3 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (x (B {X}) → x (A {Y})))
4645ssrdv 3278 . 2 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (B {X}) (A {Y}))
4724, 46eqssd 3289 1 (((A ∪ {X}) = (B ∪ {Y}) X A ¬ Y B) (Y A X B)) → (A {Y}) = (B {X}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516   ∖ cdif 3206   ∪ cun 3207  {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-sn 3741 This theorem is referenced by:  enadj  6060
 Copyright terms: Public domain W3C validator