Theorem isfi 8950

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 8925	. . 3 ⊢ Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥}
2	1	eleq2i 2821	. 2 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥})
3		relen 8926	. . . . 5 ⊢ Rel ≈
4	3	brrelex1i 5697	. . . 4 ⊢ (𝐴 ≈ 𝑥 → 𝐴 ∈ V)
5	4	rexlimivw 3131	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ V)
6		breq1 5113	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ≈ 𝑥 ↔ 𝐴 ≈ 𝑥))
7	6	rexbidv 3158	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦 ≈ 𝑥 ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥))
8	5, 7	elab3 3656	. 2 ⊢ (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥} ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
9	2, 8	bitri 275	1 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2708  ∃wrex 3054  Vcvv 3450   class class class wbr 5110  ωcom 7845   ≈ cen 8918  Fincfn 8921

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-en 8922  df-fin 8925

This theorem is referenced by:  0fi  9016  snfi  9017  snfiOLD  9018  findcard  9133  findcard2  9134  nnfi  9137  ssnnfi  9139  unfi  9141  ssfiALT  9144  enfii  9156  enfiALT  9158  php3  9179  onfin  9185  ominf  9212  ominfOLD  9213  isinf  9214  isinfOLD  9215  dif1ennnALT  9229  findcard3  9236  findcard3OLD  9237  nnsdomg  9253  nnsdomgOLD  9254  isfiniteg  9255  prfi  9281  fiint  9284  fiintOLD  9285  finnum  9908  ficardom  9921  dif1card  9970  infpwfien  10022  ficard  10525  hashkf  14304  finminlem  36313  domalom  37399