utop2nei

Description: For any symmetrical entourage V and any relation M , build a neighborhood of M . First part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	$⊢ J = unifTop (U)$
2		utoptop	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$
3	1 2	eqeltrid	$⊢ U \in UnifOn (X) \to J \in Top$
4		txtop	$⊢ (J \in Top \land J \in Top) \to J \times_{t} J \in Top$
5	3 3 4	syl2anc	$⊢ U \in UnifOn (X) \to J \times_{t} J \in Top$
6	5	3ad2ant1	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to J \times_{t} J \in Top$
7	6	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to J \times_{t} J \in Top$
8		0nei	$⊢ J \times_{t} J \in Top \to \emptyset \in nei (J \times_{t} J) (\emptyset)$
9	7 8	syl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to \emptyset \in nei (J \times_{t} J) (\emptyset)$
10		coeq1	$⊢ M = \emptyset \to M \circ V = \emptyset \circ V$
11		co01	$⊢ \emptyset \circ V = \emptyset$
12	10 11	eqtrdi	$⊢ M = \emptyset \to M \circ V = \emptyset$
13	12	coeq2d	$⊢ M = \emptyset \to V \circ (M \circ V) = V \circ \emptyset$
14		co02	$⊢ V \circ \emptyset = \emptyset$
15	13 14	eqtrdi	$⊢ M = \emptyset \to V \circ (M \circ V) = \emptyset$
16	15	adantl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to V \circ (M \circ V) = \emptyset$
17		simpr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to M = \emptyset$
18	17	fveq2d	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to nei (J \times_{t} J) (M) = nei (J \times_{t} J) (\emptyset)$
19	9 16 18	3eltr4d	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M = \emptyset) \to V \circ (M \circ V) \in nei (J \times_{t} J) (M)$
20	6	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to J \times_{t} J \in Top$
21		simpl1	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to U \in UnifOn (X)$
22	21 3	syl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to J \in Top$
23		simpl2l	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V \in U$
24		simp3	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to M \subseteq X \times X$
25	24	sselda	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to r \in (X \times X)$
26		xp1st	$⊢ r \in (X \times X) \to 1^{st} (r) \in X$
27	25 26	syl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to 1^{st} (r) \in X$
28	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 1^{st} (r) \in X) \to V [\{1^{st} (r)\}] \in nei (J) (\{1^{st} (r)\})$
29	21 23 27 28	syl3anc	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{1^{st} (r)\}] \in nei (J) (\{1^{st} (r)\})$
30		xp2nd	$⊢ r \in (X \times X) \to 2^{nd} (r) \in X$
31	25 30	syl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to 2^{nd} (r) \in X$
32	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 2^{nd} (r) \in X) \to V [\{2^{nd} (r)\}] \in nei (J) (\{2^{nd} (r)\})$
33	21 23 31 32	syl3anc	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{2^{nd} (r)\}] \in nei (J) (\{2^{nd} (r)\})$
34		eqid	$⊢ ⋃ J = ⋃ J$
35	34 34	neitx	$⊢ ((J \in Top \land J \in Top) \land (V [\{1^{st} (r)\}] \in nei (J) (\{1^{st} (r)\}) \land V [\{2^{nd} (r)\}] \in nei (J) (\{2^{nd} (r)\}))) \to V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \in nei (J \times_{t} J) (\{1^{st} (r)\} \times \{2^{nd} (r)\})$
36	22 22 29 33 35	syl22anc	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \in nei (J \times_{t} J) (\{1^{st} (r)\} \times \{2^{nd} (r)\})$
37		fvex	$⊢ 1^{st} (r) \in V$
38		fvex	$⊢ 2^{nd} (r) \in V$
39	37 38	xpsn	$⊢ \{1^{st} (r)\} \times \{2^{nd} (r)\} = \{⟨1^{st} (r), 2^{nd} (r)⟩\}$
40	39	fveq2i	$⊢ nei (J \times_{t} J) (\{1^{st} (r)\} \times \{2^{nd} (r)\}) = nei (J \times_{t} J) (\{⟨1^{st} (r), 2^{nd} (r)⟩\})$
41	36 40	eleqtrdi	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \in nei (J \times_{t} J) (\{⟨1^{st} (r), 2^{nd} (r)⟩\})$
42	24	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to M \subseteq X \times X$
43		xpss	$⊢ X \times X \subseteq V \times V$
44		sstr	$⊢ (M \subseteq X \times X \land X \times X \subseteq V \times V) \to M \subseteq V \times V$
45	43 44	mpan2	$⊢ M \subseteq X \times X \to M \subseteq V \times V$
46		df-rel	$⊢ Rel M \leftrightarrow M \subseteq V \times V$
47	45 46	sylibr	$⊢ M \subseteq X \times X \to Rel M$
48	42 47	syl	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to Rel M$
49		1st2nd	$⊢ (Rel M \land r \in M) \to r = ⟨1^{st} (r), 2^{nd} (r)⟩$
50	48 49	sylancom	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to r = ⟨1^{st} (r), 2^{nd} (r)⟩$
51	50	sneqd	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to \{r\} = \{⟨1^{st} (r), 2^{nd} (r)⟩\}$
52	51	fveq2d	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to nei (J \times_{t} J) (\{r\}) = nei (J \times_{t} J) (\{⟨1^{st} (r), 2^{nd} (r)⟩\})$
53	41 52	eleqtrrd	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \in nei (J \times_{t} J) (\{r\})$
54		relxp	$⊢ Rel (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])$
55	54	a1i	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to Rel (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])$
56		1st2nd	$⊢ (Rel (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}]) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
57	55 56	sylancom	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
58		simpll2	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to (V \in U \land V^{-1} = V)$
59	58	simprd	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to V^{-1} = V$
60		simpll1	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to U \in UnifOn (X)$
61	58	simpld	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to V \in U$
62		ustrel	$⊢ (U \in UnifOn (X) \land V \in U) \to Rel V$
63	60 61 62	syl2anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to Rel V$
64		xp1st	$⊢ z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}]) \to 1^{st} (z) \in V [\{1^{st} (r)\}]$
65	64	adantl	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 1^{st} (z) \in V [\{1^{st} (r)\}]$
66		elrelimasn	$⊢ Rel V \to (1^{st} (z) \in V [\{1^{st} (r)\}] \leftrightarrow 1^{st} (r) V 1^{st} (z))$
67	66	biimpa	$⊢ (Rel V \land 1^{st} (z) \in V [\{1^{st} (r)\}]) \to 1^{st} (r) V 1^{st} (z)$
68	63 65 67	syl2anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 1^{st} (r) V 1^{st} (z)$
69		fvex	$⊢ 1^{st} (z) \in V$
70	37 69	brcnv	$⊢ 1^{st} (r) V^{-1} 1^{st} (z) \leftrightarrow 1^{st} (z) V 1^{st} (r)$
71		breq	$⊢ V^{-1} = V \to (1^{st} (r) V^{-1} 1^{st} (z) \leftrightarrow 1^{st} (r) V 1^{st} (z))$
72	70 71	bitr3id	$⊢ V^{-1} = V \to (1^{st} (z) V 1^{st} (r) \leftrightarrow 1^{st} (r) V 1^{st} (z))$
73	72	biimpar	$⊢ (V^{-1} = V \land 1^{st} (r) V 1^{st} (z)) \to 1^{st} (z) V 1^{st} (r)$
74	59 68 73	syl2anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 1^{st} (z) V 1^{st} (r)$
75		simpll3	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to M \subseteq X \times X$
76		simplr	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to r \in M$
77		1st2ndbr	$⊢ (Rel M \land r \in M) \to 1^{st} (r) M 2^{nd} (r)$
78	47 77	sylan	$⊢ (M \subseteq X \times X \land r \in M) \to 1^{st} (r) M 2^{nd} (r)$
79	75 76 78	syl2anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 1^{st} (r) M 2^{nd} (r)$
80		xp2nd	$⊢ z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}]) \to 2^{nd} (z) \in V [\{2^{nd} (r)\}]$
81	80	adantl	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 2^{nd} (z) \in V [\{2^{nd} (r)\}]$
82		elrelimasn	$⊢ Rel V \to (2^{nd} (z) \in V [\{2^{nd} (r)\}] \leftrightarrow 2^{nd} (r) V 2^{nd} (z))$
83	82	biimpa	$⊢ (Rel V \land 2^{nd} (z) \in V [\{2^{nd} (r)\}]) \to 2^{nd} (r) V 2^{nd} (z)$
84	63 81 83	syl2anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 2^{nd} (r) V 2^{nd} (z)$
85	69 38 37	3pm3.2i	$⊢ (1^{st} (z) \in V \land 2^{nd} (r) \in V \land 1^{st} (r) \in V)$
86		brcogw	$⊢ ((1^{st} (z) \in V \land 2^{nd} (r) \in V \land 1^{st} (r) \in V) \land (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)$
87	85 86	mpan	$⊢ (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		fvex	$⊢ 2^{nd} (z) \in V$
89	69 88 38	3pm3.2i	$⊢ (1^{st} (z) \in V \land 2^{nd} (z) \in V \land 2^{nd} (r) \in V)$
90		brcogw	$⊢ ((1^{st} (z) \in V \land 2^{nd} (z) \in V \land 2^{nd} (r) \in V) \land (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)$
91	89 90	mpan	$⊢ (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)$
92	87 91	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)$
93	74 79 84 92	syl21anc	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
94		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))$
95	93 94	sylib	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in (V \circ (M \circ V))$
96	57 95	eqeltrd	$⊢ (((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \land z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}])) \to z \in (V \circ (M \circ V))$
97	96	ex	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to (z \in (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}]) \to z \in (V \circ (M \circ V)))$
98	97	ssrdv	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \subseteq V \circ (M \circ V)$
99		simp1	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to U \in UnifOn (X)$
100		simp2l	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \in U$
101		ustssxp	$⊢ (U \in UnifOn (X) \land V \in U) \to V \subseteq X \times X$
102	99 100 101	syl2anc	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \subseteq X \times X$
103		coss1	$⊢ V \subseteq X \times X \to V \circ (M \circ V) \subseteq (X \times X) \circ (M \circ V)$
104	102 103	syl	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \circ (M \circ V) \subseteq (X \times X) \circ (M \circ V)$
105		coss1	$⊢ M \subseteq X \times X \to M \circ V \subseteq (X \times X) \circ V$
106	24 105	syl	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to M \circ V \subseteq (X \times X) \circ V$
107		coss2	$⊢ V \subseteq X \times X \to (X \times X) \circ V \subseteq (X \times X) \circ (X \times X)$
108		xpcoid	$⊢ (X \times X) \circ (X \times X) = X \times X$
109	107 108	sseqtrdi	$⊢ V \subseteq X \times X \to (X \times X) \circ V \subseteq X \times X$
110	102 109	syl	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to (X \times X) \circ V \subseteq X \times X$
111	106 110	sstrd	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to M \circ V \subseteq X \times X$
112		coss2	$⊢ M \circ V \subseteq X \times X \to (X \times X) \circ (M \circ V) \subseteq (X \times X) \circ (X \times X)$
113	112 108	sseqtrdi	$⊢ M \circ V \subseteq X \times X \to (X \times X) \circ (M \circ V) \subseteq X \times X$
114	111 113	syl	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to (X \times X) \circ (M \circ V) \subseteq X \times X$
115	104 114	sstrd	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \circ (M \circ V) \subseteq X \times X$
116		utopbas	$⊢ U \in UnifOn (X) \to X = ⋃ unifTop (U)$
117	1	unieqi	$⊢ ⋃ J = ⋃ unifTop (U)$
118	116 117	eqtr4di	$⊢ U \in UnifOn (X) \to X = ⋃ J$
119	118	sqxpeqd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ J \times ⋃ J$
120	34 34	txuni	$⊢ (J \in Top \land J \in Top) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
121	3 3 120	syl2anc	$⊢ U \in UnifOn (X) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
122	119 121	eqtrd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ (J \times_{t} J)$
123	122	3ad2ant1	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to X \times X = ⋃ (J \times_{t} J)$
124	115 123	sseqtrd	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \circ (M \circ V) \subseteq ⋃ (J \times_{t} J)$
125	124	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V \circ (M \circ V) \subseteq ⋃ (J \times_{t} J)$
126		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
127	126	ssnei2	$⊢ ((J \times_{t} J \in Top \land V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \in nei (J \times_{t} J) (\{r\})) \land (V [\{1^{st} (r)\}] \times V [\{2^{nd} (r)\}] \subseteq V \circ (M \circ V) \land V \circ (M \circ V) \subseteq ⋃ (J \times_{t} J))) \to V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\})$
128	20 53 98 125 127	syl22anc	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land r \in M) \to V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\})$
129	128	ralrimiva	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to \forall r \in M V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\})$
130	129	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to \forall r \in M V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\})$
131	6	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to J \times_{t} J \in Top$
132	24 123	sseqtrd	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to M \subseteq ⋃ (J \times_{t} J)$
133	132	adantr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to M \subseteq ⋃ (J \times_{t} J)$
134		simpr	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to M \neq \emptyset$
135	126	neips	$⊢ (J \times_{t} J \in Top \land M \subseteq ⋃ (J \times_{t} J) \land M \neq \emptyset) \to (V \circ (M \circ V) \in nei (J \times_{t} J) (M) \leftrightarrow \forall r \in M V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\}))$
136	131 133 134 135	syl3anc	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to (V \circ (M \circ V) \in nei (J \times_{t} J) (M) \leftrightarrow \forall r \in M V \circ (M \circ V) \in nei (J \times_{t} J) (\{r\}))$
137	130 136	mpbird	$⊢ ((U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \land M \neq \emptyset) \to V \circ (M \circ V) \in nei (J \times_{t} J) (M)$
138	19 137	pm2.61dane	$⊢ (U \in UnifOn (X) \land (V \in U \land V^{-1} = V) \land M \subseteq X \times X) \to V \circ (M \circ V) \in nei (J \times_{t} J) (M)$

Metamath Proof Explorer

Theorem utop2nei

Proof