MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfi Structured version   Visualization version   GIF version

Theorem isfi 8969
Description: Express "𝐴 is finite". Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
isfi (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Distinct variable group:   𝑥,𝐴

Proof of Theorem isfi
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-fin 8940 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2817 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8941 . . . . 5 Rel ≈
43brrelex1i 5723 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3143 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 5142 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3170 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3669 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 275 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1533  wcel 2098  {cab 2701  wrex 3062  Vcvv 3466   class class class wbr 5139  ωcom 7849  cen 8933  Fincfn 8936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-br 5140  df-opab 5202  df-xp 5673  df-rel 5674  df-en 8937  df-fin 8940
This theorem is referenced by:  snfi  9041  findcard  9160  findcard2  9161  nnfi  9164  ssnnfi  9166  ssnnfiOLD  9167  unfi  9169  ssfiALT  9171  enfii  9186  enfiALT  9188  php3  9209  php3OLD  9221  onfin  9227  ominf  9255  ominfOLD  9256  isinf  9257  isinfOLD  9258  dif1ennnALT  9274  findcard2OLD  9281  findcard3  9282  findcard3OLD  9283  nnsdomg  9299  nnsdomgOLD  9300  isfiniteg  9301  unfiOLD  9310  fiint  9321  pwfiOLD  9344  finnum  9940  ficardom  9953  dif1card  10002  infpwfien  10054  ficard  10557  hashkf  14290  finminlem  35694  domalom  36776
  Copyright terms: Public domain W3C validator