# Metamath Proof Explorer

## Theorem ssfii

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)

Ref Expression
Assertion ssfii ${⊢}{A}\in {V}\to {A}\subseteq \mathrm{fi}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 1 intsn ${⊢}\bigcap \left\{{x}\right\}={x}$
3 simpl ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to {A}\in {V}$
4 simpr ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to {x}\in {A}$
5 4 snssd ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to \left\{{x}\right\}\subseteq {A}$
6 1 snnz ${⊢}\left\{{x}\right\}\ne \varnothing$
7 6 a1i ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to \left\{{x}\right\}\ne \varnothing$
8 snfi ${⊢}\left\{{x}\right\}\in \mathrm{Fin}$
9 8 a1i ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to \left\{{x}\right\}\in \mathrm{Fin}$
10 elfir ${⊢}\left({A}\in {V}\wedge \left(\left\{{x}\right\}\subseteq {A}\wedge \left\{{x}\right\}\ne \varnothing \wedge \left\{{x}\right\}\in \mathrm{Fin}\right)\right)\to \bigcap \left\{{x}\right\}\in \mathrm{fi}\left({A}\right)$
11 3 5 7 9 10 syl13anc ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to \bigcap \left\{{x}\right\}\in \mathrm{fi}\left({A}\right)$
12 2 11 eqeltrrid ${⊢}\left({A}\in {V}\wedge {x}\in {A}\right)\to {x}\in \mathrm{fi}\left({A}\right)$
13 12 ex ${⊢}{A}\in {V}\to \left({x}\in {A}\to {x}\in \mathrm{fi}\left({A}\right)\right)$
14 13 ssrdv ${⊢}{A}\in {V}\to {A}\subseteq \mathrm{fi}\left({A}\right)$