Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ss1oel2o GIF version

Theorem ss1oel2o 13988
Description: Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4182 which more directly illustrates the contrast with el2oss1o 6420. (Contributed by Jim Kingdon, 8-Aug-2022.)
Assertion
Ref Expression
ss1oel2o (EXMID ↔ ∀𝑥(𝑥 ⊆ 1o𝑥 ∈ 2o))

Proof of Theorem ss1oel2o
StepHypRef Expression
1 exmid01 4182 . 2 (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
2 df1o2 6406 . . . . 5 1o = {∅}
32sseq2i 3174 . . . 4 (𝑥 ⊆ 1o𝑥 ⊆ {∅})
4 df2o2 6408 . . . . . 6 2o = {∅, {∅}}
54eleq2i 2237 . . . . 5 (𝑥 ∈ 2o𝑥 ∈ {∅, {∅}})
6 vex 2733 . . . . . 6 𝑥 ∈ V
76elpr 3602 . . . . 5 (𝑥 ∈ {∅, {∅}} ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))
85, 7bitri 183 . . . 4 (𝑥 ∈ 2o ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))
93, 8imbi12i 238 . . 3 ((𝑥 ⊆ 1o𝑥 ∈ 2o) ↔ (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
109albii 1463 . 2 (∀𝑥(𝑥 ⊆ 1o𝑥 ∈ 2o) ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
111, 10bitr4i 186 1 (EXMID ↔ ∀𝑥(𝑥 ⊆ 1o𝑥 ∈ 2o))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wo 703  wal 1346   = wceq 1348  wcel 2141  wss 3121  c0 3414  {csn 3581  {cpr 3582  EXMIDwem 4178  1oc1o 6386  2oc2o 6387
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-nul 4113
This theorem depends on definitions:  df-bi 116  df-dc 830  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-sn 3587  df-pr 3588  df-exmid 4179  df-suc 4354  df-1o 6393  df-2o 6394
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator