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

Theorem en1 8595
 Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
Assertion
Ref Expression
en1 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Distinct variable group:   𝑥,𝐴

Proof of Theorem en1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df1o2 8126 . . . . 5 1o = {∅}
21breq2i 5040 . . . 4 (𝐴 ≈ 1o𝐴 ≈ {∅})
3 bren 8536 . . . 4 (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
42, 3bitri 278 . . 3 (𝐴 ≈ 1o ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
5 f1ocnv 6614 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝑓:{∅}–1-1-onto𝐴)
6 f1ofo 6609 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}–onto𝐴)
7 forn 6579 . . . . . . 7 (𝑓:{∅}–onto𝐴 → ran 𝑓 = 𝐴)
86, 7syl 17 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = 𝐴)
9 f1of 6602 . . . . . . . . 9 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}⟶𝐴)
10 0ex 5177 . . . . . . . . . . 11 ∅ ∈ V
1110fsn2 6889 . . . . . . . . . 10 (𝑓:{∅}⟶𝐴 ↔ ((𝑓‘∅) ∈ 𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩}))
1211simprbi 500 . . . . . . . . 9 (𝑓:{∅}⟶𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
139, 12syl 17 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
1413rneqd 5779 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = ran {⟨∅, (𝑓‘∅)⟩})
1510rnsnop 6053 . . . . . . 7 ran {⟨∅, (𝑓‘∅)⟩} = {(𝑓‘∅)}
1614, 15eqtrdi 2809 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = {(𝑓‘∅)})
178, 16eqtr3d 2795 . . . . 5 (𝑓:{∅}–1-1-onto𝐴𝐴 = {(𝑓‘∅)})
18 fvex 6671 . . . . . 6 (𝑓‘∅) ∈ V
19 sneq 4532 . . . . . . 7 (𝑥 = (𝑓‘∅) → {𝑥} = {(𝑓‘∅)})
2019eqeq2d 2769 . . . . . 6 (𝑥 = (𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(𝑓‘∅)}))
2118, 20spcev 3525 . . . . 5 (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥})
225, 17, 213syl 18 . . . 4 (𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
2322exlimiv 1931 . . 3 (∃𝑓 𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
244, 23sylbi 220 . 2 (𝐴 ≈ 1o → ∃𝑥 𝐴 = {𝑥})
25 vex 3413 . . . . 5 𝑥 ∈ V
2625ensn1 8592 . . . 4 {𝑥} ≈ 1o
27 breq1 5035 . . . 4 (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈ 1o))
2826, 27mpbiri 261 . . 3 (𝐴 = {𝑥} → 𝐴 ≈ 1o)
2928exlimiv 1931 . 2 (∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o)
3024, 29impbii 212 1 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∅c0 4225  {csn 4522  ⟨cop 4528   class class class wbr 5032  ◡ccnv 5523  ran crn 5525  ⟶wf 6331  –onto→wfo 6333  –1-1-onto→wf1o 6334  ‘cfv 6335  1oc1o 8105   ≈ cen 8524 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-1o 8112  df-en 8528 This theorem is referenced by:  en1b  8596  reuen1  8597  en2  8790  card1  9430  pm54.43  9463  hash1elsn  13782  hash1snb  13830  ufildom1  22626  unidifsnel  30405  unidifsnne  30406  funen1cnv  32585  lfuhgr3  32597  snen1g  40605
 Copyright terms: Public domain W3C validator