Theorem filssufil

Description: A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 .) (Contributed by Jeff Hankins, 2-Dec-2009) (Revised by Stefan O'Rear, 29-Jul-2015)

	Ref	Expression
Assertion	filssufil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )

Proof

Step	Hyp	Ref	Expression
1		filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
2		pwexg	⊢ ( 𝑋 ∈ 𝐹 → 𝒫 𝑋 ∈ V )
3		pwexg	⊢ ( 𝒫 𝑋 ∈ V → 𝒫 𝒫 𝑋 ∈ V )
4		numth3	⊢ ( 𝒫 𝒫 𝑋 ∈ V → 𝒫 𝒫 𝑋 ∈ dom card )
5	1 2 3 4	4syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝒫 𝒫 𝑋 ∈ dom card )
6		filssufilg	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
7	5 6	mpdan	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )