elfm

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

		Ref	Expression
	Assertion	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 x \in B F [x] \subseteq A))$

Proof

Step	Hyp	Ref	Expression
1		fmval	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = X filGen ran (t \in B ⟼ F [t])$
2	1	eleq2d	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X FilMap F) (B) \leftrightarrow A \in (X filGen ran (t \in B ⟼ F [t])))$
3		eqid	$⊢ ran (t \in B ⟼ F [t]) = ran (t \in B ⟼ F [t])$
4	3	fbasrn	$⊢ (B \in fBas (Y) \land F : Y ⟶ X \land X \in C) \to ran (t \in B ⟼ F [t]) \in fBas (X)$
5	4	3comr	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to ran (t \in B ⟼ F [t]) \in fBas (X)$
6		elfg	$⊢ ran (t \in B ⟼ F [t]) \in fBas (X) \to (A \in (X filGen ran (t \in B ⟼ F [t])) \leftrightarrow (A \subseteq X \land \exists y \in ran (t \in B ⟼ F [t]) y \subseteq A))$
7	5 6	syl	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X filGen ran (t \in B ⟼ F [t])) \leftrightarrow (A \subseteq X \land \exists y \in ran (t \in B ⟼ F [t]) y \subseteq A))$
8		simpr	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to x \in B$
9		eqid	$⊢ F [x] = F [x]$
10		imaeq2	$⊢ t = x \to F [t] = F [x]$
11	10	rspceeqv	$⊢ (x \in B \land F [x] = F [x]) \to \exists t \in B F [x] = F [t]$
12	8 9 11	sylancl	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to \exists t \in B F [x] = F [t]$
13		simpl1	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to X \in C$
14		imassrn	$⊢ F [x] \subseteq ran F$
15		frn	$⊢ F : Y ⟶ X \to ran F \subseteq X$
16	15	3ad2ant3	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to ran F \subseteq X$
17	16	adantr	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to ran F \subseteq X$
18	14 17	sstrid	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to F [x] \subseteq X$
19	13 18	ssexd	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to F [x] \in V$
20		eqid	$⊢ (t \in B ⟼ F [t]) = (t \in B ⟼ F [t])$
21	20	elrnmpt	$⊢ F [x] \in V \to (F [x] \in ran (t \in B ⟼ F [t]) \leftrightarrow \exists t \in B F [x] = F [t])$
22	19 21	syl	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to (F [x] \in ran (t \in B ⟼ F [t]) \leftrightarrow \exists t \in B F [x] = F [t])$
23	12 22	mpbird	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land x \in B) \to F [x] \in ran (t \in B ⟼ F [t])$
24	10	cbvmptv	$⊢ (t \in B ⟼ F [t]) = (x \in B ⟼ F [x])$
25	24	elrnmpt	$⊢ y \in ran (t \in B ⟼ F [t]) \to (y \in ran (t \in B ⟼ F [t]) \leftrightarrow \exists x \in B y = F [x])$
26	25	ibi	$⊢ y \in ran (t \in B ⟼ F [t]) \to \exists x \in B y = F [x]$
27	26	adantl	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in ran (t \in B ⟼ F [t])) \to \exists x \in B y = F [x]$
28		simpr	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land y = F [x]) \to y = F [x]$
29	28	sseq1d	$⊢ ((X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \land y = F [x]) \to (y \subseteq A \leftrightarrow F [x] \subseteq A)$
30	23 27 29	rexxfrd	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists y \in ran (t \in B ⟼ F [t]) y \subseteq A \leftrightarrow \exists x \in B F [x] \subseteq A)$
31	30	anbi2d	$⊢ (X \in C \land B \in fBas (Y) \land F : Y ⟶ X) \to ((A \subseteq X \land \exists y \in ran (t \in B ⟼ F [t]) y \subseteq A) \leftrightarrow (A \subseteq X \land \exists x \in B F [x] \subseteq A))$
32	2 7 31	3bitrd	$⊢ (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 B F [x] \subseteq A))$

Metamath Proof Explorer

Theorem elfm

Proof