Metamath Proof Explorer

Theorem cfiluexsm

Description: For a Cauchy filter base and any entourage V , there is an element of the filter small in V . (Contributed by Thierry Arnoux, 19-Nov-2017)

		Ref	Expression
	Assertion	cfiluexsm	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U) \land V \in U) \to \exists a \in F a \times a \subseteq V$

Proof

Step	Hyp	Ref	Expression
1		iscfilu	$⊢ U \in UnifOn (X) \to (F \in CauFilU (U) \leftrightarrow (F \in fBas (X) \land \forall v \in U \exists a \in F a \times a \subseteq v))$
2	1	simplbda	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to \forall v \in U \exists a \in F a \times a \subseteq v$
3	2	3adant3	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U) \land V \in U) \to \forall v \in U \exists a \in F a \times a \subseteq v$
4		sseq2	$⊢ v = V \to (a \times a \subseteq v \leftrightarrow a \times a \subseteq V)$
5	4	rexbidv	$⊢ v = V \to (\exists a \in F a \times a \subseteq v \leftrightarrow \exists a \in F a \times a \subseteq V)$
6	5	rspcv	$⊢ V \in U \to (\forall v \in U \exists a \in F a \times a \subseteq v \to \exists a \in F a \times a \subseteq V)$
7	6	3ad2ant3	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U) \land V \in U) \to (\forall v \in U \exists a \in F a \times a \subseteq v \to \exists a \in F a \times a \subseteq V)$
8	3 7	mpd	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U) \land V \in U) \to \exists a \in F a \times a \subseteq V$