restutopopn

Description: The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		elutop	$⊢ U \in UnifOn (X) \to (A \in unifTop (U) \leftrightarrow (A \subseteq X \land \forall x \in A \exists t \in U t [\{x\}] \subseteq A))$
2	1	simprbda	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to A \subseteq X$
3		restutop	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to unifTop (U) ↾_{𝑡} A \subseteq unifTop (U ↾_{𝑡} (A \times A))$
4	2 3	syldan	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to unifTop (U) ↾_{𝑡} A \subseteq unifTop (U ↾_{𝑡} (A \times A))$
5		trust	$⊢ (U \in UnifOn (X) \land A \subseteq X) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
6	2 5	syldan	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to U ↾_{𝑡} (A \times A) \in UnifOn (A)$
7		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 u \in (U ↾_{𝑡} (A \times A)) u [\{x\}] \subseteq b))$
8	6 7	syl	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to (b \in unifTop (U ↾_{𝑡} (A \times A)) \leftrightarrow (b \subseteq A \land \forall x \in b \exists u \in (U ↾_{𝑡} (A \times A)) u [\{x\}] \subseteq b))$
9	8	simprbda	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b \subseteq A$
10	2	adantr	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to A \subseteq X$
11	9 10	sstrd	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b \subseteq X$
12		simp-9l	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to U \in UnifOn (X)$
13		simplr	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to t \in U$
14		simp-4r	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to w \in U$
15		ustincl	$⊢ (U \in UnifOn (X) \land t \in U \land w \in U) \to t \cap w \in U$
16	12 13 14 15	syl3anc	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to t \cap w \in U$
17		inimass	$⊢ (t \cap w) [\{x\}] \subseteq t [\{x\}] \cap w [\{x\}]$
18		ssrin	$⊢ t [\{x\}] \subseteq A \to t [\{x\}] \cap w [\{x\}] \subseteq A \cap w [\{x\}]$
19	18	adantl	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to t [\{x\}] \cap w [\{x\}] \subseteq A \cap w [\{x\}]$
20		simpllr	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to u = w \cap (A \times A)$
21	20	imaeq1d	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to u [\{x\}] = (w \cap (A \times A)) [\{x\}]$
22	9	ad5antr	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to b \subseteq A$
23		simp-5r	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to x \in b$
24	22 23	sseldd	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to x \in A$
25	24	ad2antrr	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to x \in A$
26		inimasn	$⊢ x \in V \to (w \cap (A \times A)) [\{x\}] = w [\{x\}] \cap (A \times A) [\{x\}]$
27	26	elv	$⊢ (w \cap (A \times A)) [\{x\}] = w [\{x\}] \cap (A \times A) [\{x\}]$
28		xpimasn	$⊢ x \in A \to (A \times A) [\{x\}] = A$
29	28	ineq2d	$⊢ x \in A \to w [\{x\}] \cap (A \times A) [\{x\}] = w [\{x\}] \cap A$
30	27 29	syl5eq	$⊢ x \in A \to (w \cap (A \times A)) [\{x\}] = w [\{x\}] \cap A$
31		incom	$⊢ w [\{x\}] \cap A = A \cap w [\{x\}]$
32	30 31	eqtrdi	$⊢ x \in A \to (w \cap (A \times A)) [\{x\}] = A \cap w [\{x\}]$
33	25 32	syl	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to (w \cap (A \times A)) [\{x\}] = A \cap w [\{x\}]$
34	21 33	eqtrd	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to u [\{x\}] = A \cap w [\{x\}]$
35	19 34	sseqtrrd	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to t [\{x\}] \cap w [\{x\}] \subseteq u [\{x\}]$
36		simp-5r	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to u [\{x\}] \subseteq b$
37	35 36	sstrd	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to t [\{x\}] \cap w [\{x\}] \subseteq b$
38	17 37	sstrid	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to (t \cap w) [\{x\}] \subseteq b$
39		imaeq1	$⊢ v = t \cap w \to v [\{x\}] = (t \cap w) [\{x\}]$
40	39	sseq1d	$⊢ v = t \cap w \to (v [\{x\}] \subseteq b \leftrightarrow (t \cap w) [\{x\}] \subseteq b)$
41	40	rspcev	$⊢ (t \cap w \in U \land (t \cap w) [\{x\}] \subseteq b) \to \exists v \in U v [\{x\}] \subseteq b$
42	16 38 41	syl2anc	$⊢ (((((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \land t \in U) \land t [\{x\}] \subseteq A) \to \exists v \in U v [\{x\}] \subseteq b$
43		simp-4l	$⊢ (((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \to (U \in UnifOn (X) \land A \in unifTop (U))$
44	43	ad2antrr	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to (U \in UnifOn (X) \land A \in unifTop (U))$
45	1	simplbda	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to \forall x \in A \exists t \in U t [\{x\}] \subseteq A$
46	45	r19.21bi	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land x \in A) \to \exists t \in U t [\{x\}] \subseteq A$
47	44 24 46	syl2anc	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to \exists t \in U t [\{x\}] \subseteq A$
48	42 47	r19.29a	$⊢ (((((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \land w \in U) \land u = w \cap (A \times A)) \to \exists v \in U v [\{x\}] \subseteq b$
49		simplr	$⊢ (((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \to u \in (U ↾_{𝑡} (A \times A))$
50		sqxpexg	$⊢ A \in unifTop (U) \to A \times A \in V$
51		elrest	$⊢ (U \in UnifOn (X) \land A \times A \in V) \to (u \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists w \in U u = w \cap (A \times A))$
52	50 51	sylan2	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to (u \in (U ↾_{𝑡} (A \times A)) \leftrightarrow \exists w \in U u = w \cap (A \times A))$
53	52	biimpa	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land u \in (U ↾_{𝑡} (A \times A))) \to \exists w \in U u = w \cap (A \times A)$
54	43 49 53	syl2anc	$⊢ (((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \to \exists w \in U u = w \cap (A \times A)$
55	48 54	r19.29a	$⊢ (((((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \land u \in (U ↾_{𝑡} (A \times A))) \land u [\{x\}] \subseteq b) \to \exists v \in U v [\{x\}] \subseteq b$
56	8	simplbda	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to \forall x \in b \exists u \in (U ↾_{𝑡} (A \times A)) u [\{x\}] \subseteq b$
57	56	r19.21bi	$⊢ (((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \to \exists u \in (U ↾_{𝑡} (A \times A)) u [\{x\}] \subseteq b$
58	55 57	r19.29a	$⊢ (((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \land x \in b) \to \exists v \in U v [\{x\}] \subseteq b$
59	58	ralrimiva	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to \forall x \in b \exists v \in U v [\{x\}] \subseteq b$
60		elutop	$⊢ U \in UnifOn (X) \to (b \in unifTop (U) \leftrightarrow (b \subseteq X \land \forall x \in b \exists v \in U v [\{x\}] \subseteq b))$
61	60	ad2antrr	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to (b \in unifTop (U) \leftrightarrow (b \subseteq X \land \forall x \in b \exists v \in U v [\{x\}] \subseteq b))$
62	11 59 61	mpbir2and	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b \in unifTop (U)$
63		df-ss	$⊢ b \subseteq A \leftrightarrow b \cap A = b$
64	9 63	sylib	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b \cap A = b$
65	64	eqcomd	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b = b \cap A$
66		ineq1	$⊢ a = b \to a \cap A = b \cap A$
67	66	rspceeqv	$⊢ (b \in unifTop (U) \land b = b \cap A) \to \exists a \in unifTop (U) b = a \cap A$
68	62 65 67	syl2anc	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to \exists a \in unifTop (U) b = a \cap A$
69		fvex	$⊢ unifTop (U) \in V$
70		elrest	$⊢ (unifTop (U) \in V \land A \in unifTop (U)) \to (b \in (unifTop (U) ↾_{𝑡} A) \leftrightarrow \exists a \in unifTop (U) b = a \cap A)$
71	69 70	mpan	$⊢ A \in unifTop (U) \to (b \in (unifTop (U) ↾_{𝑡} A) \leftrightarrow \exists a \in unifTop (U) b = a \cap A)$
72	71	ad2antlr	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to (b \in (unifTop (U) ↾_{𝑡} A) \leftrightarrow \exists a \in unifTop (U) b = a \cap A)$
73	68 72	mpbird	$⊢ ((U \in UnifOn (X) \land A \in unifTop (U)) \land b \in unifTop (U ↾_{𝑡} (A \times A))) \to b \in (unifTop (U) ↾_{𝑡} A)$
74	4 73	eqelssd	$⊢ (U \in UnifOn (X) \land A \in unifTop (U)) \to unifTop (U) ↾_{𝑡} A = unifTop (U ↾_{𝑡} (A \times A))$

Metamath Proof Explorer

Theorem restutopopn

Proof