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

Theorem isfi 6411
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 6393 . . 3 Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥}
21eleq2i 2151 . 2 (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦𝑥})
3 relen 6394 . . . . 5 Rel ≈
43brrelexi 4443 . . . 4 (𝐴𝑥𝐴 ∈ V)
54rexlimivw 2481 . . 3 (∃𝑥 ∈ ω 𝐴𝑥𝐴 ∈ V)
6 breq1 3817 . . . 4 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
76rexbidv 2377 . . 3 (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦𝑥 ↔ ∃𝑥 ∈ ω 𝐴𝑥))
85, 7elab3 2757 . 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 2614   class class class wbr 3814  ωcom 4371  cen 6388  Fincfn 6390
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 3925  ax-pow 3977  ax-pr 4003
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 2616  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-br 3815  df-opab 3869  df-xp 4410  df-rel 4411  df-en 6391  df-fin 6393
This theorem is referenced by:  snfig  6464  fict  6517  fidceq  6518  nnfi  6521  enfi  6522  ssfilem  6524  dif1enen  6529  php5fin  6531  fisbth  6532  fin0  6534  fin0or  6535  diffitest  6536  findcard  6537  findcard2  6538  findcard2s  6539  diffisn  6542  infnfi  6544  fientri3  6555  unsnfi  6559  unsnfidcex  6560  unsnfidcel  6561  finnum  6732  hashcl  10038  hashen  10041  fihashdom  10060  hashun  10062
  Copyright terms: Public domain W3C validator