MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sdom2en01 Structured version   Visualization version   GIF version

Theorem sdom2en01 9718
Description: A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014.)
Assertion
Ref Expression
sdom2en01 (𝐴 ≺ 2o ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o))

Proof of Theorem sdom2en01
StepHypRef Expression
1 onfin2 8704 . . . . 5 ω = (On ∩ Fin)
2 inss2 4210 . . . . 5 (On ∩ Fin) ⊆ Fin
31, 2eqsstri 4005 . . . 4 ω ⊆ Fin
4 2onn 8261 . . . 4 2o ∈ ω
53, 4sselii 3968 . . 3 2o ∈ Fin
6 sdomdom 8531 . . 3 (𝐴 ≺ 2o𝐴 ≼ 2o)
7 domfi 8733 . . 3 ((2o ∈ Fin ∧ 𝐴 ≼ 2o) → 𝐴 ∈ Fin)
85, 6, 7sylancr 587 . 2 (𝐴 ≺ 2o𝐴 ∈ Fin)
9 id 22 . . . 4 (𝐴 = ∅ → 𝐴 = ∅)
10 0fin 8740 . . . 4 ∅ ∈ Fin
119, 10syl6eqel 2926 . . 3 (𝐴 = ∅ → 𝐴 ∈ Fin)
12 1onn 8260 . . . . 5 1o ∈ ω
133, 12sselii 3968 . . . 4 1o ∈ Fin
14 enfi 8728 . . . 4 (𝐴 ≈ 1o → (𝐴 ∈ Fin ↔ 1o ∈ Fin))
1513, 14mpbiri 259 . . 3 (𝐴 ≈ 1o𝐴 ∈ Fin)
1611, 15jaoi 853 . 2 ((𝐴 = ∅ ∨ 𝐴 ≈ 1o) → 𝐴 ∈ Fin)
17 df2o3 8113 . . . . . 6 2o = {∅, 1o}
1817eleq2i 2909 . . . . 5 ((card‘𝐴) ∈ 2o ↔ (card‘𝐴) ∈ {∅, 1o})
19 fvex 6682 . . . . . 6 (card‘𝐴) ∈ V
2019elpr 4587 . . . . 5 ((card‘𝐴) ∈ {∅, 1o} ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1o))
2118, 20bitri 276 . . . 4 ((card‘𝐴) ∈ 2o ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1o))
2221a1i 11 . . 3 (𝐴 ∈ Fin → ((card‘𝐴) ∈ 2o ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1o)))
23 cardnn 9386 . . . . . 6 (2o ∈ ω → (card‘2o) = 2o)
244, 23ax-mp 5 . . . . 5 (card‘2o) = 2o
2524eleq2i 2909 . . . 4 ((card‘𝐴) ∈ (card‘2o) ↔ (card‘𝐴) ∈ 2o)
26 finnum 9371 . . . . 5 (𝐴 ∈ Fin → 𝐴 ∈ dom card)
27 2on 8107 . . . . . 6 2o ∈ On
28 onenon 9372 . . . . . 6 (2o ∈ On → 2o ∈ dom card)
2927, 28ax-mp 5 . . . . 5 2o ∈ dom card
30 cardsdom2 9411 . . . . 5 ((𝐴 ∈ dom card ∧ 2o ∈ dom card) → ((card‘𝐴) ∈ (card‘2o) ↔ 𝐴 ≺ 2o))
3126, 29, 30sylancl 586 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) ∈ (card‘2o) ↔ 𝐴 ≺ 2o))
3225, 31syl5bbr 286 . . 3 (𝐴 ∈ Fin → ((card‘𝐴) ∈ 2o𝐴 ≺ 2o))
33 cardnueq0 9387 . . . . 5 (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
3426, 33syl 17 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
35 cardnn 9386 . . . . . . 7 (1o ∈ ω → (card‘1o) = 1o)
3612, 35ax-mp 5 . . . . . 6 (card‘1o) = 1o
3736eqeq2i 2839 . . . . 5 ((card‘𝐴) = (card‘1o) ↔ (card‘𝐴) = 1o)
38 finnum 9371 . . . . . . 7 (1o ∈ Fin → 1o ∈ dom card)
3913, 38ax-mp 5 . . . . . 6 1o ∈ dom card
40 carden2 9410 . . . . . 6 ((𝐴 ∈ dom card ∧ 1o ∈ dom card) → ((card‘𝐴) = (card‘1o) ↔ 𝐴 ≈ 1o))
4126, 39, 40sylancl 586 . . . . 5 (𝐴 ∈ Fin → ((card‘𝐴) = (card‘1o) ↔ 𝐴 ≈ 1o))
4237, 41syl5bbr 286 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) = 1o𝐴 ≈ 1o))
4334, 42orbi12d 914 . . 3 (𝐴 ∈ Fin → (((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1o) ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o)))
4422, 32, 433bitr3d 310 . 2 (𝐴 ∈ Fin → (𝐴 ≺ 2o ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o)))
458, 16, 44pm5.21nii 380 1 (𝐴 ≺ 2o ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wo 843   = wceq 1530  wcel 2107  cin 3939  c0 4295  {cpr 4566   class class class wbr 5063  dom cdm 5554  Oncon0 6190  cfv 6354  ωcom 7573  1oc1o 8091  2oc2o 8092  cen 8500  cdom 8501  csdm 8502  Fincfn 8503  cardccrd 9358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-om 7574  df-1o 8098  df-2o 8099  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-card 9362
This theorem is referenced by:  fin56  9809  en2top  21528
  Copyright terms: Public domain W3C validator