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