fmfil

Description: A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Assertion	fmfil	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) \in Fil (X)$

Step	Hyp	Ref	Expression
1		fmval	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = X filGen ran (y \in B ⟼ F [y])$
2		eqid	$⊢ ran (y \in B ⟼ F [y]) = ran (y \in B ⟼ F [y])$
3	2	fbasrn	$⊢ (B \in fBas (Y) \land F : Y ⟶ X \land X \in A) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
4	3	3comr	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
5		fgcl	$⊢ ran (y \in B ⟼ F [y]) \in fBas (X) \to X filGen ran (y \in B ⟼ F [y]) \in Fil (X)$
6	4 5	syl	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to X filGen ran (y \in B ⟼ F [y]) \in Fil (X)$
7	1 6	eqeltrd	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) \in Fil (X)$

Metamath Proof Explorer