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

Theorem ssfii 7668
Description: Any element of a set  A is the intersection of a finite subset of  A. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
ssfii  |-  ( A  e.  V  ->  A  C_  ( fi `  A
) )

Proof of Theorem ssfii
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 2974 . . . . 5  |-  x  e. 
_V
21intsn 4163 . . . 4  |-  |^| { x }  =  x
3 simpl 457 . . . . 5  |-  ( ( A  e.  V  /\  x  e.  A )  ->  A  e.  V )
4 simpr 461 . . . . . 6  |-  ( ( A  e.  V  /\  x  e.  A )  ->  x  e.  A )
54snssd 4017 . . . . 5  |-  ( ( A  e.  V  /\  x  e.  A )  ->  { x }  C_  A )
61snnz 3992 . . . . . 6  |-  { x }  =/=  (/)
76a1i 11 . . . . 5  |-  ( ( A  e.  V  /\  x  e.  A )  ->  { x }  =/=  (/) )
8 snfi 7389 . . . . . 6  |-  { x }  e.  Fin
98a1i 11 . . . . 5  |-  ( ( A  e.  V  /\  x  e.  A )  ->  { x }  e.  Fin )
10 elfir 7664 . . . . 5  |-  ( ( A  e.  V  /\  ( { x }  C_  A  /\  { x }  =/=  (/)  /\  { x }  e.  Fin )
)  ->  |^| { x }  e.  ( fi `  A ) )
113, 5, 7, 9, 10syl13anc 1220 . . . 4  |-  ( ( A  e.  V  /\  x  e.  A )  ->  |^| { x }  e.  ( fi `  A
) )
122, 11syl5eqelr 2527 . . 3  |-  ( ( A  e.  V  /\  x  e.  A )  ->  x  e.  ( fi
`  A ) )
1312ex 434 . 2  |-  ( A  e.  V  ->  (
x  e.  A  ->  x  e.  ( fi `  A ) ) )
1413ssrdv 3361 1  |-  ( A  e.  V  ->  A  C_  ( fi `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    =/= wne 2605    C_ wss 3327   (/)c0 3636   {csn 3876   |^|cint 4127   ` cfv 5417   Fincfn 7309   ficfi 7659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-int 4128  df-br 4292  df-opab 4350  df-mpt 4351  df-tr 4385  df-eprel 4631  df-id 4635  df-po 4640  df-so 4641  df-fr 4678  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-om 6476  df-1o 6919  df-en 7310  df-fin 7313  df-fi 7660
This theorem is referenced by:  fieq0  7670  dffi2  7672  inficl  7674  fiuni  7677  dffi3  7680  inffien  8232  fictb  8413  ordtbas2  18794  ordtbas  18795  ordtopn1  18797  ordtopn2  18798  leordtval2  18815  subbascn  18857  2ndcsb  19052  ptbasfi  19153  xkoopn  19161  fsubbas  19439  fbunfip  19441  isufil2  19480  ufileu  19491  filufint  19492  fmfnfmlem4  19529  fmfnfm  19530  hausflim  19553  flimclslem  19556  fclsfnflim  19599  flimfnfcls  19600  fclscmp  19602  alexsubb  19617  alexsubALTlem4  19621  ordtconlem1  26353  topjoin  28584
  Copyright terms: Public domain W3C validator