Theorem ensn1 8969

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7691. (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 5386	. . . 4 ⊢ {⟨𝐴, ∅⟩} ∈ V
2		f1oeq1 6770	. . . 4 ⊢ (𝑓 = {⟨𝐴, ∅⟩} → (𝑓:{𝐴}–1-1-onto→{∅} ↔ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}))
3		ensn1.1	. . . . 5 ⊢ 𝐴 ∈ V
4		0ex 5257	. . . . 5 ⊢ ∅ ∈ V
5	3, 4	f1osn 6822	. . . 4 ⊢ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}
6	1, 2, 5	ceqsexv2d 3496	. . 3 ⊢ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}
7		snex 5386	. . . 4 ⊢ {𝐴} ∈ V
8		snex 5386	. . . 4 ⊢ {∅} ∈ V
9		breng 8904	. . . 4 ⊢ (({𝐴} ∈ V ∧ {∅} ∈ V) → ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}))
10	7, 8, 9	mp2an 692	. . 3 ⊢ ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅})
11	6, 10	mpbir 231	. 2 ⊢ {𝐴} ≈ {∅}
12		df1o2 8418	. 2 ⊢ 1o = {∅}
13	11, 12	breqtrri 5129	1 ⊢ {𝐴} ≈ 1o

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  {csn 4585  ⟨cop 4591   class class class wbr 5102  –1-1-onto→wf1o 6498  1_oc1o 8404   ≈ cen 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-suc 6326  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-1o 8411  df-en 8896

This theorem is referenced by:  ensn1g  8970  en1  8972  sdom1  9166  fodomfiOLD  9257  pm54.43  9930  1nprm  16625  gex1  19497  sylow2a  19525  0frgp  19685  en1top  22847  en2top  22848  t1connperf  23299  ptcmplem2  23916  xrge0tsms2  24700  sconnpi1  35199  setcsnterm  49452