Theorem snfig 6991

Description: A singleton is finite. For the proper class case, see snprc 3733. (Contributed by Jim Kingdon, 13-Apr-2020.)

Assertion

Ref	Expression
snfig	⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin)

Proof of Theorem snfig

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1onn 6690	. . 3 ⊢ 1o ∈ ω
2		ensn1g 6973	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o)
3		breq2 4091	. . . 4 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 2909	. . 3 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 414	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 6936	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 134	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2201  ∃wrex 2510  {csn 3668   class class class wbr 4087  ωcom 4687  1_oc1o 6577   ≈ cen 6909  Fincfn 6911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-nul 4214  ax-pow 4263  ax-pr 4298  ax-un 4529

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-nul 3494  df-pw 3653  df-sn 3674  df-pr 3675  df-op 3677  df-uni 3893  df-int 3928  df-br 4088  df-opab 4150  df-id 4389  df-suc 4467  df-iom 4688  df-xp 4730  df-rel 4731  df-cnv 4732  df-co 4733  df-dm 4734  df-rn 4735  df-fun 5327  df-fn 5328  df-f 5329  df-f1 5330  df-fo 5331  df-f1o 5332  df-1o 6584  df-en 6912  df-fin 6914

This theorem is referenced by:  fiprc  6992  ssfiexmid  7065  ssfiexmidt  7067  domfiexmid  7069  diffitest  7078  eqsndc  7097  unfiexmid  7112  prfidisj  7121  prfidceq  7122  tpfidisj  7123  ssfii  7175  infpwfidom  7411  hashsng  11063  fihashen1  11064  hashunsng  11074  hashprg  11075  hashdifsn  11086  hashdifpr  11087  hashxp  11093  hashtpgim  11112  fsumsplitsnun  12000  fsum2dlemstep  12015  fisumcom2  12019  fsumconst  12035  fsumge1  12042  fsum00  12043  hash2iun1dif1  12061  fprod2dlemstep  12203  fprodcom2fi  12207  fprodsplitsn  12214  fprodsplit1f  12215  phicl2  12806  lgsquadlem2  15833  1loopgrvd2fi  16182  1loopgrvd0fi  16183  1hevtxdg0fi  16184  1hevtxdg1en  16185  p1evtxdeqfilem  16188  trlsegvdeglem7  16343  gfsumsn  16748