Metamath Proof Explorer

Theorem 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∈A∧Y∈B∧F:Y⟶X→XFilMapF:fBas⁡Y⟶Fil⁡X

Proof

Step Hyp Ref Expression
1 ovex ⊢XfilGenran⁡y∈b⟼Fy∈V
2 eqid ⊢b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy=b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy
3 1 2 fnmpti ⊢b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼FyFnfBas⁡Y
4 df-fm ⊢FilMap=x∈V,f∈V⟼b∈fBas⁡dom⁡f⟼xfilGenran⁡y∈b⟼fy
5 4 a1i ⊢X∈A∧Y∈B∧F:Y⟶X→FilMap=x∈V,f∈V⟼b∈fBas⁡dom⁡f⟼xfilGenran⁡y∈b⟼fy
6 dmeq ⊢f=F→dom⁡f=dom⁡F
7 6 adantl ⊢x=X∧f=F→dom⁡f=dom⁡F
8 fdm ⊢F:Y⟶X→dom⁡F=Y
9 8 3ad2ant3 ⊢X∈A∧Y∈B∧F:Y⟶X→dom⁡F=Y
10 7 9 sylan9eqr ⊢X∈A∧Y∈B∧F:Y⟶X∧x=X∧f=F→dom⁡f=Y
11 10 fveq2d ⊢X∈A∧Y∈B∧F:Y⟶X∧x=X∧f=F→fBas⁡dom⁡f=fBas⁡Y
12 id ⊢x=X→x=X
13 imaeq1 ⊢f=F→fy=Fy
14 13 mpteq2dv ⊢f=F→y∈b⟼fy=y∈b⟼Fy
15 14 rneqd ⊢f=F→ran⁡y∈b⟼fy=ran⁡y∈b⟼Fy
16 12 15 oveqan12d ⊢x=X∧f=F→xfilGenran⁡y∈b⟼fy=XfilGenran⁡y∈b⟼Fy
17 16 adantl ⊢X∈A∧Y∈B∧F:Y⟶X∧x=X∧f=F→xfilGenran⁡y∈b⟼fy=XfilGenran⁡y∈b⟼Fy
18 11 17 mpteq12dv ⊢X∈A∧Y∈B∧F:Y⟶X∧x=X∧f=F→b∈fBas⁡dom⁡f⟼xfilGenran⁡y∈b⟼fy=b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy
19 elex ⊢X∈A→X∈V
20 19 3ad2ant1 ⊢X∈A∧Y∈B∧F:Y⟶X→X∈V
21 fex2 ⊢F:Y⟶X∧Y∈B∧X∈A→F∈V
22 21 3com13 ⊢X∈A∧Y∈B∧F:Y⟶X→F∈V
23 fvex ⊢fBas⁡Y∈V
24 23 mptex ⊢b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy∈V
25 24 a1i ⊢X∈A∧Y∈B∧F:Y⟶X→b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy∈V
26 5 18 20 22 25 ovmpod ⊢X∈A∧Y∈B∧F:Y⟶X→XFilMapF=b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼Fy
27 26 fneq1d ⊢X∈A∧Y∈B∧F:Y⟶X→XFilMapFFnfBas⁡Y↔b∈fBas⁡Y⟼XfilGenran⁡y∈b⟼FyFnfBas⁡Y
28 3 27 mpbiri ⊢X∈A∧Y∈B∧F:Y⟶X→XFilMapFFnfBas⁡Y
29 simpl1 ⊢X∈A∧Y∈B∧F:Y⟶X∧b∈fBas⁡Y→X∈A
30 simpr ⊢X∈A∧Y∈B∧F:Y⟶X∧b∈fBas⁡Y→b∈fBas⁡Y
31 simpl3 ⊢X∈A∧Y∈B∧F:Y⟶X∧b∈fBas⁡Y→F:Y⟶X
32 fmfil ⊢X∈A∧b∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡b∈Fil⁡X
33 29 30 31 32 syl3anc ⊢X∈A∧Y∈B∧F:Y⟶X∧b∈fBas⁡Y→XFilMapF⁡b∈Fil⁡X
34 33 ralrimiva ⊢X∈A∧Y∈B∧F:Y⟶X→∀b∈fBas⁡YXFilMapF⁡b∈Fil⁡X
35 ffnfv ⊢XFilMapF:fBas⁡Y⟶Fil⁡X↔XFilMapFFnfBas⁡Y∧∀b∈fBas⁡YXFilMapF⁡b∈Fil⁡X
36 28 34 35 sylanbrc ⊢X∈A∧Y∈B∧F:Y⟶X→XFilMapF:fBas⁡Y⟶Fil⁡X