cfilufg

Description: The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018)

		Ref	Expression
	Assertion	cfilufg	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to X filGen F \in CauFilU (U)$

Proof

Step	Hyp	Ref	Expression
1		cfilufbas	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to F \in fBas (X)$
2		fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$
3		filfbas	$⊢ X filGen F \in Fil (X) \to X filGen F \in fBas (X)$
4	1 2 3	3syl	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to X filGen F \in fBas (X)$
5	1	ad3antrrr	$⊢ ((((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \land b \in F) \land b \times b \subseteq v) \to F \in fBas (X)$
6		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
7	5 6	syl	$⊢ ((((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \land b \in F) \land b \times b \subseteq v) \to F \subseteq X filGen F$
8		simplr	$⊢ ((((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \land b \in F) \land b \times b \subseteq v) \to b \in F$
9	7 8	sseldd	$⊢ ((((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \land b \in F) \land b \times b \subseteq v) \to b \in (X filGen F)$
10		id	$⊢ a = b \to a = b$
11	10	sqxpeqd	$⊢ a = b \to a \times a = b \times b$
12	11	sseq1d	$⊢ a = b \to (a \times a \subseteq v \leftrightarrow b \times b \subseteq v)$
13	12	rspcev	$⊢ (b \in (X filGen F) \land b \times b \subseteq v) \to \exists a \in (X filGen F) a \times a \subseteq v$
14	9 13	sylancom	$⊢ ((((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \land b \in F) \land b \times b \subseteq v) \to \exists a \in (X filGen F) a \times a \subseteq v$
15		iscfilu	$⊢ U \in UnifOn (X) \to (F \in CauFilU (U) \leftrightarrow (F \in fBas (X) \land \forall v \in U \exists b \in F b \times b \subseteq v))$
16	15	simplbda	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to \forall v \in U \exists b \in F b \times b \subseteq v$
17	16	r19.21bi	$⊢ ((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \to \exists b \in F b \times b \subseteq v$
18	14 17	r19.29a	$⊢ ((U \in UnifOn (X) \land F \in CauFilU (U)) \land v \in U) \to \exists a \in (X filGen F) a \times a \subseteq v$
19	18	ralrimiva	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to \forall v \in U \exists a \in (X filGen F) a \times a \subseteq v$
20		iscfilu	$⊢ U \in UnifOn (X) \to (X filGen F \in CauFilU (U) \leftrightarrow (X filGen F \in fBas (X) \land \forall v \in U \exists a \in (X filGen F) a \times a \subseteq v))$
21	20	adantr	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to (X filGen F \in CauFilU (U) \leftrightarrow (X filGen F \in fBas (X) \land \forall v \in U \exists a \in (X filGen F) a \times a \subseteq v))$
22	4 19 21	mpbir2and	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to X filGen F \in CauFilU (U)$

Metamath Proof Explorer

Theorem cfilufg

Proof