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

Theorem dcdifsnid 6522
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 3752 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 3752 . . 3 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
21adantl 277 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3 simpr 110 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4 velsn 3623 . . . . . . 7 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
53, 4sylibr 134 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6 elun2 3317 . . . . . 6 (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
75, 6syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8 simplr 528 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧𝐴)
9 simpr 110 . . . . . . . 8 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
109, 4sylnibr 678 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
118, 10eldifd 3153 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12 elun1 3316 . . . . . 6 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
1311, 12syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14 simpll 527 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
15 simpr 110 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
16 simplr 528 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝐵𝐴)
17 equequ1 1722 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1817dcbid 839 . . . . . . . . 9 (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦DECID 𝑧 = 𝑦))
19 eqeq2 2198 . . . . . . . . . 10 (𝑦 = 𝐵 → (𝑧 = 𝑦𝑧 = 𝐵))
2019dcbid 839 . . . . . . . . 9 (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦DECID 𝑧 = 𝐵))
2118, 20rspc2v 2868 . . . . . . . 8 ((𝑧𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2215, 16, 21syl2anc 411 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2314, 22mpd 13 . . . . . 6 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → DECID 𝑧 = 𝐵)
24 exmiddc 837 . . . . . 6 (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
2523, 24syl 14 . . . . 5 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
267, 13, 25mpjaodan 799 . . . 4 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
2726ex 115 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → (𝑧𝐴𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
2827ssrdv 3175 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
292, 28eqssd 3186 1 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 709  DECID wdc 835   = wceq 1363  wcel 2159  wral 2467  cdif 3140  cun 3141  wss 3143  {csn 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170
This theorem depends on definitions:  df-bi 117  df-dc 836  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ral 2472  df-v 2753  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-sn 3612
This theorem is referenced by:  fnsnsplitdc  6523  nndifsnid  6525  fidifsnid  6888  undifdc  6940
  Copyright terms: Public domain W3C validator