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

Theorem dcdifsnid 6195
Description: If we remove a single element from a set with decidable equality then put it back in, we end up with the original set. This strengthens difsnss 3557 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
Assertion
Ref Expression
dcdifsnid ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem dcdifsnid
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 difsnss 3557 . . 3 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
21adantl 271 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3 simpr 108 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4 velsn 3439 . . . . . . 7 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
53, 4sylibr 132 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6 elun2 3152 . . . . . 6 (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
75, 6syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8 simplr 497 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧𝐴)
9 simpr 108 . . . . . . . 8 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
109, 4sylnibr 635 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
118, 10eldifd 2994 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12 elun1 3151 . . . . . 6 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
1311, 12syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14 simpll 496 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
15 simpr 108 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
16 simplr 497 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝐵𝐴)
17 equequ1 1640 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1817dcbid 782 . . . . . . . . 9 (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦DECID 𝑧 = 𝑦))
19 eqeq2 2092 . . . . . . . . . 10 (𝑦 = 𝐵 → (𝑧 = 𝑦𝑧 = 𝐵))
2019dcbid 782 . . . . . . . . 9 (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦DECID 𝑧 = 𝐵))
2118, 20rspc2v 2723 . . . . . . . 8 ((𝑧𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2215, 16, 21syl2anc 403 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2314, 22mpd 13 . . . . . 6 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → DECID 𝑧 = 𝐵)
24 exmiddc 778 . . . . . 6 (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
2523, 24syl 14 . . . . 5 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
267, 13, 25mpjaodan 745 . . . 4 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
2726ex 113 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → (𝑧𝐴𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
2827ssrdv 3016 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
292, 28eqssd 3027 1 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wo 662  DECID wdc 776   = wceq 1285  wcel 1434  wral 2353  cdif 2981  cun 2982  wss 2984  {csn 3422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-dc 777  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2614  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-sn 3428
This theorem is referenced by:  nndifsnid  6196  fidifsnid  6517  undifdc  6561
  Copyright terms: Public domain W3C validator