Metamath Proof Explorer

Theorem fmfg

Description: The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	elfm2.l	$⊢ L = Y filGen B$
	Assertion	fmfg	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = (X FilMap F) (L)$

Proof

Step	Hyp	Ref	Expression
1		elfm2.l	$⊢ L = Y filGen B$
2	1	elfm2	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (B) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
3		fgcl	$⊢ B \in fBas (Y) \to Y filGen B \in Fil (Y)$
4	1 3	eqeltrid	$⊢ B \in fBas (Y) \to L \in Fil (Y)$
5		filfbas	$⊢ L \in Fil (Y) \to L \in fBas (Y)$
6	4 5	syl	$⊢ B \in fBas (Y) \to L \in fBas (Y)$
7		elfm	$⊢ (X \in C \land L \in fBas (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (L) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
8	6 7	syl3an2	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (L) \leftrightarrow (x \subseteq X \land \exists s \in L F [s] \subseteq x))$
9	2 8	bitr4d	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (x \in (X FilMap F) (B) \leftrightarrow x \in (X FilMap F) (L))$
10	9	eqrdv	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = (X FilMap F) (L)$