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

Theorem isfi 6881
Description: Express " A 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  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
Distinct variable group:    x, A

Proof of Theorem isfi
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-fin 6863 . . 3  |-  Fin  =  { y  |  E. x  e.  om  y  ~~  x }
21eleq2i 2348 . 2  |-  ( A  e.  Fin  <->  A  e.  { y  |  E. x  e.  om  y  ~~  x } )
3 relen 6864 . . . . 5  |-  Rel  ~~
43brrelexi 4728 . . . 4  |-  ( A 
~~  x  ->  A  e.  _V )
54rexlimivw 2664 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  A  e. 
_V )
6 breq1 4027 . . . 4  |-  ( y  =  A  ->  (
y  ~~  x  <->  A  ~~  x ) )
76rexbidv 2565 . . 3  |-  ( y  =  A  ->  ( E. x  e.  om  y  ~~  x  <->  E. x  e.  om  A  ~~  x
) )
85, 7elab3 2922 . 2  |-  ( A  e.  { y  |  E. x  e.  om  y  ~~  x }  <->  E. x  e.  om  A  ~~  x
)
92, 8bitri 240 1  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1685   {cab 2270   E.wrex 2545   _Vcvv 2789   class class class wbr 4024   omcom 4655    ~~ cen 6856   Fincfn 6859
This theorem is referenced by:  snfi  6937  php3  7043  onfin  7047  fisucdomOLD  7062  ominf  7071  isinf  7072  enfi  7075  ssnnfi  7078  ssfi  7079  dif1enOLD  7086  dif1en  7087  findcard  7093  findcard2  7094  findcard3  7096  nnsdomg  7112  isfiniteg  7113  unfi  7120  fiint  7129  pwfi  7147  finnum  7577  ficardom  7590  dif1card  7634  infpwfien  7685  ficard  8183  hashkf  11335  finminlem  25642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-xp 4694  df-rel 4695  df-en 6860  df-fin 6863
  Copyright terms: Public domain W3C validator