Theorem ufli

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

	Ref	Expression
Assertion	ufli	⊢ ( ( 𝑋 ∈ UFL ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )

Proof

Step	Hyp	Ref	Expression
1		isufl	⊢ ( 𝑋 ∈ UFL → ( 𝑋 ∈ UFL ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 ) )
2	1	ibi	⊢ ( 𝑋 ∈ UFL → ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 )
3		sseq1	⊢ ( 𝑔 = 𝐹 → ( 𝑔 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑓 ) )
4	3	rexbidv	⊢ ( 𝑔 = 𝐹 → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 ↔ ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ) )
5	4	rspccva	⊢ ( ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
6	2 5	sylan	⊢ ( ( 𝑋 ∈ UFL ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )