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

Theorem utoptop 21249
 Description: The topology induced by a uniform structure is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.)
Assertion
Ref Expression
utoptop UnifOn unifTop

Proof of Theorem utoptop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 463 . . . . . . 7 UnifOn unifTop unifTop
2 utopval 21247 . . . . . . . . 9 UnifOn unifTop
3 ssrab2 3514 . . . . . . . . 9
42, 3syl6eqss 3482 . . . . . . . 8 UnifOn unifTop
54adantr 467 . . . . . . 7 UnifOn unifTop unifTop
61, 5sstrd 3442 . . . . . 6 UnifOn unifTop
7 sspwuni 4367 . . . . . 6
86, 7sylib 200 . . . . 5 UnifOn unifTop
9 simp-4l 776 . . . . . . . . 9 UnifOn unifTop UnifOn
10 simp-4r 777 . . . . . . . . . 10 UnifOn unifTop unifTop
11 simplr 762 . . . . . . . . . 10 UnifOn unifTop
1210, 11sseldd 3433 . . . . . . . . 9 UnifOn unifTop unifTop
13 simpr 463 . . . . . . . . 9 UnifOn unifTop
14 elutop 21248 . . . . . . . . . . . 12 UnifOn unifTop
1514biimpa 487 . . . . . . . . . . 11 UnifOn unifTop
1615simprd 465 . . . . . . . . . 10 UnifOn unifTop
1716r19.21bi 2757 . . . . . . . . 9 UnifOn unifTop
189, 12, 13, 17syl21anc 1267 . . . . . . . 8 UnifOn unifTop
19 r19.41v 2942 . . . . . . . . 9
20 ssuni 4220 . . . . . . . . . 10
2120reximi 2855 . . . . . . . . 9
2219, 21sylbir 217 . . . . . . . 8
2318, 11, 22syl2anc 667 . . . . . . 7 UnifOn unifTop
24 eluni2 4202 . . . . . . . . 9
2524biimpi 198 . . . . . . . 8
2625adantl 468 . . . . . . 7 UnifOn unifTop
2723, 26r19.29a 2932 . . . . . 6 UnifOn unifTop
2827ralrimiva 2802 . . . . 5 UnifOn unifTop
29 elutop 21248 . . . . . 6 UnifOn unifTop
3029adantr 467 . . . . 5 UnifOn unifTop unifTop
318, 28, 30mpbir2and 933 . . . 4 UnifOn unifTop unifTop
3231ex 436 . . 3 UnifOn unifTop unifTop
3332alrimiv 1773 . 2 UnifOn unifTop unifTop
34 elutop 21248 . . . . . . . 8 UnifOn unifTop
3534biimpa 487 . . . . . . 7 UnifOn unifTop
3635simpld 461 . . . . . 6 UnifOn unifTop
3736adantrr 723 . . . . 5 UnifOn unifTop unifTop
38 ssinss1 3660 . . . . 5
3937, 38syl 17 . . . 4 UnifOn unifTop unifTop
40 simpl 459 . . . . . . . . . 10 UnifOn unifTop unifTop UnifOn
41 simpr31 1098 . . . . . . . . . 10 UnifOn unifTop unifTop
42 simpr32 1099 . . . . . . . . . 10 UnifOn unifTop unifTop
43 ustincl 21222 . . . . . . . . . 10 UnifOn
4440, 41, 42, 43syl3anc 1268 . . . . . . . . 9 UnifOn unifTop unifTop
45 inss1 3652 . . . . . . . . . . . 12
46 imass1 5203 . . . . . . . . . . . 12
4745, 46ax-mp 5 . . . . . . . . . . 11
48 simpr33 1100 . . . . . . . . . . . 12 UnifOn unifTop unifTop
4948simpld 461 . . . . . . . . . . 11 UnifOn unifTop unifTop
5047, 49syl5ss 3443 . . . . . . . . . 10 UnifOn unifTop unifTop
51 inss2 3653 . . . . . . . . . . . 12
52 imass1 5203 . . . . . . . . . . . 12
5351, 52ax-mp 5 . . . . . . . . . . 11
5448simprd 465 . . . . . . . . . . 11 UnifOn unifTop unifTop
5553, 54syl5ss 3443 . . . . . . . . . 10 UnifOn unifTop unifTop
5650, 55ssind 3656 . . . . . . . . 9 UnifOn unifTop unifTop
57 imaeq1 5163 . . . . . . . . . . 11
5857sseq1d 3459 . . . . . . . . . 10
5958rspcev 3150 . . . . . . . . 9
6044, 56, 59syl2anc 667 . . . . . . . 8 UnifOn unifTop unifTop
61603anassrs 1232 . . . . . . 7 UnifOn unifTop unifTop
62613anassrs 1232 . . . . . 6 UnifOn unifTop unifTop
63 simpll 760 . . . . . . . 8 UnifOn unifTop unifTop UnifOn
64 simplrl 770 . . . . . . . 8 UnifOn unifTop unifTop unifTop
65 simpr 463 . . . . . . . . . 10 UnifOn unifTop unifTop
66 elin 3617 . . . . . . . . . 10
6765, 66sylib 200 . . . . . . . . 9 UnifOn unifTop unifTop
6867simpld 461 . . . . . . . 8 UnifOn unifTop unifTop
6935simprd 465 . . . . . . . . 9 UnifOn unifTop
7069r19.21bi 2757 . . . . . . . 8 UnifOn unifTop
7163, 64, 68, 70syl21anc 1267 . . . . . . 7 UnifOn unifTop unifTop
72 simplrr 771 . . . . . . . 8 UnifOn unifTop unifTop unifTop
7367simprd 465 . . . . . . . 8 UnifOn unifTop unifTop
7463, 72, 73, 17syl21anc 1267 . . . . . . 7 UnifOn unifTop unifTop
75 reeanv 2958 . . . . . . 7
7671, 74, 75sylanbrc 670 . . . . . 6 UnifOn unifTop unifTop
7762, 76r19.29vva 2934 . . . . 5 UnifOn unifTop unifTop
7877ralrimiva 2802 . . . 4 UnifOn unifTop unifTop
79 elutop 21248 . . . . 5 UnifOn unifTop
8079adantr 467 . . . 4 UnifOn unifTop unifTop unifTop
8139, 78, 80mpbir2and 933 . . 3 UnifOn unifTop unifTop unifTop
8281ralrimivva 2809 . 2 UnifOn unifTop unifTop unifTop
83 fvex 5875 . . 3 unifTop
84 istopg 19925 . . 3 unifTop unifTop unifTop unifTop unifTop unifTop unifTop
8583, 84ax-mp 5 . 2 unifTop unifTop unifTop unifTop unifTop unifTop
8633, 82, 85sylanbrc 670 1 UnifOn unifTop
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 985  wal 1442   wceq 1444   wcel 1887  wral 2737  wrex 2738  crab 2741  cvv 3045   cin 3403   wss 3404  cpw 3951  csn 3968  cuni 4198  cima 4837  cfv 5582  ctop 19917  UnifOncust 21214  unifTopcutop 21245 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-fv 5590  df-top 19921  df-ust 21215  df-utop 21246 This theorem is referenced by:  utoptopon  21251  utop2nei  21265  utop3cls  21266  utopreg  21267
 Copyright terms: Public domain W3C validator