Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  utop2nei Structured version   Unicode version

Theorem utop2nei 18311
 Description: For any symmetrical entourage and any relation , build a neighborhood of . First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
Hypothesis
Ref Expression
utoptop.1 unifTop
Assertion
Ref Expression
utop2nei UnifOn

Proof of Theorem utop2nei
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 utoptop.1 . . . . . . . 8 unifTop
2 utoptop 18295 . . . . . . . 8 UnifOn unifTop
31, 2syl5eqel 2526 . . . . . . 7 UnifOn
4 txtop 17632 . . . . . . 7
53, 3, 4syl2anc 644 . . . . . 6 UnifOn
653ad2ant1 979 . . . . 5 UnifOn
76adantr 453 . . . 4 UnifOn
8 0nei 17223 . . . 4
97, 8syl 16 . . 3 UnifOn
10 coeq1 5059 . . . . . . 7
11 co01 5413 . . . . . . 7
1210, 11syl6eq 2490 . . . . . 6
1312coeq2d 5064 . . . . 5
14 co02 5412 . . . . 5
1513, 14syl6eq 2490 . . . 4
1615adantl 454 . . 3 UnifOn
17 simpr 449 . . . 4 UnifOn
1817fveq2d 5761 . . 3 UnifOn
199, 16, 183eltr4d 2523 . 2 UnifOn
206adantr 453 . . . . . 6 UnifOn
21 simpl1 961 . . . . . . . . . 10 UnifOn UnifOn
2221, 3syl 16 . . . . . . . . 9 UnifOn
23 simpl2l 1011 . . . . . . . . . 10 UnifOn
24 simp3 960 . . . . . . . . . . . 12 UnifOn
2524sselda 3334 . . . . . . . . . . 11 UnifOn
26 xp1st 6405 . . . . . . . . . . 11
2725, 26syl 16 . . . . . . . . . 10 UnifOn
281utopsnnei 18310 . . . . . . . . . 10 UnifOn
2921, 23, 27, 28syl3anc 1185 . . . . . . . . 9 UnifOn
30 xp2nd 6406 . . . . . . . . . . 11
3125, 30syl 16 . . . . . . . . . 10 UnifOn
321utopsnnei 18310 . . . . . . . . . 10 UnifOn
3321, 23, 31, 32syl3anc 1185 . . . . . . . . 9 UnifOn
34 eqid 2442 . . . . . . . . . 10
3534, 34neitx 17670 . . . . . . . . 9
3622, 22, 29, 33, 35syl22anc 1186 . . . . . . . 8 UnifOn
37 fvex 5771 . . . . . . . . . 10
38 fvex 5771 . . . . . . . . . 10
3937, 38xpsn 5939 . . . . . . . . 9
4039fveq2i 5760 . . . . . . . 8
4136, 40syl6eleq 2532 . . . . . . 7 UnifOn
4224adantr 453 . . . . . . . . . . 11 UnifOn
43 xpss 5011 . . . . . . . . . . . . 13
44 sstr 3342 . . . . . . . . . . . . 13
4543, 44mpan2 654 . . . . . . . . . . . 12
46 df-rel 4914 . . . . . . . . . . . 12
4745, 46sylibr 205 . . . . . . . . . . 11
4842, 47syl 16 . . . . . . . . . 10 UnifOn
49 1st2nd 6422 . . . . . . . . . 10
5048, 49sylancom 650 . . . . . . . . 9 UnifOn
5150sneqd 3851 . . . . . . . 8 UnifOn
5251fveq2d 5761 . . . . . . 7 UnifOn
5341, 52eleqtrrd 2519 . . . . . 6 UnifOn
54 relxp 5012 . . . . . . . . . . 11
5554a1i 11 . . . . . . . . . 10 UnifOn
56 1st2nd 6422 . . . . . . . . . 10
5755, 56sylancom 650 . . . . . . . . 9 UnifOn
58 simpll2 998 . . . . . . . . . . . . 13 UnifOn
5958simprd 451 . . . . . . . . . . . 12 UnifOn
60 simpll1 997 . . . . . . . . . . . . . 14 UnifOn UnifOn
6158simpld 447 . . . . . . . . . . . . . 14 UnifOn
62 ustrel 18272 . . . . . . . . . . . . . 14 UnifOn
6360, 61, 62syl2anc 644 . . . . . . . . . . . . 13 UnifOn
64 xp1st 6405 . . . . . . . . . . . . . 14
6564adantl 454 . . . . . . . . . . . . 13 UnifOn
66 elrelimasn 5257 . . . . . . . . . . . . . 14
6766biimpa 472 . . . . . . . . . . . . 13
6863, 65, 67syl2anc 644 . . . . . . . . . . . 12 UnifOn
69 fvex 5771 . . . . . . . . . . . . . . 15
7037, 69brcnv 5084 . . . . . . . . . . . . . 14
71 breq 4239 . . . . . . . . . . . . . 14
7270, 71syl5bbr 252 . . . . . . . . . . . . 13
7372biimpar 473 . . . . . . . . . . . 12
7459, 68, 73syl2anc 644 . . . . . . . . . . 11 UnifOn
75 simpll3 999 . . . . . . . . . . . 12 UnifOn
76 simplr 733 . . . . . . . . . . . 12 UnifOn
77 1st2ndbr 6425 . . . . . . . . . . . . 13
7847, 77sylan 459 . . . . . . . . . . . 12
7975, 76, 78syl2anc 644 . . . . . . . . . . 11 UnifOn
80 xp2nd 6406 . . . . . . . . . . . . 13
8180adantl 454 . . . . . . . . . . . 12 UnifOn
82 elrelimasn 5257 . . . . . . . . . . . . 13
8382biimpa 472 . . . . . . . . . . . 12
8463, 81, 83syl2anc 644 . . . . . . . . . . 11 UnifOn
8569, 38, 373pm3.2i 1133 . . . . . . . . . . . . 13
86 brcogw 5070 . . . . . . . . . . . . 13
8785, 86mpan 653 . . . . . . . . . . . 12
88 fvex 5771 . . . . . . . . . . . . . 14
8969, 88, 383pm3.2i 1133 . . . . . . . . . . . . 13
90 brcogw 5070 . . . . . . . . . . . . 13
9189, 90mpan 653 . . . . . . . . . . . 12
9287, 91sylan 459 . . . . . . . . . . 11
9374, 79, 84, 92syl21anc 1184 . . . . . . . . . 10 UnifOn
94 df-br 4238 . . . . . . . . . 10
9593, 94sylib 190 . . . . . . . . 9 UnifOn
9657, 95eqeltrd 2516 . . . . . . . 8 UnifOn
9796ex 425 . . . . . . 7 UnifOn
9897ssrdv 3340 . . . . . 6 UnifOn
99 simp1 958 . . . . . . . . . . 11 UnifOn UnifOn
100 simp2l 984 . . . . . . . . . . 11 UnifOn
101 ustssxp 18265 . . . . . . . . . . 11 UnifOn
10299, 100, 101syl2anc 644 . . . . . . . . . 10 UnifOn
103 coss1 5057 . . . . . . . . . 10
104102, 103syl 16 . . . . . . . . 9 UnifOn
105 coss1 5057 . . . . . . . . . . . 12
10624, 105syl 16 . . . . . . . . . . 11 UnifOn
107 coss2 5058 . . . . . . . . . . . . 13
108 xpcoid 5444 . . . . . . . . . . . . 13
109107, 108syl6sseq 3380 . . . . . . . . . . . 12
110102, 109syl 16 . . . . . . . . . . 11 UnifOn
111106, 110sstrd 3344 . . . . . . . . . 10 UnifOn
112 coss2 5058 . . . . . . . . . . 11
113112, 108syl6sseq 3380 . . . . . . . . . 10
114111, 113syl 16 . . . . . . . . 9 UnifOn
115104, 114sstrd 3344 . . . . . . . 8 UnifOn
116 utopbas 18296 . . . . . . . . . . . 12 UnifOn unifTop
1171unieqi 4049 . . . . . . . . . . . 12 unifTop
118116, 117syl6eqr 2492 . . . . . . . . . . 11 UnifOn
119118, 118xpeq12d 4932 . . . . . . . . . 10 UnifOn
12034, 34txuni 17655 . . . . . . . . . . 11
1213, 3, 120syl2anc 644 . . . . . . . . . 10 UnifOn
122119, 121eqtrd 2474 . . . . . . . . 9 UnifOn
1231223ad2ant1 979 . . . . . . . 8 UnifOn
124115, 123sseqtrd 3370 . . . . . . 7 UnifOn
125124adantr 453 . . . . . 6 UnifOn
126 eqid 2442 . . . . . . 7
127126ssnei2 17211 . . . . . 6
12820, 53, 98, 125, 127syl22anc 1186 . . . . 5 UnifOn
129128ralrimiva 2795 . . . 4 UnifOn
130129adantr 453 . . 3 UnifOn
1316adantr 453 . . . 4 UnifOn
13224, 123sseqtrd 3370 . . . . 5 UnifOn
133132adantr 453 . . . 4 UnifOn
134 simpr 449 . . . 4 UnifOn
135126neips 17208 . . . 4
136131, 133, 134, 135syl3anc 1185 . . 3 UnifOn
137130, 136mpbird 225 . 2 UnifOn
13819, 137pm2.61dane 2688 1 UnifOn
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1727   wne 2605  wral 2711  cvv 2962   wss 3306  c0 3613  csn 3838  cop 3841  cuni 4039   class class class wbr 4237   cxp 4905  ccnv 4906  cima 4910   ccom 4911   wrel 4912  cfv 5483  (class class class)co 6110  c1st 6376  c2nd 6377  ctop 16989  cnei 17192   ctx 17623  UnifOncust 18260  unifTopcutop 18291 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-rep 4345  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-int 4075  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-1st 6378  df-2nd 6379  df-recs 6662  df-rdg 6697  df-1o 6753  df-oadd 6757  df-er 6934  df-en 7139  df-fin 7142  df-fi 7445  df-topgen 13698  df-top 16994  df-bases 16996  df-topon 16997  df-nei 17193  df-tx 17625  df-ust 18261  df-utop 18292
 Copyright terms: Public domain W3C validator