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

Theorem exmidundifim 4130
 Description: Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4129 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.)
Assertion
Ref Expression
exmidundifim (EXMID ↔ ∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦))
Distinct variable group:   𝑥,𝑦

Proof of Theorem exmidundifim
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 undifss 3443 . . . . . . 7 (𝑥𝑦 ↔ (𝑥 ∪ (𝑦𝑥)) ⊆ 𝑦)
21biimpi 119 . . . . . 6 (𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) ⊆ 𝑦)
32adantl 275 . . . . 5 ((EXMID𝑥𝑦) → (𝑥 ∪ (𝑦𝑥)) ⊆ 𝑦)
4 elun1 3243 . . . . . . . . . 10 (𝑧𝑥𝑧 ∈ (𝑥 ∪ (𝑦𝑥)))
54adantl 275 . . . . . . . . 9 (((EXMID𝑧𝑦) ∧ 𝑧𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦𝑥)))
6 simplr 519 . . . . . . . . . . 11 (((EXMID𝑧𝑦) ∧ ¬ 𝑧𝑥) → 𝑧𝑦)
7 simpr 109 . . . . . . . . . . 11 (((EXMID𝑧𝑦) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
86, 7eldifd 3081 . . . . . . . . . 10 (((EXMID𝑧𝑦) ∧ ¬ 𝑧𝑥) → 𝑧 ∈ (𝑦𝑥))
9 elun2 3244 . . . . . . . . . 10 (𝑧 ∈ (𝑦𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦𝑥)))
108, 9syl 14 . . . . . . . . 9 (((EXMID𝑧𝑦) ∧ ¬ 𝑧𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦𝑥)))
11 exmidexmid 4120 . . . . . . . . . . 11 (EXMIDDECID 𝑧𝑥)
12 exmiddc 821 . . . . . . . . . . 11 (DECID 𝑧𝑥 → (𝑧𝑥 ∨ ¬ 𝑧𝑥))
1311, 12syl 14 . . . . . . . . . 10 (EXMID → (𝑧𝑥 ∨ ¬ 𝑧𝑥))
1413adantr 274 . . . . . . . . 9 ((EXMID𝑧𝑦) → (𝑧𝑥 ∨ ¬ 𝑧𝑥))
155, 10, 14mpjaodan 787 . . . . . . . 8 ((EXMID𝑧𝑦) → 𝑧 ∈ (𝑥 ∪ (𝑦𝑥)))
1615ex 114 . . . . . . 7 (EXMID → (𝑧𝑦𝑧 ∈ (𝑥 ∪ (𝑦𝑥))))
1716ssrdv 3103 . . . . . 6 (EXMID𝑦 ⊆ (𝑥 ∪ (𝑦𝑥)))
1817adantr 274 . . . . 5 ((EXMID𝑥𝑦) → 𝑦 ⊆ (𝑥 ∪ (𝑦𝑥)))
193, 18eqssd 3114 . . . 4 ((EXMID𝑥𝑦) → (𝑥 ∪ (𝑦𝑥)) = 𝑦)
2019ex 114 . . 3 (EXMID → (𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦))
2120alrimivv 1847 . 2 (EXMID → ∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦))
22 vex 2689 . . . . . 6 𝑧 ∈ V
23 p0ex 4112 . . . . . 6 {∅} ∈ V
24 sseq12 3122 . . . . . . . 8 ((𝑥 = 𝑧𝑦 = {∅}) → (𝑥𝑦𝑧 ⊆ {∅}))
25 simpl 108 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = {∅}) → 𝑥 = 𝑧)
26 simpr 109 . . . . . . . . . . 11 ((𝑥 = 𝑧𝑦 = {∅}) → 𝑦 = {∅})
2726, 25difeq12d 3195 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = {∅}) → (𝑦𝑥) = ({∅} ∖ 𝑧))
2825, 27uneq12d 3231 . . . . . . . . 9 ((𝑥 = 𝑧𝑦 = {∅}) → (𝑥 ∪ (𝑦𝑥)) = (𝑧 ∪ ({∅} ∖ 𝑧)))
2928, 26eqeq12d 2154 . . . . . . . 8 ((𝑥 = 𝑧𝑦 = {∅}) → ((𝑥 ∪ (𝑦𝑥)) = 𝑦 ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
3024, 29imbi12d 233 . . . . . . 7 ((𝑥 = 𝑧𝑦 = {∅}) → ((𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) ↔ (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
3130spc2gv 2776 . . . . . 6 ((𝑧 ∈ V ∧ {∅} ∈ V) → (∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
3222, 23, 31mp2an 422 . . . . 5 (∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
33 0ex 4055 . . . . . . . 8 ∅ ∈ V
3433snid 3556 . . . . . . 7 ∅ ∈ {∅}
35 eleq2 2203 . . . . . . 7 ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ ∅ ∈ {∅}))
3634, 35mpbiri 167 . . . . . 6 ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → ∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)))
37 eldifn 3199 . . . . . . . 8 (∅ ∈ ({∅} ∖ 𝑧) → ¬ ∅ ∈ 𝑧)
3837orim2i 750 . . . . . . 7 ((∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)) → (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
39 elun 3217 . . . . . . 7 (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ (∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)))
40 df-dc 820 . . . . . . 7 (DECID ∅ ∈ 𝑧 ↔ (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
4138, 39, 403imtr4i 200 . . . . . 6 (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) → DECID ∅ ∈ 𝑧)
4236, 41syl 14 . . . . 5 ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → DECID ∅ ∈ 𝑧)
4332, 42syl6 33 . . . 4 (∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
4443alrimiv 1846 . . 3 (∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
45 df-exmid 4119 . . 3 (EXMID ↔ ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
4644, 45sylibr 133 . 2 (∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦) → EXMID)
4721, 46impbii 125 1 (EXMID ↔ ∀𝑥𝑦(𝑥𝑦 → (𝑥 ∪ (𝑦𝑥)) = 𝑦))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819  ∀wal 1329   = wceq 1331   ∈ wcel 1480  Vcvv 2686   ∖ cdif 3068   ∪ cun 3069   ⊆ wss 3071  ∅c0 3363  {csn 3527  EXMIDwem 4118 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-nul 4054  ax-pow 4098 This theorem depends on definitions:  df-bi 116  df-dc 820  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rab 2425  df-v 2688  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-exmid 4119 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator