Theorem ensn1 8996

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7713. (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 5393	. . . 4 ⊢ {⟨𝐴, ∅⟩} ∈ V
2		f1oeq1 6789	. . . 4 ⊢ (𝑓 = {⟨𝐴, ∅⟩} → (𝑓:{𝐴}–1-1-onto→{∅} ↔ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}))
3		ensn1.1	. . . . 5 ⊢ 𝐴 ∈ V
4		0ex 5254	. . . . 5 ⊢ ∅ ∈ V
5	3, 4	f1osn 6843	. . . 4 ⊢ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}
6	1, 2, 5	ceqsexv2d 3502	. . 3 ⊢ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}
7		snex 5393	. . . 4 ⊢ {𝐴} ∈ V
8		snex 5393	. . . 4 ⊢ {∅} ∈ V
9		breng 8930	. . . 4 ⊢ (({𝐴} ∈ V ∧ {∅} ∈ V) → ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}))
10	7, 8, 9	mp2an 702	. . 3 ⊢ ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅})
11	6, 10	mpbir 233	. 2 ⊢ {𝐴} ≈ {∅}
12		df1o2 8438	. 2 ⊢ 1o = {∅}
13	11, 12	breqtrri 5124	1 ⊢ {𝐴} ≈ 1o

Syntax hints:   ↔ wb 208  ∃wex 1798   ∈ wcel 2141  Vcvv 3453  ∅c0 4283  {csn 4579  ⟨cop 4585   class class class wbr 5097  –1-1-onto→wf1o 6515  1_oc1o 8424   ≈ cen 8918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-suc 6347  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-1o 8431  df-en 8922

This theorem is referenced by:  ensn1g  8997  en1  8999  sdom1  9188  pm54.43  9953  1nprm  16704  gex1  19622  sylow2a  19650  0frgp  19810  en1top  23032  en2top  23033  t1connperf  23484  ptcmplem2  24101  xrge0tsms2  24884  fldlring  33656  sconnpi1  35550  setcsnterm  50072