trcfilu

Description: Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to U \in UnifOn (X)$
2		simp2l	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to F \in CauFilU (U)$
3		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))$
4	3	biimpa	$⊢ (U \in UnifOn (X) \land F \in CauFilU (U)) \to (F \in fBas (X) \land \forall v \in U \exists a \in F a \times a \subseteq v)$
5	1 2 4	syl2anc	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to (F \in fBas (X) \land \forall v \in U \exists a \in F a \times a \subseteq v)$
6	5	simpld	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to F \in fBas (X)$
7		simp3	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to A \subseteq X$
8		simp2r	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to \neg \emptyset \in (F ↾_{𝑡} A)$
9		trfbas2	$⊢ (F \in fBas (X) \land A \subseteq X) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow \neg \emptyset \in (F ↾_{𝑡} A))$
10	9	biimpar	$⊢ ((F \in fBas (X) \land A \subseteq X) \land \neg \emptyset \in (F ↾_{𝑡} A)) \to F ↾_{𝑡} A \in fBas (A)$
11	6 7 8 10	syl21anc	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to F ↾_{𝑡} A \in fBas (A)$
12	2	ad5antr	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to F \in CauFilU (U)$
13	1	adantr	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to U \in UnifOn (X)$
14	13	elfvexd	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to X \in V$
15	7	adantr	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to A \subseteq X$
16	14 15	ssexd	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to A \in V$
17	16	ad4antr	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to A \in V$
18		simplr	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to a \in F$
19		elrestr	$⊢ (F \in CauFilU (U) \land A \in V \land a \in F) \to a \cap A \in (F ↾_{𝑡} A)$
20	12 17 18 19	syl3anc	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to a \cap A \in (F ↾_{𝑡} A)$
21		inxp	$⊢ (a \times a) \cap (A \times A) = (a \cap A) \times (a \cap A)$
22		simpr	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to a \times a \subseteq v$
23	22	ssrind	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to (a \times a) \cap (A \times A) \subseteq v \cap (A \times A)$
24		simpllr	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to w = v \cap (A \times A)$
25	23 24	sseqtrrd	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to (a \times a) \cap (A \times A) \subseteq w$
26	21 25	eqsstrrid	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to (a \cap A) \times (a \cap A) \subseteq w$
27		id	$⊢ b = a \cap A \to b = a \cap A$
28	27	sqxpeqd	$⊢ b = a \cap A \to b \times b = (a \cap A) \times (a \cap A)$
29	28	sseq1d	$⊢ b = a \cap A \to (b \times b \subseteq w \leftrightarrow (a \cap A) \times (a \cap A) \subseteq w)$
30	29	rspcev	$⊢ (a \cap A \in (F ↾_{𝑡} A) \land (a \cap A) \times (a \cap A) \subseteq w) \to \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w$
31	20 26 30	syl2anc	$⊢ ((((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \land a \in F) \land a \times a \subseteq v) \to \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w$
32	5	simprd	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to \forall v \in U \exists a \in F a \times a \subseteq v$
33	32	r19.21bi	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land v \in U) \to \exists a \in F a \times a \subseteq v$
34	33	ad4ant13	$⊢ ((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \to \exists a \in F a \times a \subseteq v$
35	31 34	r19.29a	$⊢ ((((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \land v \in U) \land w = v \cap (A \times A)) \to \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w$
36	16 16	xpexd	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to A \times A \in V$
37		simpr	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to w \in (U ↾_{𝑡} (A \times A))$
38		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (w \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists v \in U w = v \cap (A \times A))$
39	38	biimpa	$⊢ ((U \in UnifOn (X) \land A \times A \in V) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists v \in U w = v \cap (A \times A)$
40	13 36 37 39	syl21anc	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists v \in U w = v \cap (A \times A)$
41	35 40	r19.29a	$⊢ ((U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \land w \in (U ↾_{𝑡} (A \times A))) \to \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w$
42	41	ralrimiva	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to \forall w \in (U ↾_{𝑡} (A \times A)) \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w$
43		trust	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
44	1 7 43	syl2anc	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
45		iscfilu	$⊢ U ↾_{𝑡} (A \times A) \in UnifOn (A) \to (F ↾_{𝑡} A \in CauFilU (U ↾_{𝑡} (A \times A)) \leftrightarrow (F ↾_{𝑡} A \in fBas (A) \land \forall w \in (U ↾_{𝑡} (A \times A)) \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w))$
46	44 45	syl	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to (F ↾_{𝑡} A \in CauFilU (U ↾_{𝑡} (A \times A)) \leftrightarrow (F ↾_{𝑡} A \in fBas (A) \land \forall w \in (U ↾_{𝑡} (A \times A)) \exists b \in (F ↾_{𝑡} A) b \times b \subseteq w))$
47	11 42 46	mpbir2and	$⊢ (U \in UnifOn (X) \land (F \in CauFilU (U) \land \neg \emptyset \in (F ↾_{𝑡} A)) \land A \subseteq X) \to F ↾_{𝑡} A \in CauFilU (U ↾_{𝑡} (A \times A))$

Metamath Proof Explorer

Theorem trcfilu

Proof