utop3cls

Description: Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018)

		Ref	Expression
	Hypothesis	utoptop.1	$⊢ J = unifTop (U)$
	Assertion	utop3cls	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to cls (J \times_{t} J) (M) \subseteq V \circ (M \circ V)$

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	$⊢ J = unifTop (U)$
2		relxp	$⊢ Rel (X \times X)$
3		utoptop	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$
4	1 3	eqeltrid	$⊢ U \in UnifOn (X) \to J \in Top$
5		txtop	$⊢ (J \in Top \land J \in Top) \to J \times_{t} J \in Top$
6	4 4 5	syl2anc	$⊢ U \in UnifOn (X) \to J \times_{t} J \in Top$
7	6	ad3antrrr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to J \times_{t} J \in Top$
8		simpllr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to M \subseteq X \times X$
9		utoptopon	$⊢ U \in UnifOn (X) \to unifTop (U) \in TopOn (X)$
10	1 9	eqeltrid	$⊢ U \in UnifOn (X) \to J \in TopOn (X)$
11		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
12	10 11	syl	$⊢ U \in UnifOn (X) \to X = ⋃ J$
13	12	sqxpeqd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ J \times ⋃ J$
14		eqid	$⊢ ⋃ J = ⋃ J$
15	14 14	txuni	$⊢ (J \in Top \land J \in Top) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
16	4 4 15	syl2anc	$⊢ U \in UnifOn (X) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
17	13 16	eqtrd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ (J \times_{t} J)$
18	17	ad3antrrr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to X \times X = ⋃ (J \times_{t} J)$
19	8 18	sseqtrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to M \subseteq ⋃ (J \times_{t} J)$
20		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
21	20	clsss3	$⊢ (J \times_{t} J \in Top \land M \subseteq ⋃ (J \times_{t} J)) \to cls (J \times_{t} J) (M) \subseteq ⋃ (J \times_{t} J)$
22	7 19 21	syl2anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to cls (J \times_{t} J) (M) \subseteq ⋃ (J \times_{t} J)$
23	22 18	sseqtrrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to cls (J \times_{t} J) (M) \subseteq X \times X$
24		simpr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in cls (J \times_{t} J) (M)$
25	23 24	sseldd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in (X \times X)$
26		1st2nd	$⊢ (Rel (X \times X) \land z \in (X \times X)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
27	2 25 26	sylancr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
28		simplll	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to U \in UnifOn (X)$
29		simplrl	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to V \in U$
30	4	3ad2ant1	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to J \in Top$
31		xp1st	$⊢ z \in (X \times X) \to 1^{st} (z) \in X$
32	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 1^{st} (z) \in X) \to V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\})$
33	31 32	syl3an3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\})$
34		xp2nd	$⊢ z \in (X \times X) \to 2^{nd} (z) \in X$
35	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 2^{nd} (z) \in X) \to V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\})$
36	34 35	syl3an3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\})$
37	14 14	neitx	$⊢ ((J \in Top \land J \in Top) \land (V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\}) \land V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\}))) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
38	30 30 33 36 37	syl22anc	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
39		1st2nd2	$⊢ z \in (X \times X) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
40	39	sneqd	$⊢ z \in (X \times X) \to \{z\} = \{⟨1^{st} (z), 2^{nd} (z)⟩\}$
41		fvex	$⊢ 1^{st} (z) \in V$
42		fvex	$⊢ 2^{nd} (z) \in V$
43	41 42	xpsn	$⊢ \{1^{st} (z)\} \times \{2^{nd} (z)\} = \{⟨1^{st} (z), 2^{nd} (z)⟩\}$
44	40 43	eqtr4di	$⊢ z \in (X \times X) \to \{z\} = \{1^{st} (z)\} \times \{2^{nd} (z)\}$
45	44	fveq2d	$⊢ z \in (X \times X) \to nei (J \times_{t} J) (\{z\}) = nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
46	45	3ad2ant3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to nei (J \times_{t} J) (\{z\}) = nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
47	38 46	eleqtrrd	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\})$
48	28 29 25 47	syl3anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\})$
49	20	neindisj	$⊢ ((J \times_{t} J \in Top \land M \subseteq ⋃ (J \times_{t} J)) \land (z \in cls (J \times_{t} J) (M) \land V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\}))) \to (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M \neq \emptyset$
50	7 19 24 48 49	syl22anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M \neq \emptyset$
51		simp-4l	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to U \in UnifOn (X)$
52		simpr1l	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land ((V \in U \land V^{-1} = V) \land z \in cls (J \times_{t} J) (M) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M))) \to V \in U$
53	52	3anassrs	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to V \in U$
54		ustrel	$⊢ (U \in UnifOn (X) \land V \in U) \to Rel V$
55	51 53 54	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to Rel V$
56		simpr	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)$
57		elin	$⊢ r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M) \leftrightarrow (r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \land r \in M)$
58	56 57	sylib	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to (r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \land r \in M)$
59	58	simpld	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}])$
60		xp1st	$⊢ r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \to 1^{st} (r) \in V [\{1^{st} (z)\}]$
61	59 60	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (r) \in V [\{1^{st} (z)\}]$
62		elrelimasn	$⊢ Rel V \to (1^{st} (r) \in V [\{1^{st} (z)\}] \leftrightarrow 1^{st} (z) V 1^{st} (r))$
63	62	biimpa	$⊢ (Rel V \land 1^{st} (r) \in V [\{1^{st} (z)\}]) \to 1^{st} (z) V 1^{st} (r)$
64	55 61 63	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (z) V 1^{st} (r)$
65		simp-4r	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to M \subseteq X \times X$
66		xpss	$⊢ X \times X \subseteq V \times V$
67	65 66	sstrdi	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to M \subseteq V \times V$
68		df-rel	$⊢ Rel M \leftrightarrow M \subseteq V \times V$
69	67 68	sylibr	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to Rel M$
70	58	simprd	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in M$
71		1st2ndbr	$⊢ (Rel M \land r \in M) \to 1^{st} (r) M 2^{nd} (r)$
72	69 70 71	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (r) M 2^{nd} (r)$
73		xp2nd	$⊢ r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \to 2^{nd} (r) \in V [\{2^{nd} (z)\}]$
74	59 73	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (r) \in V [\{2^{nd} (z)\}]$
75		elrelimasn	$⊢ Rel V \to (2^{nd} (r) \in V [\{2^{nd} (z)\}] \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
76	75	biimpa	$⊢ (Rel V \land 2^{nd} (r) \in V [\{2^{nd} (z)\}]) \to 2^{nd} (z) V 2^{nd} (r)$
77	55 74 76	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (z) V 2^{nd} (r)$
78		simpr1r	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land ((V \in U \land V^{-1} = V) \land z \in cls (J \times_{t} J) (M) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M))) \to V^{-1} = V$
79	78	3anassrs	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to V^{-1} = V$
80		breq	$⊢ V^{-1} = V \to (2^{nd} (r) V^{-1} 2^{nd} (z) \leftrightarrow 2^{nd} (r) V 2^{nd} (z))$
81		fvex	$⊢ 2^{nd} (r) \in V$
82	81 42	brcnv	$⊢ 2^{nd} (r) V^{-1} 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r)$
83	80 82	bitr3di	$⊢ V^{-1} = V \to (2^{nd} (r) V 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
84	79 83	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to (2^{nd} (r) V 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
85	77 84	mpbird	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (r) V 2^{nd} (z)$
86		fvex	$⊢ 1^{st} (r) \in V$
87	41 86 81	brcoi	$⊢ (1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r)) \to 1^{st} (z) (M \circ V) 2^{nd} (r)$
88	41 81 42	brcoi	$⊢ (1^{st} (z) (M \circ V) 2^{nd} (r) \land 2^{nd} (r) V 2^{nd} (z)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
89	87 88	sylan	$⊢ ((1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r)) \land 2^{nd} (r) V 2^{nd} (z)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
90	64 72 85 89	syl21anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
91	50 90	n0limd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
92		df-br	$⊢ 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z) \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ \in (V \circ (M \circ V))$
93	91 92	sylib	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in (V \circ (M \circ V))$
94	27 93	eqeltrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in (V \circ (M \circ V))$
95	94	ex	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to (z \in cls (J \times_{t} J) (M) \to z \in (V \circ (M \circ V)))$
96	95	ssrdv	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to cls (J \times_{t} J) (M) \subseteq V \circ (M \circ V)$

Metamath Proof Explorer

Theorem utop3cls

Proof