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

Theorem utop3cls 19926
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.)
Hypothesis
Ref Expression
utoptop.1
Assertion
Ref Expression
utop3cls

Proof of Theorem utop3cls
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5029 . . . . 5
2 utoptop.1 . . . . . . . . . . 11
3 utoptop 19909 . . . . . . . . . . 11
42, 3syl5eqel 2540 . . . . . . . . . 10
5 txtop 19242 . . . . . . . . . 10
64, 4, 5syl2anc 661 . . . . . . . . 9
76ad3antrrr 729 . . . . . . . 8
8 simpllr 758 . . . . . . . . 9
9 utoptopon 19911 . . . . . . . . . . . . . 14
102, 9syl5eqel 2540 . . . . . . . . . . . . 13
11 toponuni 18632 . . . . . . . . . . . . 13
1210, 11syl 16 . . . . . . . . . . . 12
1312, 12xpeq12d 4947 . . . . . . . . . . 11
14 eqid 2450 . . . . . . . . . . . . 13
1514, 14txuni 19265 . . . . . . . . . . . 12
164, 4, 15syl2anc 661 . . . . . . . . . . 11
1713, 16eqtrd 2490 . . . . . . . . . 10
1817ad3antrrr 729 . . . . . . . . 9
198, 18sseqtrd 3474 . . . . . . . 8
20 eqid 2450 . . . . . . . . 9
2120clsss3 18763 . . . . . . . 8
227, 19, 21syl2anc 661 . . . . . . 7
2322, 18sseqtr4d 3475 . . . . . 6
24 simpr 461 . . . . . 6
2523, 24sseldd 3439 . . . . 5
26 1st2nd 6704 . . . . 5
271, 25, 26sylancr 663 . . . 4
28 simp-4l 765 . . . . . . . . . 10
29 simpr1l 1045 . . . . . . . . . . 11
30293anassrs 1210 . . . . . . . . . 10
31 ustrel 19886 . . . . . . . . . 10
3228, 30, 31syl2anc 661 . . . . . . . . 9
33 simpr 461 . . . . . . . . . . . 12
34 elin 3621 . . . . . . . . . . . 12
3533, 34sylib 196 . . . . . . . . . . 11
3635simpld 459 . . . . . . . . . 10
37 xp1st 6690 . . . . . . . . . 10
3836, 37syl 16 . . . . . . . . 9
39 elrelimasn 5275 . . . . . . . . . 10
4039biimpa 484 . . . . . . . . 9
4132, 38, 40syl2anc 661 . . . . . . . 8
42 simp-4r 766 . . . . . . . . . . 11
43 xpss 5028 . . . . . . . . . . 11
4442, 43syl6ss 3450 . . . . . . . . . 10
45 df-rel 4929 . . . . . . . . . 10
4644, 45sylibr 212 . . . . . . . . 9
4735simprd 463 . . . . . . . . 9
48 1st2ndbr 6707 . . . . . . . . 9
4946, 47, 48syl2anc 661 . . . . . . . 8
50 xp2nd 6691 . . . . . . . . . . 11
5136, 50syl 16 . . . . . . . . . 10
52 elrelimasn 5275 . . . . . . . . . . 11
5352biimpa 484 . . . . . . . . . 10
5432, 51, 53syl2anc 661 . . . . . . . . 9
55 simpr1r 1046 . . . . . . . . . . 11
56553anassrs 1210 . . . . . . . . . 10
57 fvex 5783 . . . . . . . . . . . 12
58 fvex 5783 . . . . . . . . . . . 12
5957, 58brcnv 5104 . . . . . . . . . . 11
60 breq 4376 . . . . . . . . . . 11
6159, 60syl5rbbr 260 . . . . . . . . . 10
6256, 61syl 16 . . . . . . . . 9
6354, 62mpbird 232 . . . . . . . 8
64 fvex 5783 . . . . . . . . . 10
65 fvex 5783 . . . . . . . . . 10
66 brcogw 5090 . . . . . . . . . . 11
6766ex 434 . . . . . . . . . 10
6864, 57, 65, 67mp3an 1315 . . . . . . . . 9
69 brcogw 5090 . . . . . . . . . . 11
7069ex 434 . . . . . . . . . 10
7164, 58, 57, 70mp3an 1315 . . . . . . . . 9
7268, 71sylan 471 . . . . . . . 8
7341, 49, 63, 72syl21anc 1218 . . . . . . 7
7473ralrimiva 2879 . . . . . 6
75 simplll 757 . . . . . . . . 9
76 simplrl 759 . . . . . . . . 9
7743ad2ant1 1009 . . . . . . . . . . 11
78 xp1st 6690 . . . . . . . . . . . 12
792utopsnnei 19924 . . . . . . . . . . . 12
8078, 79syl3an3 1254 . . . . . . . . . . 11
81 xp2nd 6691 . . . . . . . . . . . 12
822utopsnnei 19924 . . . . . . . . . . . 12
8381, 82syl3an3 1254 . . . . . . . . . . 11
8414, 14neitx 19280 . . . . . . . . . . 11
8577, 77, 80, 83, 84syl22anc 1220 . . . . . . . . . 10
86 1st2nd2 6697 . . . . . . . . . . . . . 14
8786sneqd 3971 . . . . . . . . . . . . 13
8864, 58xpsn 5968 . . . . . . . . . . . . 13
8987, 88syl6eqr 2508 . . . . . . . . . . . 12
9089fveq2d 5777 . . . . . . . . . . 11
91903ad2ant3 1011 . . . . . . . . . 10
9285, 91eleqtrrd 2539 . . . . . . . . 9
9375, 76, 25, 92syl3anc 1219 . . . . . . . 8
9420neindisj 18821 . . . . . . . 8
957, 19, 24, 93, 94syl22anc 1220 . . . . . . 7
96 r19.3rzv 3855 . . . . . . 7
9795, 96syl 16 . . . . . 6
9874, 97mpbird 232 . . . . 5
99 df-br 4375 . . . . 5
10098, 99sylib 196 . . . 4
10127, 100eqeltrd 2536 . . 3
102101ex 434 . 2
103102ssrdv 3444 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  =/=wne 2641  A.wral 2792   cvv 3052  i^icin 3409  C_wss 3410   c0 3719  {csn 3959  <.cop 3965  U.cuni 4173   class class class wbr 4374  X.cxp 4920  `'ccnv 4921  "cima 4925  o.ccom 4926  Relwrel 4927  `cfv 5500  (class class class)co 6174   c1st 6659   c2nd 6660   ctop 18598   ctopon 18599   ccl 18722   cnei 18801   ctx 19233   cust 19874   cutop 19905
This theorem is referenced by:  utopreg  19927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-iin 4256  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-oadd 7008  df-er 7185  df-en 7395  df-fin 7398  df-fi 7746  df-topgen 14468  df-top 18603  df-bases 18605  df-topon 18606  df-cld 18723  df-ntr 18724  df-cls 18725  df-nei 18802  df-tx 19235  df-ust 19875  df-utop 19906
  Copyright terms: Public domain W3C validator