ssfg

Description: A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$

Step	Hyp	Ref	Expression
1		fbelss	$⊢ (F \in fBas (X) \land t \in F) \to t \subseteq X$
2	1	ex	$⊢ F \in fBas (X) \to (t \in F \to t \subseteq X)$
3		ssid	$⊢ t \subseteq t$
4		sseq1	$⊢ x = t \to (x \subseteq t \leftrightarrow t \subseteq t)$
5	4	rspcev	$⊢ (t \in F \land t \subseteq t) \to \exists x \in F x \subseteq t$
6	3 5	mpan2	$⊢ t \in F \to \exists x \in F x \subseteq t$
7	2 6	jca2	$⊢ F \in fBas (X) \to (t \in F \to (t \subseteq X \land \exists x \in F x \subseteq t))$
8		elfg	$⊢ F \in fBas (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists x \in F x \subseteq t))$
9	7 8	sylibrd	$⊢ F \in fBas (X) \to (t \in F \to t \in (X filGen F))$
10	9	ssrdv	$⊢ F \in fBas (X) \to F \subseteq X filGen F$

Metamath Proof Explorer