This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL )

Proof

Step Hyp Ref Expression
1 filssufilg ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 )
2 1 ancoms ⊢ ( ( 𝒫 𝒫 𝑋 ∈ dom card ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 )
3 2 ralrimiva ⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 )
4 pwexr ⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → 𝒫 𝑋 ∈ V )
5 pwexb ⊢ ( 𝑋 ∈ V ↔ 𝒫 𝑋 ∈ V )
6 4 5 sylibr ⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ V )
7 isufl ⊢ ( 𝑋 ∈ V → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )
8 6 7 syl ⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )
9 3 8 mpbird ⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL )