Theorem isfi 8924

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.

Step	Hyp	Ref	Expression
1		df-fin 8899	. . 3 ⊢ Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥}
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥})
3		relen 8900	. . . . 5 ⊢ Rel ≈
4	3	brrelex1i 5688	. . . 4 ⊢ (𝐴 ≈ 𝑥 → 𝐴 ∈ V)
5	4	rexlimivw 3135	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ V)
6		breq1 5103	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ≈ 𝑥 ↔ 𝐴 ≈ 𝑥))
7	6	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦 ≈ 𝑥 ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥))
8	5, 7	elab3 3643	. 2 ⊢ (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥} ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
9	2, 8	bitri 275	1 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3062  Vcvv 3442   class class class wbr 5100  ωcom 7818   ≈ cen 8892  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-en 8896  df-fin 8899

This theorem is referenced by:  0fi  8991  snfi  8992  findcard  9100  findcard2  9101  nnfi  9104  ssnnfi  9106  unfi  9107  ssfiALT  9110  enfii  9122  enfiALT  9124  php3  9145  onfin  9151  ominf  9176  isinf  9177  dif1ennnALT  9189  findcard3  9195  nnsdomg  9211  isfiniteg  9212  prfi  9236  fiint  9239  finnum  9872  ficardom  9885  dif1card  9932  infpwfien  9984  ficard  10487  hashkf  14267  finminlem  36534  domalom  37659