Theorem ensn1 8961

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7682. (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 5376	. . . 4 ⊢ {⟨𝐴, ∅⟩} ∈ V
2		f1oeq1 6762	. . . 4 ⊢ (𝑓 = {⟨𝐴, ∅⟩} → (𝑓:{𝐴}–1-1-onto→{∅} ↔ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}))
3		ensn1.1	. . . . 5 ⊢ 𝐴 ∈ V
4		0ex 5242	. . . . 5 ⊢ ∅ ∈ V
5	3, 4	f1osn 6815	. . . 4 ⊢ {⟨𝐴, ∅⟩}:{𝐴}–1-1-onto→{∅}
6	1, 2, 5	ceqsexv2d 3480	. . 3 ⊢ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}
7		snex 5376	. . . 4 ⊢ {𝐴} ∈ V
8		snex 5376	. . . 4 ⊢ {∅} ∈ V
9		breng 8895	. . . 4 ⊢ (({𝐴} ∈ V ∧ {∅} ∈ V) → ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅}))
10	7, 8, 9	mp2an 693	. . 3 ⊢ ({𝐴} ≈ {∅} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{∅})
11	6, 10	mpbir 231	. 2 ⊢ {𝐴} ≈ {∅}
12		df1o2 8405	. 2 ⊢ 1o = {∅}
13	11, 12	breqtrri 5113	1 ⊢ {𝐴} ≈ 1o

Syntax hints:   ↔ wb 206  ∃wex 1781   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  {csn 4568  ⟨cop 4574   class class class wbr 5086  –1-1-onto→wf1o 6491  1_oc1o 8391   ≈ cen 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-suc 6323  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-1o 8398  df-en 8887

This theorem is referenced by:  ensn1g  8962  en1  8964  sdom1  9153  fodomfiOLD  9233  pm54.43  9916  1nprm  16639  gex1  19557  sylow2a  19585  0frgp  19745  en1top  22959  en2top  22960  t1connperf  23411  ptcmplem2  24028  xrge0tsms2  24811  sconnpi1  35437  setcsnterm  49977