fgss

Description: A bigger base generates a bigger filter. (Contributed by NM, 5-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fgss	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to X filGen F \subseteq X filGen G$

Step	Hyp	Ref	Expression
1		ssrexv	$⊢ F \subseteq G \to (\exists x \in F x \subseteq t \to \exists x \in G x \subseteq t)$
2	1	anim2d	$⊢ F \subseteq G \to ((t \subseteq X \land \exists x \in F x \subseteq t) \to (t \subseteq X \land \exists x \in G x \subseteq t))$
3	2	3ad2ant3	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to ((t \subseteq X \land \exists x \in F x \subseteq t) \to (t \subseteq X \land \exists x \in G x \subseteq t))$
4		elfg	$⊢ F \in fBas (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists x \in F x \subseteq t))$
5	4	3ad2ant1	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists x \in F x \subseteq t))$
6		elfg	$⊢ G \in fBas (X) \to (t \in (X filGen G) \leftrightarrow (t \subseteq X \land \exists x \in G x \subseteq t))$
7	6	3ad2ant2	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to (t \in (X filGen G) \leftrightarrow (t \subseteq X \land \exists x \in G x \subseteq t))$
8	3 5 7	3imtr4d	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to (t \in (X filGen F) \to t \in (X filGen G))$
9	8	ssrdv	$⊢ (F \in fBas (X) \land G \in fBas (X) \land F \subseteq G) \to X filGen F \subseteq X filGen G$

Metamath Proof Explorer