Metamath Proof Explorer

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 ⊢ F ∈ Fil ⁡ X → ∃ f ∈ UFil ⁡ X F ⊆ f

Proof

Step Hyp Ref Expression
1 filtop ⊢ F ∈ Fil ⁡ X → X ∈ F
2 pwexg ⊢ X ∈ F → 𝒫 X ∈ V
3 pwexg ⊢ 𝒫 X ∈ V → 𝒫 𝒫 X ∈ V
4 numth3 ⊢ 𝒫 𝒫 X ∈ V → 𝒫 𝒫 X ∈ dom ⁡ card
5 1 2 3 4 4syl ⊢ F ∈ Fil ⁡ X → 𝒫 𝒫 X ∈ dom ⁡ card
6 filssufilg ⊢ F ∈ Fil ⁡ X ∧ 𝒫 𝒫 X ∈ dom ⁡ card → ∃ f ∈ UFil ⁡ X F ⊆ f
7 5 6 mpdan ⊢ F ∈ Fil ⁡ X → ∃ f ∈ UFil ⁡ X F ⊆ f