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

Theorem isfi 7458
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 7439 . . 3  |-  Fin  =  { y  |  E. x  e.  om  y  ~~  x }
21eleq2i 2460 . 2  |-  ( A  e.  Fin  <->  A  e.  { y  |  E. x  e.  om  y  ~~  x } )
3 relen 7440 . . . . 5  |-  Rel  ~~
43brrelexi 4954 . . . 4  |-  ( A 
~~  x  ->  A  e.  _V )
54rexlimivw 2871 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  A  e. 
_V )
6 breq1 4370 . . . 4  |-  ( y  =  A  ->  (
y  ~~  x  <->  A  ~~  x ) )
76rexbidv 2893 . . 3  |-  ( y  =  A  ->  ( E. x  e.  om  y  ~~  x  <->  E. x  e.  om  A  ~~  x
) )
85, 7elab3 3178 . 2  |-  ( A  e.  { y  |  E. x  e.  om  y  ~~  x }  <->  E. x  e.  om  A  ~~  x
)
92, 8bitri 249 1  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1399    e. wcel 1826   {cab 2367   E.wrex 2733   _Vcvv 3034   class class class wbr 4367   omcom 6599    ~~ cen 7432   Fincfn 7435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-en 7436  df-fin 7439
This theorem is referenced by:  snfi  7515  php3  7622  onfin  7627  ominf  7648  isinf  7649  enfi  7652  ssnnfi  7655  ssfi  7656  dif1en  7668  findcard  7674  findcard2  7675  findcard3  7678  nnsdomg  7694  isfiniteg  7695  unfi  7702  fiint  7712  pwfi  7730  finnum  8242  ficardom  8255  dif1card  8301  infpwfien  8356  ficard  8853  hashkf  12309  finminlem  30302
  Copyright terms: Public domain W3C validator