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)$$