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

Theorem isfi 8968
Description: Express "𝐴 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 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Distinct variable group:   𝑥,𝐴

Proof of Theorem isfi
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-fin 8939 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2825 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8940 . . . . 5 Rel ≈
43brrelex1i 5730 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3151 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 5150 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3178 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3675 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 274 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  {cab 2709  wrex 3070  Vcvv 3474   class class class wbr 5147  ωcom 7851  cen 8932  Fincfn 8935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-en 8936  df-fin 8939
This theorem is referenced by:  snfi  9040  findcard  9159  findcard2  9160  nnfi  9163  ssnnfi  9165  ssnnfiOLD  9166  unfi  9168  ssfiALT  9170  enfii  9185  enfiALT  9187  php3  9208  php3OLD  9220  onfin  9226  ominf  9254  ominfOLD  9255  isinf  9256  isinfOLD  9257  dif1ennnALT  9273  findcard2OLD  9280  findcard3  9281  findcard3OLD  9282  nnsdomg  9298  nnsdomgOLD  9299  isfiniteg  9300  unfiOLD  9309  fiint  9320  pwfiOLD  9343  finnum  9939  ficardom  9952  dif1card  10001  infpwfien  10053  ficard  10556  hashkf  14288  finminlem  35191  domalom  36273
  Copyright terms: Public domain W3C validator