restutop

Description: Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \to (U \in UnifOn (X) \land A \subseteq X)$
2		fvexd	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to unifTop (U) \in V$
3		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
4	3	adantr	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to X \in V$
5		simpr	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \subseteq X$
6	4 5	ssexd	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to A \in V$
7		elrest	$⊢ (unifTop (U) \in V \land A \in V) \to (b \in (unifTop (U) ↾_{𝑡} A) \leftrightarrow \exists a \in unifTop (U) b = a \cap A)$
8	2 6 7	syl2anc	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (b \in (unifTop (U) ↾_{𝑡} A) \leftrightarrow \exists a \in unifTop (U) b = a \cap A)$
9	8	biimpa	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \to \exists a \in unifTop (U) b = a \cap A$
10		inss2	$⊢ a \cap A \subseteq A$
11		sseq1	$⊢ b = a \cap A \to (b \subseteq A \leftrightarrow a \cap A \subseteq A)$
12	10 11	mpbiri	$⊢ b = a \cap A \to b \subseteq A$
13	12	rexlimivw	$⊢ \exists a \in unifTop (U) b = a \cap A \to b \subseteq A$
14	9 13	syl	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \to b \subseteq A$
15		simp-5l	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to U \in UnifOn (X)$
16	15	ad2antrr	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to U \in UnifOn (X)$
17	6	ad6antr	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to A \in V$
18	17 17	xpexd	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to A \times A \in V$
19		simplr	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to u \in U$
20		elrestr	$⊢ (U \in UnifOn (X) \land A \times A \in V \land u \in U) \to u \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
21	16 18 19 20	syl3anc	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to u \cap (A \times A) \in (U ↾_{𝑡} (A \times A))$
22		inss1	$⊢ u \cap (A \times A) \subseteq u$
23		imass1	$⊢ u \cap (A \times A) \subseteq u \to (u \cap (A \times A)) [\{x\}] \subseteq u [\{x\}]$
24	22 23	ax-mp	$⊢ (u \cap (A \times A)) [\{x\}] \subseteq u [\{x\}]$
25		sstr	$⊢ ((u \cap (A \times A)) [\{x\}] \subseteq u [\{x\}] \land u [\{x\}] \subseteq a) \to (u \cap (A \times A)) [\{x\}] \subseteq a$
26	24 25	mpan	$⊢ u [\{x\}] \subseteq a \to (u \cap (A \times A)) [\{x\}] \subseteq a$
27		imassrn	$⊢ (u \cap (A \times A)) [\{x\}] \subseteq ran (u \cap (A \times A))$
28		rnin	$⊢ ran (u \cap (A \times A)) \subseteq ran u \cap ran (A \times A)$
29	27 28	sstri	$⊢ (u \cap (A \times A)) [\{x\}] \subseteq ran u \cap ran (A \times A)$
30		inss2	$⊢ ran u \cap ran (A \times A) \subseteq ran (A \times A)$
31	29 30	sstri	$⊢ (u \cap (A \times A)) [\{x\}] \subseteq ran (A \times A)$
32		rnxpid	$⊢ ran (A \times A) = A$
33	31 32	sseqtri	$⊢ (u \cap (A \times A)) [\{x\}] \subseteq A$
34	33	a1i	$⊢ u [\{x\}] \subseteq a \to (u \cap (A \times A)) [\{x\}] \subseteq A$
35	26 34	ssind	$⊢ u [\{x\}] \subseteq a \to (u \cap (A \times A)) [\{x\}] \subseteq a \cap A$
36	35	adantl	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to (u \cap (A \times A)) [\{x\}] \subseteq a \cap A$
37		simpllr	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to b = a \cap A$
38	36 37	sseqtrrd	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to (u \cap (A \times A)) [\{x\}] \subseteq b$
39		imaeq1	$⊢ v = u \cap (A \times A) \to v [\{x\}] = (u \cap (A \times A)) [\{x\}]$
40	39	sseq1d	$⊢ v = u \cap (A \times A) \to (v [\{x\}] \subseteq b \leftrightarrow (u \cap (A \times A)) [\{x\}] \subseteq b)$
41	40	rspcev	$⊢ (u \cap (A \times A) \in (U ↾_{𝑡} (A \times A)) \land (u \cap (A \times A)) [\{x\}] \subseteq b) \to \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b$
42	21 38 41	syl2anc	$⊢ (((((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \land u \in U) \land u [\{x\}] \subseteq a) \to \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b$
43		simplr	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to a \in unifTop (U)$
44		simpllr	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to x \in b$
45		simpr	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to b = a \cap A$
46	44 45	eleqtrd	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to x \in (a \cap A)$
47	46	elin1d	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to x \in a$
48		elutop	$⊢ U \in UnifOn (X) \to (a \in unifTop (U) \leftrightarrow (a \subseteq X \land \forall x \in a \exists u \in U u [\{x\}] \subseteq a))$
49	48	simplbda	$⊢ (U \in UnifOn (X) \land a \in unifTop (U)) \to \forall x \in a \exists u \in U u [\{x\}] \subseteq a$
50	49	r19.21bi	$⊢ ((U \in UnifOn (X) \land a \in unifTop (U)) \land x \in a) \to \exists u \in U u [\{x\}] \subseteq a$
51	15 43 47 50	syl21anc	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to \exists u \in U u [\{x\}] \subseteq a$
52	42 51	r19.29a	$⊢ (((((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \land a \in unifTop (U)) \land b = a \cap A) \to \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b$
53	9	adantr	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \to \exists a \in unifTop (U) b = a \cap A$
54	52 53	r19.29a	$⊢ (((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \land x \in b) \to \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b$
55	54	ralrimiva	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \to \forall x \in b \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b$
56		trust	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
57		elutop	$⊢ U ↾_{𝑡} (A \times A) \in UnifOn (A) \to (b \in unifTop (U ↾_{𝑡} (A \times A)) \leftrightarrow (b \subseteq A \land \forall x \in b \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b))$
58	56 57	syl	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (b \in unifTop (U ↾_{𝑡} (A \times A)) \leftrightarrow (b \subseteq A \land \forall x \in b \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b))$
59	58	biimpar	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land (b \subseteq A \land \forall x \in b \exists v \in (U ↾_{𝑡} (A \times A)) v [\{x\}] \subseteq b)) \to b \in unifTop (U ↾_{𝑡} (A \times A))$
60	1 14 55 59	syl12anc	$⊢ ((U \in UnifOn (X) \land A \subseteq X) \land b \in (unifTop (U) ↾_{𝑡} A)) \to b \in unifTop (U ↾_{𝑡} (A \times A))$
61	60	ex	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to (b \in (unifTop (U) ↾_{𝑡} A) \to b \in unifTop (U ↾_{𝑡} (A \times A)))$
62	61	ssrdv	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to unifTop (U) ↾_{𝑡} A \subseteq unifTop (U ↾_{𝑡} (A \times A))$

Metamath Proof Explorer

Theorem restutop

Proof