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

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

Proof of Theorem sdom2en01
StepHypRef Expression
1 onfin2 8137 . . . . 5 ω = (On ∩ Fin)
2 inss2 3826 . . . . 5 (On ∩ Fin) ⊆ Fin
31, 2eqsstri 3627 . . . 4 ω ⊆ Fin
4 2onn 7705 . . . 4 2𝑜 ∈ ω
53, 4sselii 3592 . . 3 2𝑜 ∈ Fin
6 sdomdom 7968 . . 3 (𝐴 ≺ 2𝑜𝐴 ≼ 2𝑜)
7 domfi 8166 . . 3 ((2𝑜 ∈ Fin ∧ 𝐴 ≼ 2𝑜) → 𝐴 ∈ Fin)
85, 6, 7sylancr 694 . 2 (𝐴 ≺ 2𝑜𝐴 ∈ Fin)
9 id 22 . . . 4 (𝐴 = ∅ → 𝐴 = ∅)
10 0fin 8173 . . . 4 ∅ ∈ Fin
119, 10syl6eqel 2707 . . 3 (𝐴 = ∅ → 𝐴 ∈ Fin)
12 1onn 7704 . . . . 5 1𝑜 ∈ ω
133, 12sselii 3592 . . . 4 1𝑜 ∈ Fin
14 enfi 8161 . . . 4 (𝐴 ≈ 1𝑜 → (𝐴 ∈ Fin ↔ 1𝑜 ∈ Fin))
1513, 14mpbiri 248 . . 3 (𝐴 ≈ 1𝑜𝐴 ∈ Fin)
1611, 15jaoi 394 . 2 ((𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜) → 𝐴 ∈ Fin)
17 df2o3 7558 . . . . . 6 2𝑜 = {∅, 1𝑜}
1817eleq2i 2691 . . . . 5 ((card‘𝐴) ∈ 2𝑜 ↔ (card‘𝐴) ∈ {∅, 1𝑜})
19 fvex 6188 . . . . . 6 (card‘𝐴) ∈ V
2019elpr 4189 . . . . 5 ((card‘𝐴) ∈ {∅, 1𝑜} ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1𝑜))
2118, 20bitri 264 . . . 4 ((card‘𝐴) ∈ 2𝑜 ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1𝑜))
2221a1i 11 . . 3 (𝐴 ∈ Fin → ((card‘𝐴) ∈ 2𝑜 ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1𝑜)))
23 cardnn 8774 . . . . . 6 (2𝑜 ∈ ω → (card‘2𝑜) = 2𝑜)
244, 23ax-mp 5 . . . . 5 (card‘2𝑜) = 2𝑜
2524eleq2i 2691 . . . 4 ((card‘𝐴) ∈ (card‘2𝑜) ↔ (card‘𝐴) ∈ 2𝑜)
26 finnum 8759 . . . . 5 (𝐴 ∈ Fin → 𝐴 ∈ dom card)
27 2on 7553 . . . . . 6 2𝑜 ∈ On
28 onenon 8760 . . . . . 6 (2𝑜 ∈ On → 2𝑜 ∈ dom card)
2927, 28ax-mp 5 . . . . 5 2𝑜 ∈ dom card
30 cardsdom2 8799 . . . . 5 ((𝐴 ∈ dom card ∧ 2𝑜 ∈ dom card) → ((card‘𝐴) ∈ (card‘2𝑜) ↔ 𝐴 ≺ 2𝑜))
3126, 29, 30sylancl 693 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) ∈ (card‘2𝑜) ↔ 𝐴 ≺ 2𝑜))
3225, 31syl5bbr 274 . . 3 (𝐴 ∈ Fin → ((card‘𝐴) ∈ 2𝑜𝐴 ≺ 2𝑜))
33 cardnueq0 8775 . . . . 5 (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
3426, 33syl 17 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
35 cardnn 8774 . . . . . . 7 (1𝑜 ∈ ω → (card‘1𝑜) = 1𝑜)
3612, 35ax-mp 5 . . . . . 6 (card‘1𝑜) = 1𝑜
3736eqeq2i 2632 . . . . 5 ((card‘𝐴) = (card‘1𝑜) ↔ (card‘𝐴) = 1𝑜)
38 finnum 8759 . . . . . . 7 (1𝑜 ∈ Fin → 1𝑜 ∈ dom card)
3913, 38ax-mp 5 . . . . . 6 1𝑜 ∈ dom card
40 carden2 8798 . . . . . 6 ((𝐴 ∈ dom card ∧ 1𝑜 ∈ dom card) → ((card‘𝐴) = (card‘1𝑜) ↔ 𝐴 ≈ 1𝑜))
4126, 39, 40sylancl 693 . . . . 5 (𝐴 ∈ Fin → ((card‘𝐴) = (card‘1𝑜) ↔ 𝐴 ≈ 1𝑜))
4237, 41syl5bbr 274 . . . 4 (𝐴 ∈ Fin → ((card‘𝐴) = 1𝑜𝐴 ≈ 1𝑜))
4334, 42orbi12d 745 . . 3 (𝐴 ∈ Fin → (((card‘𝐴) = ∅ ∨ (card‘𝐴) = 1𝑜) ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜)))
4422, 32, 433bitr3d 298 . 2 (𝐴 ∈ Fin → (𝐴 ≺ 2𝑜 ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜)))
458, 16, 44pm5.21nii 368 1 (𝐴 ≺ 2𝑜 ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383   = wceq 1481  wcel 1988  cin 3566  c0 3907  {cpr 4170   class class class wbr 4644  dom cdm 5104  Oncon0 5711  cfv 5876  ωcom 7050  1𝑜c1o 7538  2𝑜c2o 7539  cen 7937  cdom 7938  csdm 7939  Fincfn 7940  cardccrd 8746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-om 7051  df-1o 7545  df-2o 7546  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750
This theorem is referenced by:  fin56  9200  en2top  20770
  Copyright terms: Public domain W3C validator