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	biimpi	$⊢ p \in ⋃ x \to \exists y \in x p \in y$
26	25	adantl	$⊢ ((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \to \exists y \in x p \in y$
27	23 26	r19.29a	$⊢ ((U \in UnifOn (X) \land x \subseteq unifTop (U)) \land p \in ⋃ x) \to \exists v \in U v [\{p\}] \subseteq ⋃ x$
28	27	ralrimiva	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to \forall p \in ⋃ x \exists v \in U v [\{p\}] \subseteq ⋃ x$
29		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))$
30	29	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))$
31	8 28 30	mpbir2and	$⊢ (U \in UnifOn (X) \land x \subseteq unifTop (U)) \to ⋃ x \in unifTop (U)$
32	31	ex	$⊢ U \in UnifOn (X) \to (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U))$
33	32	alrimiv	$⊢ U \in UnifOn (X) \to \forall x (x \subseteq unifTop (U) \to ⋃ x \in unifTop (U))$
34		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))$
35	34	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)$
36	35	simpld	$⊢ (U \in UnifOn (X) \land x \in unifTop (U)) \to x \subseteq X$
37	36	adantrr	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \subseteq X$
38		ssinss1	$⊢ x \subseteq X \to x \cap y \subseteq X$
39	37 38	syl	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \cap y \subseteq X$
40		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)$
41		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$
42		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$
43		ustincl	$⊢ (U \in UnifOn (X) \land u \in U \land v \in U) \to u \cap v \in U$
44	40 41 42 43	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$
45		inss1	$⊢ u \cap v \subseteq u$
46		imass1	$⊢ u \cap v \subseteq u \to (u \cap v) [\{p\}] \subseteq u [\{p\}]$
47	45 46	ax-mp	$⊢ (u \cap v) [\{p\}] \subseteq u [\{p\}]$
48		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)$
49	48	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$
50	47 49	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$
51		inss2	$⊢ u \cap v \subseteq v$
52		imass1	$⊢ u \cap v \subseteq v \to (u \cap v) [\{p\}] \subseteq v [\{p\}]$
53	51 52	ax-mp	$⊢ (u \cap v) [\{p\}] \subseteq v [\{p\}]$
54	48	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$
55	53 54	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$
56	50 55	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$
57		imaeq1	$⊢ w = u \cap v \to w [\{p\}] = (u \cap v) [\{p\}]$
58	57	sseq1d	$⊢ w = u \cap v \to (w [\{p\}] \subseteq x \cap y \leftrightarrow (u \cap v) [\{p\}] \subseteq x \cap y)$
59	58	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$
60	44 56 59	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$
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	61	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$
63		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)$
64		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)$
65		simpr	$⊢ ((U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \land p \in (x \cap y)) \to p \in (x \cap y)$
66		elin	$⊢ p \in (x \cap y) \leftrightarrow (p \in x \land p \in y)$
67	65 66	sylib	$⊢ ((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)$
68	67	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$
69	35	simprd	$⊢ (U \in UnifOn (X) \land x \in unifTop (U)) \to \forall p \in x \exists u \in U u [\{p\}] \subseteq x$
70	69	r19.21bi	$⊢ ((U \in UnifOn (X) \land x \in unifTop (U)) \land p \in x) \to \exists u \in U u [\{p\}] \subseteq x$
71	63 64 68 70	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$
72		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)$
73	67	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$
74	63 72 73 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$
75		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)$
76	71 74 75	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)$
77	62 76	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$
78	77	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$
79		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))$
80	79	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))$
81	39 78 80	mpbir2and	$⊢ (U \in UnifOn (X) \land (x \in unifTop (U) \land y \in unifTop (U))) \to x \cap y \in unifTop (U)$
82	81	ralrimivva	$⊢ U \in UnifOn (X) \to \forall x \in unifTop (U) \forall y \in unifTop (U) x \cap y \in unifTop (U)$
83		fvex	$⊢ unifTop (U) \in V$
84		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)))$
85	83 84	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))$
86	33 82 85	sylanbrc	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$

Metamath Proof Explorer

Theorem utoptop

Proof