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	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	intsn	⊢ ∩ { 𝑥 } = 𝑥
3		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
4		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
5	4	snssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ⊆ 𝐴 )
6	1	snnz	⊢ { 𝑥 } ≠ ∅
7	6	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ≠ ∅ )
8		snfi	⊢ { 𝑥 } ∈ Fin
9	8	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ Fin )
10		elfir	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( { 𝑥 } ⊆ 𝐴 ∧ { 𝑥 } ≠ ∅ ∧ { 𝑥 } ∈ Fin ) ) → ∩ { 𝑥 } ∈ ( fi ‘ 𝐴 ) )
11	3 5 7 9 10	syl13anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → ∩ { 𝑥 } ∈ ( fi ‘ 𝐴 ) )
12	2 11	eqeltrrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( fi ‘ 𝐴 ) )
13	12	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( fi ‘ 𝐴 ) ) )
14	13	ssrdv	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )