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

Theorem en1 9062
Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) Avoid ax-un 7753. (Revised by BTernaryTau, 23-Sep-2024.)
Assertion
Ref Expression
en1 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Distinct variable group:   𝑥,𝐴

Proof of Theorem en1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df1o2 8511 . . . . 5 1o = {∅}
21breq2i 5155 . . . 4 (𝐴 ≈ 1o𝐴 ≈ {∅})
3 encv 8991 . . . . . 6 (𝐴 ≈ {∅} → (𝐴 ∈ V ∧ {∅} ∈ V))
4 breng 8992 . . . . . 6 ((𝐴 ∈ V ∧ {∅} ∈ V) → (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅}))
53, 4syl 17 . . . . 5 (𝐴 ≈ {∅} → (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅}))
65ibi 267 . . . 4 (𝐴 ≈ {∅} → ∃𝑓 𝑓:𝐴1-1-onto→{∅})
72, 6sylbi 217 . . 3 (𝐴 ≈ 1o → ∃𝑓 𝑓:𝐴1-1-onto→{∅})
8 f1ocnv 6860 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝑓:{∅}–1-1-onto𝐴)
9 f1ofo 6855 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}–onto𝐴)
10 forn 6823 . . . . . . 7 (𝑓:{∅}–onto𝐴 → ran 𝑓 = 𝐴)
119, 10syl 17 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = 𝐴)
12 f1of 6848 . . . . . . . . 9 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}⟶𝐴)
13 0ex 5312 . . . . . . . . . . 11 ∅ ∈ V
1413fsn2 7155 . . . . . . . . . 10 (𝑓:{∅}⟶𝐴 ↔ ((𝑓‘∅) ∈ 𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩}))
1514simprbi 496 . . . . . . . . 9 (𝑓:{∅}⟶𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
1612, 15syl 17 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
1716rneqd 5951 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = ran {⟨∅, (𝑓‘∅)⟩})
1813rnsnop 6245 . . . . . . 7 ran {⟨∅, (𝑓‘∅)⟩} = {(𝑓‘∅)}
1917, 18eqtrdi 2790 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = {(𝑓‘∅)})
2011, 19eqtr3d 2776 . . . . 5 (𝑓:{∅}–1-1-onto𝐴𝐴 = {(𝑓‘∅)})
21 fvex 6919 . . . . . 6 (𝑓‘∅) ∈ V
22 sneq 4640 . . . . . . 7 (𝑥 = (𝑓‘∅) → {𝑥} = {(𝑓‘∅)})
2322eqeq2d 2745 . . . . . 6 (𝑥 = (𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(𝑓‘∅)}))
2421, 23spcev 3605 . . . . 5 (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥})
258, 20, 243syl 18 . . . 4 (𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
2625exlimiv 1927 . . 3 (∃𝑓 𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
277, 26syl 17 . 2 (𝐴 ≈ 1o → ∃𝑥 𝐴 = {𝑥})
28 vex 3481 . . . . 5 𝑥 ∈ V
2928ensn1 9059 . . . 4 {𝑥} ≈ 1o
30 breq1 5150 . . . 4 (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈ 1o))
3129, 30mpbiri 258 . . 3 (𝐴 = {𝑥} → 𝐴 ≈ 1o)
3231exlimiv 1927 . 2 (∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o)
3327, 32impbii 209 1 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1536  wex 1775  wcel 2105  Vcvv 3477  c0 4338  {csn 4630  cop 4636   class class class wbr 5147  ccnv 5687  ran crn 5689  wf 6558  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  1oc1o 8497  cen 8980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-1o 8504  df-en 8984
This theorem is referenced by:  en1b  9063  reuen1  9064  en1eqsn  9305  en2  9312  card1  10005  pm54.43  10038  hash1elsn  14406  hash1snb  14454  ufildom1  23949  unidifsnel  32560  unidifsnne  32561  funen1cnv  35080  lfuhgr3  35103  snen1g  43513
  Copyright terms: Public domain W3C validator