This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmufil

Description: An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fmufil ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
2 filfbas ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
3 1 2 syl ⊢ ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
4 fmfil ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
5 3 4 syl3an2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
6 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → 𝐿 ∈ ( UFil ‘ 𝑌 ) )
7 6 1 2 3syl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
8 simprl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
9 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
10 simprr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 )
11 7 8 9 10 fmfnfm ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → ∃ 𝑔 ∈ ( Fil ‘ 𝑌 ) ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) )
12 6 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → 𝐿 ∈ ( UFil ‘ 𝑌 ) )
13 simprl ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → 𝑔 ∈ ( Fil ‘ 𝑌 ) )
14 simprrl ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → 𝐿 ⊆ 𝑔 )
15 ufilmax ⊢ ( ( 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝑔 ) → 𝐿 = 𝑔 )
16 12 13 14 15 syl3anc ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → 𝐿 = 𝑔 )
17 16 fveq2d ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) )
18 simprrr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) )
19 17 18 eqtr4d ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝐿 ⊆ 𝑔 ∧ 𝑓 = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝑔 ) ) ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = 𝑓 )
20 11 19 rexlimddv ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 ) ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = 𝑓 )
21 20 expr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = 𝑓 ) )
22 21 ralrimiva ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = 𝑓 ) )
23 isufil2 ⊢ ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) ↔ ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ⊆ 𝑓 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) = 𝑓 ) ) )
24 5 22 23 sylanbrc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) )