Theorem ensn1 8958

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7678. (Revised by BTernaryTau, 23-Sep-2024.)

Hypothesis

Ref	Expression
ensn1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
ensn1	⊢ {𝐴} ≈ 1o

Proof of Theorem ensn1

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 5368	. . . 4 ⊢ {⟨𝐴, ∅⟩} ∈ V
2		f1oeq1 6755	. . . 4 ⊢ (𝑓 = {⟨𝐴, ∅⟩} → (𝑓:{𝐴}–1-1-onto→{∅} ↔ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}))
3		ensn1.1	. . . . 5 ⊢ 𝐴 ∈ V
4		0ex 5229	. . . . 5 ⊢ ∅ ∈ V
5	3, 4	f1osn 6808	. . . 4 ⊢ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}
6	1, 2, 5	ceqsexv2d 3480	. . 3 ⊢ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}
7		snex 5368	. . . 4 ⊢ {𝐴} ∈ V
8		snex 5368	. . . 4 ⊢ {∅} ∈ V
9		breng 8892	. . . 4 ⊢ (({𝐴} ∈ V ∧ {∅} ∈ V) → ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}))
10	7, 8, 9	mp2an 698	. . 3 ⊢ ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅})
11	6, 10	mpbir 232	. 2 ⊢ {𝐴} ≈ {∅}
12		df1o2 8402	. 2 ⊢ 1o = {∅}
13	11, 12	breqtrri 5099	1 ⊢ {𝐴} ≈ 1o

Syntax hints:   ↔ wb 207  ∃wex 1786   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  {csn 4555  ⟨cop 4561   class class class wbr 5072  –1-1-onto→wf1o 6484  1_oc1o 8388   ≈ cen 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-suc 6316  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-1o 8395  df-en 8884

This theorem is referenced by:  ensn1g  8959  en1  8961  sdom1  9150  fodomfiOLD  9230  pm54.43  9916  1nprm  16639  gex1  19557  sylow2a  19585  0frgp  19745  en1top  22967  en2top  22968  t1connperf  23419  ptcmplem2  24036  xrge0tsms2  24819  sconnpi1  35467  setcsnterm  49980