utoptop

Description: The topology induced by a uniform structure U is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017)

		Ref	Expression
	Assertion	utoptop	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to x \subseteq unifTop (U)$
2		utopval	$⊢ U \in UnifOn (X) \to unifTop (U) = \{a \in 𝒫 X \| \forall p \in a \exists v \in U v [\{p\}] \subseteq a\}$
3		ssrab2	$⊢ \{a \in 𝒫 X \| \forall p \in a \exists v \in U v [\{p\}] \subseteq a\} \subseteq 𝒫 X$
4	2 3	eqsstrdi	$⊢ U \in UnifOn (X) \to unifTop (U) \subseteq 𝒫 X$
5	4	adantr	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to unifTop (U) \subseteq 𝒫 X$
6	1 5	sstrd	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to x \subseteq 𝒫 X$
7		sspwuni	$⊢ x \subseteq 𝒫 X \leftrightarrow ⋃ x \subseteq X$
8	6 7	sylib	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to ⋃ x \subseteq X$
9		simp-4l	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to U \in UnifOn (X)$
10		simp-4r	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to x \subseteq unifTop (U)$
11		simplr	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to y \in x$
12	10 11	sseldd	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to y \in unifTop (U)$
13		simpr	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to p \in y$
14		elutop	$⊢ U \in UnifOn (X) \to (y \in unifTop (U) \leftrightarrow (y \subseteq X \land \forall p \in y \exists v \in U v [\{p\}] \subseteq y))$
15	14	biimpa	$⊢ (U \in UnifOn (X) \land y \in unifTop (U)) \to (y \subseteq X \land \forall p \in y \exists v \in U v [\{p\}] \subseteq y)$
16	15	simprd	$⊢ (U \in UnifOn (X) \land y \in unifTop (U)) \to \forall p \in y \exists v \in U v [\{p\}] \subseteq y$
17	16	r19.21bi	$⊢ ((U \in UnifOn (X) \land y \in unifTop (U)) \land p \in y) \to \exists v \in U v [\{p\}] \subseteq y$
18	9 12 13 17	syl21anc	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to \exists v \in U v [\{p\}] \subseteq y$
19		r19.41v	$⊢ \exists v \in U (v [\{p\}] \subseteq y \land y \in x) \leftrightarrow (\exists v \in U v [\{p\}] \subseteq y \land y \in x)$
20		ssuni	$⊢ (v [\{p\}] \subseteq y \land y \in x) \to v [\{p\}] \subseteq ⋃ x$
21	20	reximi	$⊢ \exists v \in U (v [\{p\}] \subseteq y \land y \in x) \to \exists v \in U v [\{p\}] \subseteq ⋃ x$
22	19 21	sylbir	$⊢ (\exists v \in U v [\{p\}] \subseteq y \land y \in x) \to \exists v \in U v [\{p\}] \subseteq ⋃ x$
23	18 11 22	syl2anc	$⊢ ((((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \land y \in x) \land p \in y) \to \exists v \in U v [\{p\}] \subseteq ⋃ x$
24		eluni2	$⊢ p \in ⋃ x \leftrightarrow \exists y \in x p \in y$
25	24	bilani	$⊢ ((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \to \exists y \in x p \in y$
26	23 25	r19.29a	$⊢ ((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \to \exists v \in U v [\{p\}] \subseteq ⋃ x$
27	26	ralrimiva	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to \forall p \in ⋃ x \exists v \in U v [\{p\}] \subseteq ⋃ x$
28		elutop	$⊢ U \in UnifOn (X) \to (⋃ x \in unifTop (U) \leftrightarrow (⋃ x \subseteq X \land \forall p \in ⋃ x \exists v \in U v [\{p\}] \subseteq ⋃ x))$
29	28	adantr	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to (⋃ x \in unifTop (U) \leftrightarrow (⋃ x \subseteq X \land \forall p \in ⋃ x \exists v \in U v [\{p\}] \subseteq ⋃ x))$
30	8 27 29	mpbir2and	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to ⋃ x \in unifTop (U)$
31	30	ex	$⊢ U \in UnifOn (X) \to (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U))$
32	31	alrimiv	$⊢ U \in UnifOn (X) \to \forall x (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U))$
33		elutop	$⊢ U \in UnifOn (X) \to (x \in unifTop (U) \leftrightarrow (x \subseteq X \land \forall p \in x \exists u \in U u [\{p\}] \subseteq x))$
34	33	biimpa	$⊢ (U \in UnifOn (X) \land x \in unifTop (U)) \to (x \subseteq X \land \forall p \in x \exists u \in U u [\{p\}] \subseteq x)$
35	34	simpld	$⊢ (U \in UnifOn (X) \land x \in unifTop (U)) \to x \subseteq X$
36	35	adantrr	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \subseteq X$
37		ssinss1	$⊢ x \subseteq X \to x \cap y \subseteq X$
38	36 37	syl	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \cap y \subseteq X$
39		simpl	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to U \in UnifOn (X)$
40		simpr31	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to u \in U$
41		simpr32	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to v \in U$
42		ustincl	$⊢ (U \in UnifOn (X) \land u \in U \land v \in U) \to u \cap v \in U$
43	39 40 41 42	syl3anc	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to u \cap v \in U$
44		inss1	$⊢ u \cap v \subseteq u$
45		imass1	$⊢ u \cap v \subseteq u \to (u \cap v) [\{p\}] \subseteq u [\{p\}]$
46	44 45	ax-mp	$⊢ (u \cap v) [\{p\}] \subseteq u [\{p\}]$
47		simpr33	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)$
48	47	simpld	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to u [\{p\}] \subseteq x$
49	46 48	sstrid	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to (u \cap v) [\{p\}] \subseteq x$
50		inss2	$⊢ u \cap v \subseteq v$
51		imass1	$⊢ u \cap v \subseteq v \to (u \cap v) [\{p\}] \subseteq v [\{p\}]$
52	50 51	ax-mp	$⊢ (u \cap v) [\{p\}] \subseteq v [\{p\}]$
53	47	simprd	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to v [\{p\}] \subseteq y$
54	52 53	sstrid	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to (u \cap v) [\{p\}] \subseteq y$
55	49 54	ssind	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to (u \cap v) [\{p\}] \subseteq x \cap y$
56		imaeq1	$⊢ w = u \cap v \to w [\{p\}] = (u \cap v) [\{p\}]$
57	56	sseq1d	$⊢ w = u \cap v \to (w [\{p\}] \subseteq x \cap y \leftrightarrow (u \cap v) [\{p\}] \subseteq x \cap y)$
58	57	rspcev	$⊢ (u \cap v \in U \land (u \cap v) [\{p\}] \subseteq x \cap y) \to \exists w \in U w [\{p\}] \subseteq x \cap y$
59	43 55 58	syl2anc	$⊢ (U \in UnifOn (X) \land ((x \in unifTop (U) \land y \in unifTop (U)) \land p \in (x \cap y) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)))) \to \exists w \in U w [\{p\}] \subseteq x \cap y$
60	59	3anassrs	$⊢ (((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \land (u \in U \land v \in U \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y))) \to \exists w \in U w [\{p\}] \subseteq x \cap y$
61	60	3anassrs	$⊢ (((((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \land u \in U) \land v \in U) \land (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)) \to \exists w \in U w [\{p\}] \subseteq x \cap y$
62		simpll	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to U \in UnifOn (X)$
63		simplrl	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to x \in unifTop (U)$
64		elin	$⊢ p \in (x \cap y) \leftrightarrow (p \in x \land p \in y)$
65	64	bilani	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to (p \in x \land p \in y)$
66	65	simpld	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to p \in x$
67	34	simprd	$⊢ (U \in UnifOn (X) \land x \in unifTop (U)) \to \forall p \in x \exists u \in U u [\{p\}] \subseteq x$
68	67	r19.21bi	$⊢ ((U \in UnifOn (X) \land x \in unifTop (U)) \land p \in x) \to \exists u \in U u [\{p\}] \subseteq x$
69	62 63 66 68	syl21anc	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to \exists u \in U u [\{p\}] \subseteq x$
70		simplrr	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to y \in unifTop (U)$
71	65	simprd	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to p \in y$
72	62 70 71 17	syl21anc	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to \exists v \in U v [\{p\}] \subseteq y$
73		reeanv	$⊢ \exists u \in U \exists v \in U (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y) \leftrightarrow (\exists u \in U u [\{p\}] \subseteq x \land \exists v \in U v [\{p\}] \subseteq y)$
74	69 72 73	sylanbrc	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to \exists u \in U \exists v \in U (u [\{p\}] \subseteq x \land v [\{p\}] \subseteq y)$
75	61 74	r19.29vva	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to \exists w \in U w [\{p\}] \subseteq x \cap y$
76	75	ralrimiva	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to \forall p \in (x \cap y) \exists w \in U w [\{p\}] \subseteq x \cap y$
77		elutop	$⊢ U \in UnifOn (X) \to (x \cap y \in unifTop (U) \leftrightarrow (x \cap y \subseteq X \land \forall p \in (x \cap y) \exists w \in U w [\{p\}] \subseteq x \cap y))$
78	77	adantr	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to (x \cap y \in unifTop (U) \leftrightarrow (x \cap y \subseteq X \land \forall p \in (x \cap y) \exists w \in U w [\{p\}] \subseteq x \cap y))$
79	38 76 78	mpbir2and	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \cap y \in unifTop (U)$
80	79	ralrimivva	$⊢ U \in UnifOn (X) \to \forall x \in unifTop (U) \forall y \in unifTop (U) x \cap y \in unifTop (U)$
81		fvex	$⊢ unifTop (U) \in V$
82		istopg	$⊢ unifTop (U) \in V \to (unifTop (U) \in Top \leftrightarrow (\forall x (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U)) \land \forall x \in unifTop (U) \forall y \in unifTop (U) x \cap y \in unifTop (U)))$
83	81 82	ax-mp	$⊢ unifTop (U) \in Top \leftrightarrow (\forall x (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U)) \land \forall x \in unifTop (U) \forall y \in unifTop (U) x \cap y \in unifTop (U))$
84	32 80 83	sylanbrc	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$

Metamath Proof Explorer

Theorem utoptop

Proof