Metamath Proof Explorer


Theorem 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 UnifOn X V U V -1 = V M X × X V M V nei J × t J M

Proof

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