This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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