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

Theorem isfi 7354
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 7335 . . 3  |-  Fin  =  { y  |  E. x  e.  om  y  ~~  x }
21eleq2i 2507 . 2  |-  ( A  e.  Fin  <->  A  e.  { y  |  E. x  e.  om  y  ~~  x } )
3 relen 7336 . . . . 5  |-  Rel  ~~
43brrelexi 4900 . . . 4  |-  ( A 
~~  x  ->  A  e.  _V )
54rexlimivw 2858 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  A  e. 
_V )
6 breq1 4316 . . . 4  |-  ( y  =  A  ->  (
y  ~~  x  <->  A  ~~  x ) )
76rexbidv 2757 . . 3  |-  ( y  =  A  ->  ( E. x  e.  om  y  ~~  x  <->  E. x  e.  om  A  ~~  x
) )
85, 7elab3 3134 . 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 1369    e. wcel 1756   {cab 2429   E.wrex 2737   _Vcvv 2993   class class class wbr 4313   omcom 6497    ~~ cen 7328   Fincfn 7331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-rel 4868  df-en 7332  df-fin 7335
This theorem is referenced by:  snfi  7411  php3  7518  onfin  7522  fisucdomOLD  7537  ominf  7546  isinf  7547  enfi  7550  ssnnfi  7553  ssfi  7554  dif1enOLD  7565  dif1en  7566  findcard  7572  findcard2  7573  findcard3  7576  nnsdomg  7592  isfiniteg  7593  unfi  7600  fiint  7609  pwfi  7627  finnum  8139  ficardom  8152  dif1card  8198  infpwfien  8253  ficard  8750  hashkf  12126  finminlem  28539
  Copyright terms: Public domain W3C validator