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

Theorem exmidn0m 4054
Description: Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.)
Assertion
Ref Expression
exmidn0m (EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
Distinct variable group:   𝑥,𝑦

Proof of Theorem exmidn0m
StepHypRef Expression
1 simpr 109 . . . . 5 ((EXMID ∧ ∃𝑦 𝑦𝑥) → ∃𝑦 𝑦𝑥)
21olcd 691 . . . 4 ((EXMID ∧ ∃𝑦 𝑦𝑥) → (𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
3 notm0 3322 . . . . . . 7 (¬ ∃𝑦 𝑦𝑥𝑥 = ∅)
43biimpi 119 . . . . . 6 (¬ ∃𝑦 𝑦𝑥𝑥 = ∅)
54adantl 272 . . . . 5 ((EXMID ∧ ¬ ∃𝑦 𝑦𝑥) → 𝑥 = ∅)
65orcd 690 . . . 4 ((EXMID ∧ ¬ ∃𝑦 𝑦𝑥) → (𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
7 exmidexmid 4052 . . . . 5 (EXMIDDECID𝑦 𝑦𝑥)
8 exmiddc 785 . . . . 5 (DECID𝑦 𝑦𝑥 → (∃𝑦 𝑦𝑥 ∨ ¬ ∃𝑦 𝑦𝑥))
97, 8syl 14 . . . 4 (EXMID → (∃𝑦 𝑦𝑥 ∨ ¬ ∃𝑦 𝑦𝑥))
102, 6, 9mpjaodan 750 . . 3 (EXMID → (𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
1110alrimiv 1809 . 2 (EXMID → ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
12 orc 671 . . . . . 6 (𝑥 = ∅ → (𝑥 = ∅ ∨ 𝑥 = {∅}))
1312a1d 22 . . . . 5 (𝑥 = ∅ → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
14 sssnm 3620 . . . . . . . 8 (∃𝑦 𝑦𝑥 → (𝑥 ⊆ {∅} ↔ 𝑥 = {∅}))
1514biimpa 291 . . . . . . 7 ((∃𝑦 𝑦𝑥𝑥 ⊆ {∅}) → 𝑥 = {∅})
1615olcd 691 . . . . . 6 ((∃𝑦 𝑦𝑥𝑥 ⊆ {∅}) → (𝑥 = ∅ ∨ 𝑥 = {∅}))
1716ex 114 . . . . 5 (∃𝑦 𝑦𝑥 → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
1813, 17jaoi 674 . . . 4 ((𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥) → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
1918alimi 1396 . . 3 (∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥) → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
20 exmid01 4053 . . 3 (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
2119, 20sylibr 133 . 2 (∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥) → EXMID)
2211, 21impbii 125 1 (EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦𝑥))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 667  DECID wdc 783  wal 1294   = wceq 1296  wex 1433  wss 3013  c0 3302  {csn 3466  EXMIDwem 4050
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-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-nul 3986  ax-pow 4030
This theorem depends on definitions:  df-bi 116  df-dc 784  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rab 2379  df-v 2635  df-dif 3015  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-exmid 4051
This theorem is referenced by:  exmidsssn  4055
  Copyright terms: Public domain W3C validator