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 ‘ 𝑋 ) )