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

Theorem dcdifsnid 6303
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 3605 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 3605 . . 3 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
21adantl 272 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
3 simpr 109 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵)
4 velsn 3483 . . . . . . 7 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
53, 4sylibr 133 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵})
6 elun2 3183 . . . . . 6 (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
75, 6syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
8 simplr 498 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧𝐴)
9 simpr 109 . . . . . . . 8 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵)
109, 4sylnibr 640 . . . . . . 7 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵})
118, 10eldifd 3023 . . . . . 6 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
12 elun1 3182 . . . . . 6 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
1311, 12syl 14 . . . . 5 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
14 simpll 497 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
15 simpr 109 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
16 simplr 498 . . . . . . . 8 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝐵𝐴)
17 equequ1 1652 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1817dcbid 789 . . . . . . . . 9 (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦DECID 𝑧 = 𝑦))
19 eqeq2 2104 . . . . . . . . . 10 (𝑦 = 𝐵 → (𝑧 = 𝑦𝑧 = 𝐵))
2019dcbid 789 . . . . . . . . 9 (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦DECID 𝑧 = 𝐵))
2118, 20rspc2v 2748 . . . . . . . 8 ((𝑧𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2215, 16, 21syl2anc 404 . . . . . . 7 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID 𝑧 = 𝐵))
2314, 22mpd 13 . . . . . 6 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → DECID 𝑧 = 𝐵)
24 exmiddc 785 . . . . . 6 (DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
2523, 24syl 14 . . . . 5 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵))
267, 13, 25mpjaodan 750 . . . 4 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) ∧ 𝑧𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
2726ex 114 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → (𝑧𝐴𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})))
2827ssrdv 3045 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
292, 28eqssd 3056 1 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 667  DECID wdc 783   = wceq 1296  wcel 1445  wral 2370  cdif 3010  cun 3011  wss 3013  {csn 3466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-dc 784  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-v 2635  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472
This theorem is referenced by:  fnsnsplitdc  6304  nndifsnid  6306  fidifsnid  6667  undifdc  6714
  Copyright terms: Public domain W3C validator