elfm2

Description: An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	elfm2.l	$⊢ L = Y filGen B$
	Assertion	elfm2	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X FilMap F) (B) \leftrightarrow (A \subseteq X \land \exists x \in L F [x] \subseteq A))$

Proof

Step	Hyp	Ref	Expression
1		elfm2.l	$⊢ L = Y filGen B$
2		elfm	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X FilMap F) (B) \leftrightarrow (A \subseteq X \land \exists y \in B F [y] \subseteq A))$
3		ssfg	$⊢ B \in fBas (Y) \to B \subseteq Y filGen B$
4	3 1	sseqtrrdi	$⊢ B \in fBas (Y) \to B \subseteq L$
5	4	sselda	$⊢ (B \in fBas (Y) \land y \in B) \to y \in L$
6	5	adantrr	$⊢ (B \in fBas (Y) \land (y \in B \land F [y] \subseteq A)) \to y \in L$
7	6	3ad2antl2	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (y \in B \land F [y] \subseteq A)) \to y \in L$
8		simprr	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (y \in B \land F [y] \subseteq A)) \to F [y] \subseteq A$
9		imaeq2	$⊢ x = y \to F [x] = F [y]$
10	9	sseq1d	$⊢ x = y \to (F [x] \subseteq A \leftrightarrow F [y] \subseteq A)$
11	10	rspcev	$⊢ (y \in L \land F [y] \subseteq A) \to \exists x \in L F [x] \subseteq A$
12	7 8 11	syl2anc	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (y \in B \land F [y] \subseteq A)) \to \exists x \in L F [x] \subseteq A$
13	12	rexlimdvaa	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists y \in B F [y] \subseteq A \to \exists x \in L F [x] \subseteq A)$
14	1	eleq2i	$⊢ x \in L \leftrightarrow x \in (Y filGen B)$
15		elfg	$⊢ B \in fBas (Y) \to (x \in (Y filGen B) \leftrightarrow (x \subseteq Y \land \exists y \in B y \subseteq x))$
16	14 15	syl5bb	$⊢ B \in fBas (Y) \to (x \in L \leftrightarrow (x \subseteq Y \land \exists y \in B y \subseteq x))$
17	16	3ad2ant2	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (x \in L \leftrightarrow (x \subseteq Y \land \exists y \in B y \subseteq x))$
18		imass2	$⊢ y \subseteq x \to F [y] \subseteq F [x]$
19		sstr2	$⊢ F [y] \subseteq F [x] \to (F [x] \subseteq A \to F [y] \subseteq A)$
20	19	com12	$⊢ F [x] \subseteq A \to (F [y] \subseteq F [x] \to F [y] \subseteq A)$
21	20	ad2antll	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (x \subseteq Y \land F [x] \subseteq A)) \to (F [y] \subseteq F [x] \to F [y] \subseteq A)$
22	18 21	syl5	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (x \subseteq Y \land F [x] \subseteq A)) \to (y \subseteq x \to F [y] \subseteq A)$
23	22	reximdv	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land (x \subseteq Y \land F [x] \subseteq A)) \to (\exists y \in B y \subseteq x \to \exists y \in B F [y] \subseteq A)$
24	23	expr	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \subseteq Y) \to (F [x] \subseteq A \to (\exists y \in B y \subseteq x \to \exists y \in B F [y] \subseteq A))$
25	24	com23	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \subseteq Y) \to (\exists y \in B y \subseteq x \to (F [x] \subseteq A \to \exists y \in B F [y] \subseteq A))$
26	25	expimpd	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to ((x \subseteq Y \land \exists y \in B y \subseteq x) \to (F [x] \subseteq A \to \exists y \in B F [y] \subseteq A))$
27	17 26	sylbid	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (x \in L \to (F [x] \subseteq A \to \exists y \in B F [y] \subseteq A))$
28	27	rexlimdv	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists x \in L F [x] \subseteq A \to \exists y \in B F [y] \subseteq A)$
29	13 28	impbid	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists y \in B F [y] \subseteq A \leftrightarrow \exists x \in L F [x] \subseteq A)$
30	29	anbi2d	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to ((A \subseteq X \land \exists y \in B F [y] \subseteq A) \leftrightarrow (A \subseteq X \land \exists x \in L F [x] \subseteq A))$
31	2 30	bitrd	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X FilMap F) (B) \leftrightarrow (A \subseteq X \land \exists x \in L F [x] \subseteq A))$

Metamath Proof Explorer

Theorem elfm2

Proof