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 e. ( UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )

Proof

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

Metamath Proof Explorer

Theorem utop2nei

Proof