ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isfi GIF version

Theorem isfi 6430
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 6412 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2151 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 6413 . . . . 5 Rel ≈
43brrelexi 4450 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 2481 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 3823 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 2377 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 2758 . 2 (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥} ↔ ∃𝑥 ∈ ω 𝐴𝑥)
92, 8bitri 182 1 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1287  wcel 1436  {cab 2071  wrex 2356  Vcvv 2615   class class class wbr 3820  ωcom 4378  cen 6407  Fincfn 6409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-br 3821  df-opab 3875  df-xp 4417  df-rel 4418  df-en 6410  df-fin 6412
This theorem is referenced by:  snfig  6483  fict  6536  fidceq  6537  nnfi  6540  enfi  6541  ssfilem  6543  dif1enen  6548  php5fin  6550  fisbth  6551  fin0  6553  fin0or  6554  diffitest  6555  findcard  6556  findcard2  6557  findcard2s  6558  diffisn  6561  infnfi  6563  fientri3  6577  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  finnum  6755  hashcl  10085  hashen  10088  fihashdom  10107  hashun  10109  zfz1iso  10142
  Copyright terms: Public domain W3C validator