ufli

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

		Ref	Expression
	Assertion	ufli	$⊢ (X \in UFL \land F \in Fil (X)) \to \exists f \in UFil (X) F \subseteq f$

Step	Hyp	Ref	Expression
1		isufl	$⊢ X \in UFL \to (X \in UFL \leftrightarrow \forall g \in Fil (X) \exists f \in UFil (X) g \subseteq f)$
2	1	ibi	$⊢ X \in UFL \to \forall g \in Fil (X) \exists f \in UFil (X) g \subseteq f$
3		sseq1	$⊢ g = F \to (g \subseteq f \leftrightarrow F \subseteq f)$
4	3	rexbidv	$⊢ g = F \to (\exists f \in UFil (X) g \subseteq f \leftrightarrow \exists f \in UFil (X) F \subseteq f)$
5	4	rspccva	$⊢ (\forall g \in Fil (X) \exists f \in UFil (X) g \subseteq f \land F \in Fil (X)) \to \exists f \in UFil (X) F \subseteq f$
6	2 5	sylan	$⊢ (X \in UFL \land F \in Fil (X)) \to \exists f \in UFil (X) F \subseteq f$

Metamath Proof Explorer