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

Theorem isfi 8990
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 8961 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2821 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 8962 . . . . 5 Rel ≈
43brrelex1i 5728 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 3147 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 5145 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 3174 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 3674 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 275 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wcel 2099  {cab 2705  wrex 3066  Vcvv 3470   class class class wbr 5142  ωcom 7864  cen 8954  Fincfn 8957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-xp 5678  df-rel 5679  df-en 8958  df-fin 8961
This theorem is referenced by:  snfi  9062  findcard  9181  findcard2  9182  nnfi  9185  ssnnfi  9187  ssnnfiOLD  9188  unfi  9190  ssfiALT  9192  enfii  9207  enfiALT  9209  php3  9230  php3OLD  9242  onfin  9248  ominf  9276  ominfOLD  9277  isinf  9278  isinfOLD  9279  dif1ennnALT  9295  findcard2OLD  9302  findcard3  9303  findcard3OLD  9304  nnsdomg  9320  nnsdomgOLD  9321  isfiniteg  9322  unfiOLD  9331  fiint  9342  pwfiOLD  9365  finnum  9965  ficardom  9978  dif1card  10027  infpwfien  10079  ficard  10582  hashkf  14317  finminlem  35796  domalom  36877
  Copyright terms: Public domain W3C validator