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

Theorem isfi 9014
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 8987 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2830 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8988 . . . . 5 Rel ≈
43brrelex1i 5744 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3148 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 5150 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3176 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3688 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 275 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1536  wcel 2105  {cab 2711  wrex 3067  Vcvv 3477   class class class wbr 5147  ωcom 7886  cen 8980  Fincfn 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-en 8984  df-fin 8987
This theorem is referenced by:  0fi  9080  snfi  9081  snfiOLD  9082  findcard  9201  findcard2  9202  nnfi  9205  ssnnfi  9207  unfi  9209  ssfiALT  9212  enfii  9223  enfiALT  9225  php3  9246  php3OLD  9258  onfin  9264  ominf  9291  ominfOLD  9292  isinf  9293  isinfOLD  9294  dif1ennnALT  9308  findcard3  9315  findcard3OLD  9316  nnsdomg  9332  nnsdomgOLD  9333  isfiniteg  9334  prfi  9360  fiint  9363  fiintOLD  9364  finnum  9985  ficardom  9998  dif1card  10047  infpwfien  10099  ficard  10602  hashkf  14367  finminlem  36300  domalom  37386
  Copyright terms: Public domain W3C validator