Theorem ensn1 9035

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

Syntax hints:   ↔ wb 206  ∃wex 1779   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  {csn 4601  ⟨cop 4607   class class class wbr 5119  –1-1-onto→wf1o 6530  1_oc1o 8473   ≈ cen 8956

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-suc 6358  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-1o 8480  df-en 8960

This theorem is referenced by:  ensn1g  9036  en1  9038  sdom1  9250  fodomfiOLD  9342  pm54.43  10015  1nprm  16698  gex1  19572  sylow2a  19600  0frgp  19760  en1top  22922  en2top  22923  t1connperf  23374  ptcmplem2  23991  xrge0tsms2  24775  sconnpi1  35261  setcsnterm  49375