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

Theorem isfi 6887
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 6869 . . 3  |-  Fin  =  { y  |  E. x  e.  om  y  ~~  x }
21eleq2i 2349 . 2  |-  ( A  e.  Fin  <->  A  e.  { y  |  E. x  e.  om  y  ~~  x } )
3 relen 6870 . . . . 5  |-  Rel  ~~
43brrelexi 4731 . . . 4  |-  ( A 
~~  x  ->  A  e.  _V )
54rexlimivw 2665 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  A  e. 
_V )
6 breq1 4028 . . . 4  |-  ( y  =  A  ->  (
y  ~~  x  <->  A  ~~  x ) )
76rexbidv 2566 . . 3  |-  ( y  =  A  ->  ( E. x  e.  om  y  ~~  x  <->  E. x  e.  om  A  ~~  x
) )
85, 7elab3 2923 . 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 1625    e. wcel 1686   {cab 2271   E.wrex 2546   _Vcvv 2790   class class class wbr 4025   omcom 4658    ~~ cen 6862   Fincfn 6865
This theorem is referenced by:  snfi  6943  php3  7049  onfin  7053  fisucdomOLD  7068  ominf  7077  isinf  7078  enfi  7081  ssnnfi  7084  ssfi  7085  dif1enOLD  7092  dif1en  7093  findcard  7099  findcard2  7100  findcard3  7102  nnsdomg  7118  isfiniteg  7119  unfi  7126  fiint  7135  pwfi  7153  finnum  7583  ficardom  7596  dif1card  7640  infpwfien  7691  ficard  8189  hashkf  11341  finminlem  26242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698  df-en 6866  df-fin 6869
  Copyright terms: Public domain W3C validator