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 ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) : ( fBas ‘ 𝑌 ) ⟶ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ∈ V
2 eqid ⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) )
3 1 2 fnmpti ⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) Fn ( fBas ‘ 𝑌 )
4 df-fm ⊢ FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) )
5 4 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) ) )
6 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
7 6 adantl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 )
8 fdm ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → dom 𝐹 = 𝑌 )
9 8 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → dom 𝐹 = 𝑌 )
10 7 9 sylan9eqr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → dom 𝑓 = 𝑌 )
11 10 fveq2d ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → ( fBas ‘ dom 𝑓 ) = ( fBas ‘ 𝑌 ) )
12 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
13 imaeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ 𝑦 ) = ( 𝐹 “ 𝑦 ) )
14 13 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) = ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) )
15 14 rneqd ⊢ ( 𝑓 = 𝐹 → ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) )
16 12 15 oveqan12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) )
17 16 adantl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) )
18 11 17 mpteq12dv ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
19 elex ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ V )
20 19 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 ∈ V )
21 fex2 ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 ∈ V )
22 21 3com13 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 ∈ V )
23 fvex ⊢ ( fBas ‘ 𝑌 ) ∈ V
24 23 mptex ⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ∈ V
25 24 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ∈ V )
26 5 18 20 22 25 ovmpod ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
27 26 fneq1d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) ↔ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) Fn ( fBas ‘ 𝑌 ) ) )
28 3 27 mpbiri ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) )
29 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝑋 ∈ 𝐴 )
30 simpr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝑏 ∈ ( fBas ‘ 𝑌 ) )
31 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
32 fmfil ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) ∈ ( Fil ‘ 𝑋 ) )
33 29 30 31 32 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑏 ∈ ( fBas ‘ 𝑌 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) ∈ ( Fil ‘ 𝑋 ) )
34 33 ralrimiva ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ∀ 𝑏 ∈ ( fBas ‘ 𝑌 ) ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) ∈ ( Fil ‘ 𝑋 ) )
35 ffnfv ⊢ ( ( 𝑋 FilMap 𝐹 ) : ( fBas ‘ 𝑌 ) ⟶ ( Fil ‘ 𝑋 ) ↔ ( ( 𝑋 FilMap 𝐹 ) Fn ( fBas ‘ 𝑌 ) ∧ ∀ 𝑏 ∈ ( fBas ‘ 𝑌 ) ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑏 ) ∈ ( Fil ‘ 𝑋 ) ) )
36 28 34 35 sylanbrc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) : ( fBas ‘ 𝑌 ) ⟶ ( Fil ‘ 𝑋 ) )