cfiluweak

Description: A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018)

		Ref	Expression
	Assertion	cfiluweak	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \in CauFilU (U)$

Proof

Step	Hyp	Ref	Expression
1		trust	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
2		iscfilu	$⊢ U ↾_{𝑡} (A \times A) \in UnifOn (A) \to (F \in CauFilU (U ↾_{𝑡} (A \times A)) \leftrightarrow (F \in fBas (A) \land \forall u \in (U ↾_{𝑡} (A \times A)) \exists a \in F a \times a \subseteq u))$
3	2	biimpa	$⊢ (U ↾_{𝑡} (A \times A) \in UnifOn (A) \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to (F \in fBas (A) \land \forall u \in (U ↾_{𝑡} (A \times A)) \exists a \in F a \times a \subseteq u)$
4	1 3	stoic3	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to (F \in fBas (A) \land \forall u \in (U ↾_{𝑡} (A \times A)) \exists a \in F a \times a \subseteq u)$
5	4	simpld	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \in fBas (A)$
6		fbsspw	$⊢ F \in fBas (A) \to F \subseteq 𝒫 A$
7	5 6	syl	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \subseteq 𝒫 A$
8		simp2	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to A \subseteq X$
9	8	sspwd	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to 𝒫 A \subseteq 𝒫 X$
10	7 9	sstrd	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \subseteq 𝒫 X$
11		simp1	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to U \in UnifOn (X)$
12	11	elfvexd	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to X \in V$
13		fbasweak	$⊢ (F \in fBas (A) \land F \subseteq 𝒫 X \land X \in V) \to F \in fBas (X)$
14	5 10 12 13	syl3anc	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \in fBas (X)$
15		sseq2	$⊢ u = v \cap (A \times A) \to (a \times a \subseteq u \leftrightarrow a \times a \subseteq v \cap (A \times A))$
16	15	rexbidv	$⊢ u = v \cap (A \times A) \to (\exists a \in F a \times a \subseteq u \leftrightarrow \exists a \in F a \times a \subseteq v \cap (A \times A))$
17	4	simprd	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to \forall u \in (U ↾_{𝑡} (A \times A)) \exists a \in F a \times a \subseteq u$
18	17	adantr	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to \forall u \in (U ↾_{𝑡} (A \times A)) \exists a \in F a \times a \subseteq u$
19	11	adantr	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to U \in UnifOn (X)$
20	12	adantr	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to X \in V$
21	8	adantr	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to A \subseteq X$
22	20 21	ssexd	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to A \in V$
23	22 22	xpexd	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to A \times A \in V$
24		simpr	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to v \in U$
25		elrestr	$⊢ (U \in UnifOn (X) \land A \times A \in V \land v \in U) \to v \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
26	19 23 24 25	syl3anc	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to v \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
27	16 18 26	rspcdva	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to \exists a \in F a \times a \subseteq v \cap (A \times A)$
28		inss1	$⊢ v \cap (A \times A) \subseteq v$
29		sstr	$⊢ (a \times a \subseteq v \cap (A \times A) \land v \cap (A \times A) \subseteq v) \to a \times a \subseteq v$
30	28 29	mpan2	$⊢ a \times a \subseteq v \cap (A \times A) \to a \times a \subseteq v$
31	30	reximi	$⊢ \exists a \in F a \times a \subseteq v \cap (A \times A) \to \exists a \in F a \times a \subseteq v$
32	27 31	syl	$⊢ ((U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \land v \in U) \to \exists a \in F a \times a \subseteq v$
33	32	ralrimiva	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to \forall v \in U \exists a \in F a \times a \subseteq v$
34		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))$
35	34	3ad2ant1	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to (F \in CauFilU (U) \leftrightarrow (F \in fBas (X) \land \forall v \in U \exists a \in F a \times a \subseteq v))$
36	14 33 35	mpbir2and	$⊢ (U \in UnifOn (X) \land A \subseteq X \land F \in CauFilU (U ↾_{𝑡} (A \times A))) \to F \in CauFilU (U)$

Metamath Proof Explorer

Theorem cfiluweak

Proof