MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssfii Structured version   Visualization version   GIF version

Theorem ssfii 9410
Description: Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
ssfii (𝐴𝑉𝐴 ⊆ (fi‘𝐴))

Proof of Theorem ssfii
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vex 3478 . . . . 5 𝑥 ∈ V
21intsn 4989 . . . 4 {𝑥} = 𝑥
3 simpl 483 . . . . 5 ((𝐴𝑉𝑥𝐴) → 𝐴𝑉)
4 simpr 485 . . . . . 6 ((𝐴𝑉𝑥𝐴) → 𝑥𝐴)
54snssd 4811 . . . . 5 ((𝐴𝑉𝑥𝐴) → {𝑥} ⊆ 𝐴)
61snnz 4779 . . . . . 6 {𝑥} ≠ ∅
76a1i 11 . . . . 5 ((𝐴𝑉𝑥𝐴) → {𝑥} ≠ ∅)
8 snfi 9040 . . . . . 6 {𝑥} ∈ Fin
98a1i 11 . . . . 5 ((𝐴𝑉𝑥𝐴) → {𝑥} ∈ Fin)
10 elfir 9406 . . . . 5 ((𝐴𝑉 ∧ ({𝑥} ⊆ 𝐴 ∧ {𝑥} ≠ ∅ ∧ {𝑥} ∈ Fin)) → {𝑥} ∈ (fi‘𝐴))
113, 5, 7, 9, 10syl13anc 1372 . . . 4 ((𝐴𝑉𝑥𝐴) → {𝑥} ∈ (fi‘𝐴))
122, 11eqeltrrid 2838 . . 3 ((𝐴𝑉𝑥𝐴) → 𝑥 ∈ (fi‘𝐴))
1312ex 413 . 2 (𝐴𝑉 → (𝑥𝐴𝑥 ∈ (fi‘𝐴)))
1413ssrdv 3987 1 (𝐴𝑉𝐴 ⊆ (fi‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wne 2940  wss 3947  c0 4321  {csn 4627   cint 4949  cfv 6540  Fincfn 8935  ficfi 9401
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-1o 8462  df-en 8936  df-fin 8939  df-fi 9402
This theorem is referenced by:  fieq0  9412  dffi2  9414  inficl  9416  fiuni  9419  dffi3  9422  inffien  10054  fictb  10236  ordtbas2  22686  ordtbas  22687  ordtopn1  22689  ordtopn2  22690  leordtval2  22707  subbascn  22749  2ndcsb  22944  ptbasfi  23076  xkoopn  23084  fsubbas  23362  fbunfip  23364  isufil2  23403  ufileu  23414  filufint  23415  fmfnfmlem4  23452  fmfnfm  23453  hausflim  23476  flimclslem  23479  fclsfnflim  23522  flimfnfcls  23523  fclscmp  23525  alexsubb  23541  alexsubALTlem4  23545  ordtconnlem1  32892  topjoin  35238
  Copyright terms: Public domain W3C validator