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 \in V \to A \subseteq fi (A)$

Proof

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