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

Theorem isfi 9016
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 8989 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2833 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8990 . . . . 5 Rel ≈
43brrelex1i 5741 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3151 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 5146 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3179 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3686 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 275 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wcel 2108  {cab 2714  wrex 3070  Vcvv 3480   class class class wbr 5143  ωcom 7887  cen 8982  Fincfn 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-en 8986  df-fin 8989
This theorem is referenced by:  0fi  9082  snfi  9083  snfiOLD  9084  findcard  9203  findcard2  9204  nnfi  9207  ssnnfi  9209  unfi  9211  ssfiALT  9214  enfii  9226  enfiALT  9228  php3  9249  php3OLD  9261  onfin  9267  ominf  9294  ominfOLD  9295  isinf  9296  isinfOLD  9297  dif1ennnALT  9311  findcard3  9318  findcard3OLD  9319  nnsdomg  9335  nnsdomgOLD  9336  isfiniteg  9337  prfi  9363  fiint  9366  fiintOLD  9367  finnum  9988  ficardom  10001  dif1card  10050  infpwfien  10102  ficard  10605  hashkf  14371  finminlem  36319  domalom  37405
  Copyright terms: Public domain W3C validator