Metamath Proof Explorer

Theorem imaelfm

Description: An image of a filter element is in the image filter. (Contributed by Jeff Hankins, 5-Oct-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	imaelfm.l	$⊢ L = Y filGen B$
	Assertion	imaelfm	$⊢ ((X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \land S \in L) \to F [S] \in (X FilMap F) (B)$

Proof

Step	Hyp	Ref	Expression
1		imaelfm.l	$⊢ L = Y filGen B$
2		fimass	$⊢ F : Y ⟶ X \to F [S] \subseteq X$
3	2	3ad2ant3	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to F [S] \subseteq X$
4		ssid	$⊢ F [S] \subseteq F [S]$
5		imaeq2	$⊢ x = S \to F [x] = F [S]$
6	5	sseq1d	$⊢ x = S \to (F [x] \subseteq F [S] \leftrightarrow F [S] \subseteq F [S])$
7	6	rspcev	$⊢ (S \in L \land F [S] \subseteq F [S]) \to \exists x \in L F [x] \subseteq F [S]$
8	4 7	mpan2	$⊢ S \in L \to \exists x \in L F [x] \subseteq F [S]$
9	3 8	anim12i	$⊢ ((X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \land S \in L) \to (F [S] \subseteq X \land \exists x \in L F [x] \subseteq F [S])$
10	1	elfm2	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to (F [S] \in (X FilMap F) (B) \leftrightarrow (F [S] \subseteq X \land \exists x \in L F [x] \subseteq F [S]))$
11	10	adantr	$⊢ ((X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \land S \in L) \to (F [S] \in (X FilMap F) (B) \leftrightarrow (F [S] \subseteq X \land \exists x \in L F [x] \subseteq F [S]))$
12	9 11	mpbird	$⊢ ((X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \land S \in L) \to F [S] \in (X FilMap F) (B)$