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

Theorem isfi 7067
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 7049 . . 3  |-  Fin  =  { y  |  E. x  e.  om  y  ~~  x }
21eleq2i 2451 . 2  |-  ( A  e.  Fin  <->  A  e.  { y  |  E. x  e.  om  y  ~~  x } )
3 relen 7050 . . . . 5  |-  Rel  ~~
43brrelexi 4858 . . . 4  |-  ( A 
~~  x  ->  A  e.  _V )
54rexlimivw 2769 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  A  e. 
_V )
6 breq1 4156 . . . 4  |-  ( y  =  A  ->  (
y  ~~  x  <->  A  ~~  x ) )
76rexbidv 2670 . . 3  |-  ( y  =  A  ->  ( E. x  e.  om  y  ~~  x  <->  E. x  e.  om  A  ~~  x
) )
85, 7elab3 3032 . 2  |-  ( A  e.  { y  |  E. x  e.  om  y  ~~  x }  <->  E. x  e.  om  A  ~~  x
)
92, 8bitri 241 1  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1717   {cab 2373   E.wrex 2650   _Vcvv 2899   class class class wbr 4153   omcom 4785    ~~ cen 7042   Fincfn 7045
This theorem is referenced by:  snfi  7123  php3  7229  onfin  7233  fisucdomOLD  7248  ominf  7257  isinf  7258  enfi  7261  ssnnfi  7264  ssfi  7265  dif1enOLD  7276  dif1en  7277  findcard  7283  findcard2  7284  findcard3  7286  nnsdomg  7302  isfiniteg  7303  unfi  7310  fiint  7319  pwfi  7337  finnum  7768  ficardom  7781  dif1card  7825  infpwfien  7876  ficard  8373  hashkf  11547  finminlem  26012
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-en 7046  df-fin 7049
  Copyright terms: Public domain W3C validator