Theorem ensn1 8954

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

Syntax hints:   ↔ wb 206  ∃wex 1780   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  {csn 4577  ⟨cop 4583   class class class wbr 5095  –1-1-onto→wf1o 6488  1_oc1o 8387   ≈ cen 8876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-suc 6320  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-1o 8394  df-en 8880

This theorem is referenced by:  ensn1g  8955  en1  8957  sdom1  9145  fodomfiOLD  9225  pm54.43  9905  1nprm  16597  gex1  19511  sylow2a  19539  0frgp  19699  en1top  22919  en2top  22920  t1connperf  23371  ptcmplem2  23988  xrge0tsms2  24771  sconnpi1  35355  setcsnterm  49651