Metamath Proof Explorer

Theorem ufli

Description: Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufli ⊢ X ∈ UFL ∧ F ∈ Fil ⁡ X → ∃ f ∈ UFil ⁡ X F ⊆ f

Proof

Step Hyp Ref Expression
1 isufl ⊢ X ∈ UFL → X ∈ UFL ↔ ∀ g ∈ Fil ⁡ X ∃ f ∈ UFil ⁡ X g ⊆ f
2 1 ibi ⊢ X ∈ UFL → ∀ g ∈ Fil ⁡ X ∃ f ∈ UFil ⁡ X g ⊆ f
3 sseq1 ⊢ g = F → g ⊆ f ↔ F ⊆ f
4 3 rexbidv ⊢ g = F → ∃ f ∈ UFil ⁡ X g ⊆ f ↔ ∃ f ∈ UFil ⁡ X F ⊆ f
5 4 rspccva ⊢ ∀ g ∈ Fil ⁡ X ∃ f ∈ UFil ⁡ X g ⊆ f ∧ F ∈ Fil ⁡ X → ∃ f ∈ UFil ⁡ X F ⊆ f
6 2 5 sylan ⊢ X ∈ UFL ∧ F ∈ Fil ⁡ X → ∃ f ∈ UFil ⁡ X F ⊆ f