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 )