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

Theorem isfi 8188
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 8168 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2836 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8169 . . . . 5 Rel ≈
43brrelex1i 5330 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3176 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 4814 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3199 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3515 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 266 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  wcel 2155  {cab 2751  wrex 3056  Vcvv 3350   class class class wbr 4811  ωcom 7267  cen 8161  Fincfn 8164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-xp 5285  df-rel 5286  df-en 8165  df-fin 8168
This theorem is referenced by:  snfi  8249  php3  8357  onfin  8362  ominf  8383  isinf  8384  enfi  8387  ssnnfi  8390  ssfi  8391  dif1en  8404  findcard  8410  findcard2  8411  findcard3  8414  nnsdomg  8430  isfiniteg  8431  unfi  8438  fiint  8448  pwfi  8472  finnum  9029  ficardom  9042  dif1card  9088  infpwfien  9140  ficard  9644  hashkf  13330  finminlem  32779
  Copyright terms: Public domain W3C validator