fmf

Description: Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ X filGen ran (y \in b ⟼ F [y]) \in V$
2		eqid	$⊢ (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y])) = (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y]))$
3	1 2	fnmpti	$⊢ (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y])) Fn fBas (Y)$
4		df-fm	$⊢ FilMap = (x \in V, f \in V ⟼ (b \in fBas (dom f) ⟼ x filGen ran (y \in b ⟼ f [y])))$
5	4	a1i	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to FilMap = (x \in V, f \in V ⟼ (b \in fBas (dom f) ⟼ x filGen ran (y \in b ⟼ f [y])))$
6		dmeq	$⊢ f = F \to dom f = dom F$
7	6	adantl	$⊢ (x = X \land f = F) \to dom f = dom F$
8		fdm	$⊢ F : Y ⟶ X \to dom F = Y$
9	8	3ad2ant3	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to dom F = Y$
10	7 9	sylan9eqr	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land (x = X \land f = F)) \to dom f = Y$
11	10	fveq2d	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land (x = X \land f = F)) \to fBas (dom f) = fBas (Y)$
12		id	$⊢ x = X \to x = X$
13		imaeq1	$⊢ f = F \to f [y] = F [y]$
14	13	mpteq2dv	$⊢ f = F \to (y \in b ⟼ f [y]) = (y \in b ⟼ F [y])$
15	14	rneqd	$⊢ f = F \to ran (y \in b ⟼ f [y]) = ran (y \in b ⟼ F [y])$
16	12 15	oveqan12d	$⊢ (x = X \land f = F) \to x filGen ran (y \in b ⟼ f [y]) = X filGen ran (y \in b ⟼ F [y])$
17	16	adantl	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land (x = X \land f = F)) \to x filGen ran (y \in b ⟼ f [y]) = X filGen ran (y \in b ⟼ F [y])$
18	11 17	mpteq12dv	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land (x = X \land f = F)) \to (b \in fBas (dom f) ⟼ x filGen ran (y \in b ⟼ f [y])) = (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y]))$
19		elex	$⊢ X \in A \to X \in V$
20	19	3ad2ant1	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to X \in V$
21		fex2	$⊢ (F : Y ⟶ X \land Y \in B \land X \in A) \to F \in V$
22	21	3com13	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to F \in V$
23		fvex	$⊢ fBas (Y) \in V$
24	23	mptex	$⊢ (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y])) \in V$
25	24	a1i	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y])) \in V$
26	5 18 20 22 25	ovmpod	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to X FilMap F = (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y]))$
27	26	fneq1d	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to ((X FilMap F) Fn fBas (Y) \leftrightarrow (b \in fBas (Y) ⟼ X filGen ran (y \in b ⟼ F [y])) Fn fBas (Y))$
28	3 27	mpbiri	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to (X FilMap F) Fn fBas (Y)$
29		simpl1	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land b \in fBas (Y)) \to X \in A$
30		simpr	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land b \in fBas (Y)) \to b \in fBas (Y)$
31		simpl3	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land b \in fBas (Y)) \to F : Y ⟶ X$
32		fmfil	$⊢ (X \in A \land b \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (b) \in Fil (X)$
33	29 30 31 32	syl3anc	$⊢ ((X \in A \land Y \in B \land F : Y ⟶ X) \land b \in fBas (Y)) \to (X FilMap F) (b) \in Fil (X)$
34	33	ralrimiva	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to \forall b \in fBas (Y) (X FilMap F) (b) \in Fil (X)$
35		ffnfv	$⊢ (X FilMap F) : fBas (Y) ⟶ Fil (X) \leftrightarrow ((X FilMap F) Fn fBas (Y) \land \forall b \in fBas (Y) (X FilMap F) (b) \in Fil (X))$
36	28 34 35	sylanbrc	$⊢ (X \in A \land Y \in B \land F : Y ⟶ X) \to (X FilMap F) : fBas (Y) ⟶ Fil (X)$

Metamath Proof Explorer

Theorem fmf

Proof