Theorem en1 8595

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)

Assertion

Ref	Expression
en1	⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})

Distinct variable group:   𝑥,𝐴

Proof of Theorem en1

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df1o2 8126	. . . . 5 ⊢ 1o = {∅}
2	1	breq2i 5040	. . . 4 ⊢ (𝐴 ≈ 1o ↔ 𝐴 ≈ {∅})
3		bren 8536	. . . 4 ⊢ (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴–1-1-onto→{∅})
4	2, 3	bitri 278	. . 3 ⊢ (𝐴 ≈ 1o ↔ ∃𝑓 𝑓:𝐴–1-1-onto→{∅})
5		f1ocnv 6614	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→{∅} → ◡𝑓:{∅}–1-1-onto→𝐴)
6		f1ofo 6609	. . . . . . 7 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}–onto→𝐴)
7		forn 6579	. . . . . . 7 ⊢ (◡𝑓:{∅}–onto→𝐴 → ran ◡𝑓 = 𝐴)
8	6, 7	syl 17	. . . . . 6 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = 𝐴)
9		f1of 6602	. . . . . . . . 9 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓:{∅}⟶𝐴)
10		0ex 5177	. . . . . . . . . . 11 ⊢ ∅ ∈ V
11	10	fsn2 6889	. . . . . . . . . 10 ⊢ (◡𝑓:{∅}⟶𝐴 ↔ ((◡𝑓‘∅) ∈ 𝐴 ∧ ◡𝑓 = {⟨∅, (◡𝑓‘∅)⟩}))
12	11	simprbi 500	. . . . . . . . 9 ⊢ (◡𝑓:{∅}⟶𝐴 → ◡𝑓 = {⟨∅, (◡𝑓‘∅)⟩})
13	9, 12	syl 17	. . . . . . . 8 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ◡𝑓 = {⟨∅, (◡𝑓‘∅)⟩})
14	13	rneqd 5779	. . . . . . 7 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = ran {⟨∅, (◡𝑓‘∅)⟩})
15	10	rnsnop 6053	. . . . . . 7 ⊢ ran {⟨∅, (◡𝑓‘∅)⟩} = {(◡𝑓‘∅)}
16	14, 15	eqtrdi 2809	. . . . . 6 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → ran ◡𝑓 = {(◡𝑓‘∅)})
17	8, 16	eqtr3d 2795	. . . . 5 ⊢ (◡𝑓:{∅}–1-1-onto→𝐴 → 𝐴 = {(◡𝑓‘∅)})
18		fvex 6671	. . . . . 6 ⊢ (◡𝑓‘∅) ∈ V
19		sneq 4532	. . . . . . 7 ⊢ (𝑥 = (◡𝑓‘∅) → {𝑥} = {(◡𝑓‘∅)})
20	19	eqeq2d 2769	. . . . . 6 ⊢ (𝑥 = (◡𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(◡𝑓‘∅)}))
21	18, 20	spcev 3525	. . . . 5 ⊢ (𝐴 = {(◡𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥})
22	5, 17, 21	3syl 18	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
23	22	exlimiv 1931	. . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
24	4, 23	sylbi 220	. 2 ⊢ (𝐴 ≈ 1o → ∃𝑥 𝐴 = {𝑥})
25		vex 3413	. . . . 5 ⊢ 𝑥 ∈ V
26	25	ensn1 8592	. . . 4 ⊢ {𝑥} ≈ 1o
27		breq1 5035	. . . 4 ⊢ (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈ 1o))
28	26, 27	mpbiri 261	. . 3 ⊢ (𝐴 = {𝑥} → 𝐴 ≈ 1o)
29	28	exlimiv 1931	. 2 ⊢ (∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o)
30	24, 29	impbii 212	1 ⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})

Syntax hints:   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∅c0 4225  {csn 4522  ⟨cop 4528   class class class wbr 5032  ^◡ccnv 5523  ran crn 5525  ⟶wf 6331  –onto→wfo 6333  –1-1-onto→wf1o 6334  ‘cfv 6335  1_oc1o 8105   ≈ cen 8524

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-1o 8112  df-en 8528

This theorem is referenced by:  en1b  8596  reuen1  8597  en2  8790  card1  9430  pm54.43  9463  hash1elsn  13782  hash1snb  13830  ufildom1  22626  unidifsnel  30405  unidifsnne  30406  funen1cnv  32585  lfuhgr3  32597  snen1g  40605