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

Theorem en1 6702
 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.
StepHypRef Expression
1 df1o2 6335 . . . . 5 1o = {∅}
21breq2i 3946 . . . 4 (𝐴 ≈ 1o𝐴 ≈ {∅})
3 bren 6650 . . . 4 (𝐴 ≈ {∅} ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
42, 3bitri 183 . . 3 (𝐴 ≈ 1o ↔ ∃𝑓 𝑓:𝐴1-1-onto→{∅})
5 f1ocnv 5389 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝑓:{∅}–1-1-onto𝐴)
6 f1ofo 5383 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}–onto𝐴)
7 forn 5357 . . . . . . . 8 (𝑓:{∅}–onto𝐴 → ran 𝑓 = 𝐴)
86, 7syl 14 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = 𝐴)
9 f1of 5376 . . . . . . . . . 10 (𝑓:{∅}–1-1-onto𝐴𝑓:{∅}⟶𝐴)
10 0ex 4064 . . . . . . . . . . . 12 ∅ ∈ V
1110fsn2 5603 . . . . . . . . . . 11 (𝑓:{∅}⟶𝐴 ↔ ((𝑓‘∅) ∈ 𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩}))
1211simprbi 273 . . . . . . . . . 10 (𝑓:{∅}⟶𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
139, 12syl 14 . . . . . . . . 9 (𝑓:{∅}–1-1-onto𝐴𝑓 = {⟨∅, (𝑓‘∅)⟩})
1413rneqd 4777 . . . . . . . 8 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = ran {⟨∅, (𝑓‘∅)⟩})
1510rnsnop 5028 . . . . . . . 8 ran {⟨∅, (𝑓‘∅)⟩} = {(𝑓‘∅)}
1614, 15eqtrdi 2189 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴 → ran 𝑓 = {(𝑓‘∅)})
178, 16eqtr3d 2175 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴𝐴 = {(𝑓‘∅)})
185, 17syl 14 . . . . 5 (𝑓:𝐴1-1-onto→{∅} → 𝐴 = {(𝑓‘∅)})
19 f1ofn 5377 . . . . . . 7 (𝑓:{∅}–1-1-onto𝐴𝑓 Fn {∅})
2010snid 3564 . . . . . . 7 ∅ ∈ {∅}
21 funfvex 5447 . . . . . . . 8 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (𝑓‘∅) ∈ V)
2221funfni 5232 . . . . . . 7 ((𝑓 Fn {∅} ∧ ∅ ∈ {∅}) → (𝑓‘∅) ∈ V)
2319, 20, 22sylancl 410 . . . . . 6 (𝑓:{∅}–1-1-onto𝐴 → (𝑓‘∅) ∈ V)
24 sneq 3544 . . . . . . . 8 (𝑥 = (𝑓‘∅) → {𝑥} = {(𝑓‘∅)})
2524eqeq2d 2152 . . . . . . 7 (𝑥 = (𝑓‘∅) → (𝐴 = {𝑥} ↔ 𝐴 = {(𝑓‘∅)}))
2625spcegv 2778 . . . . . 6 ((𝑓‘∅) ∈ V → (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}))
2723, 26syl 14 . . . . 5 (𝑓:{∅}–1-1-onto𝐴 → (𝐴 = {(𝑓‘∅)} → ∃𝑥 𝐴 = {𝑥}))
285, 18, 27sylc 62 . . . 4 (𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
2928exlimiv 1578 . . 3 (∃𝑓 𝑓:𝐴1-1-onto→{∅} → ∃𝑥 𝐴 = {𝑥})
304, 29sylbi 120 . 2 (𝐴 ≈ 1o → ∃𝑥 𝐴 = {𝑥})
31 vex 2693 . . . . 5 𝑥 ∈ V
3231ensn1 6699 . . . 4 {𝑥} ≈ 1o
33 breq1 3941 . . . 4 (𝐴 = {𝑥} → (𝐴 ≈ 1o ↔ {𝑥} ≈ 1o))
3432, 33mpbiri 167 . . 3 (𝐴 = {𝑥} → 𝐴 ≈ 1o)
3534exlimiv 1578 . 2 (∃𝑥 𝐴 = {𝑥} → 𝐴 ≈ 1o)
3630, 35impbii 125 1 (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481  Vcvv 2690  ∅c0 3369  {csn 3533  ⟨cop 3536   class class class wbr 3938  ◡ccnv 4547  ran crn 4549   Fn wfn 5127  ⟶wf 5128  –onto→wfo 5130  –1-1-onto→wf1o 5131  ‘cfv 5132  1oc1o 6315   ≈ cen 6641 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-reu 2424  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-id 4224  df-suc 4302  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-1o 6322  df-en 6644 This theorem is referenced by:  en1bg  6703  reuen1  6704  pm54.43  7066
 Copyright terms: Public domain W3C validator