ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  en1 GIF version

Theorem en1 6309
Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
Assertion
Ref Expression
en1 (𝐴 ≈ 1𝑜 ↔ ∃𝑥 𝐴 = {𝑥})
Distinct variable group:   𝑥,𝐴

Proof of Theorem en1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df1o2 6043 . . . . 5 1𝑜 = {∅}
21breq2i 3799 . . . 4 (𝐴 ≈ 1𝑜𝐴 ≈ {∅})
3 bren 6258 . . . 4 (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
42, 3bitri 177 . . 3 (𝐴 ≈ 1𝑜 ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
5 f1ocnv 5166 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝑓:{∅}–1-1-onto𝐴)
6 f1ofo 5160 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}–onto𝐴)
7 forn 5136 . . . . . . . 8 (𝑓:{∅}–onto𝐴 → ran 𝑓 = 𝐴)
86, 7syl 14 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = 𝐴)
9 f1of 5153 . . . . . . . . . 10 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}⟶𝐴)
10 0ex 3911 . . . . . . . . . . . 12 ∅ ∈ V
1110fsn2 5364 . . . . . . . . . . 11 (𝑓:{∅}⟶𝐴 ↔ ((𝑓‘∅) ∈ 𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩}))
1211simprbi 264 . . . . . . . . . 10 (𝑓:{∅}⟶𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
139, 12syl 14 . . . . . . . . 9 (𝑓:{∅}–1-1-onto𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
1413rneqd 4590 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = ran {⟨∅, (𝑓‘∅)⟩})
1510rnsnop 4828 . . . . . . . 8 ran {⟨∅, (𝑓‘∅)⟩} = {(𝑓‘∅)}
1614, 15syl6eq 2104 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = {(𝑓‘∅)})
178, 16eqtr3d 2090 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴𝐴 = {(𝑓‘∅)})
185, 17syl 14 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝐴 = {(𝑓‘∅)})
19 f1ofn 5154 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴𝑓 Fn {∅})
2010snid 3429 . . . . . . 7 ∅ ∈ {∅}
21 funfvex 5219 . . . . . . . 8 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (𝑓‘∅) ∈ V)
2221funfni 5026 . . . . . . 7 ((𝑓 Fn {∅} ∧ ∅ ∈ {∅}) → (𝑓‘∅) ∈ V)
2319, 20, 22sylancl 398 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → (𝑓‘∅) ∈ V)
24 sneq 3413 . . . . . . . 8 (𝑥 = (𝑓‘∅) → {𝑥} = {(𝑓‘∅)})
2524eqeq2d 2067 . . . . . . 7 (𝑥 = (𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(𝑓‘∅)}))
2625spcegv 2658 . . . . . 6 ((𝑓‘∅) ∈ V → (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}))
2723, 26syl 14 . . . . 5 (𝑓:{∅}–1-1-onto𝐴 → (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}))
285, 18, 27sylc 60 . . . 4 (𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
2928exlimiv 1505 . . 3 (∃𝑓 𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
304, 29sylbi 118 . 2 (𝐴 ≈ 1𝑜 → ∃𝑥 𝐴 = {𝑥})
31 vex 2577 . . . . 5 𝑥 ∈ V
3231ensn1 6306 . . . 4 {𝑥} ≈ 1𝑜
33 breq1 3794 . . . 4 (𝐴 = {𝑥} → (𝐴 ≈ 1𝑜 ↔ {𝑥} ≈ 1𝑜))
3432, 33mpbiri 161 . . 3 (𝐴 = {𝑥} → 𝐴 ≈ 1𝑜)
3534exlimiv 1505 . 2 (∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1𝑜)
3630, 35impbii 121 1 (𝐴 ≈ 1𝑜 ↔ ∃𝑥 𝐴 = {𝑥})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102   = wceq 1259  wex 1397  wcel 1409  Vcvv 2574  c0 3251  {csn 3402  cop 3405   class class class wbr 3791  ccnv 4371  ran crn 4373   Fn wfn 4924  wf 4925  ontowfo 4927  1-1-ontowf1o 4928  cfv 4929  1𝑜c1o 6024  cen 6249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-reu 2330  df-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-id 4057  df-suc 4135  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-1o 6031  df-en 6252
This theorem is referenced by:  en1bg  6310  reuen1  6311
  Copyright terms: Public domain W3C validator