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 e. V -> A C_ ( fi ` A ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	intsn	|- |^| { x } = x
3		simpl	|- ( ( A e. V /\ x e. A ) -> A e. V )
4		simpr	|- ( ( A e. V /\ x e. A ) -> x e. A )
5	4	snssd	|- ( ( A e. V /\ x e. A ) -> { x } C_ A )
6	1	snnz	|- { x } =/= (/)
7	6	a1i	|- ( ( A e. V /\ x e. A ) -> { x } =/= (/) )
8		snfi	|- { x } e. Fin
9	8	a1i	|- ( ( A e. V /\ x e. A ) -> { x } e. Fin )
10		elfir	|- ( ( A e. V /\ ( { x } C_ A /\ { x } =/= (/) /\ { x } e. Fin ) ) -> |^| { x } e. ( fi ` A ) )
11	3 5 7 9 10	syl13anc	|- ( ( A e. V /\ x e. A ) -> |^| { x } e. ( fi ` A ) )
12	2 11	eqeltrrid	|- ( ( A e. V /\ x e. A ) -> x e. ( fi ` A ) )
13	12	ex	|- ( A e. V -> ( x e. A -> x e. ( fi ` A ) ) )
14	13	ssrdv	|- ( A e. V -> A C_ ( fi ` A ) )