Metamath Proof Explorer

Theorem numufl

Description: Consequence of filssufilg : a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion numufl ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → X ∈ UFL

Proof

Step Hyp Ref Expression
1 filssufilg ⊢ f ∈ Fil ⁡ X ∧ 𝒫 𝒫 X ∈ dom ⁡ card → ∃ g ∈ UFil ⁡ X f ⊆ g
2 1 ancoms ⊢ 𝒫 𝒫 X ∈ dom ⁡ card ∧ f ∈ Fil ⁡ X → ∃ g ∈ UFil ⁡ X f ⊆ g
3 2 ralrimiva ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → ∀ f ∈ Fil ⁡ X ∃ g ∈ UFil ⁡ X f ⊆ g
4 pwexr ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → 𝒫 X ∈ V
5 pwexb ⊢ X ∈ V ↔ 𝒫 X ∈ V
6 4 5 sylibr ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → X ∈ V
7 isufl ⊢ X ∈ V → X ∈ UFL ↔ ∀ f ∈ Fil ⁡ X ∃ g ∈ UFil ⁡ X f ⊆ g
8 6 7 syl ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → X ∈ UFL ↔ ∀ f ∈ Fil ⁡ X ∃ g ∈ UFil ⁡ X f ⊆ g
9 3 8 mpbird ⊢ 𝒫 𝒫 X ∈ dom ⁡ card → X ∈ UFL