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

Theorem isusp 21354
 Description: The predicate is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.)
Hypotheses
Ref Expression
isusp.1
isusp.2 UnifSt
isusp.3
Assertion
Ref Expression
isusp UnifSp UnifOn unifTop

Proof of Theorem isusp
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3040 . 2 UnifSp
2 0nep0 4572 . . . . 5
3 isusp.1 . . . . . . . . . . . 12
4 fvprc 5873 . . . . . . . . . . . 12
53, 4syl5eq 2517 . . . . . . . . . . 11
65fveq2d 5883 . . . . . . . . . 10 UnifOn UnifOn
7 ust0 21312 . . . . . . . . . 10 UnifOn
86, 7syl6eq 2521 . . . . . . . . 9 UnifOn
98eleq2d 2534 . . . . . . . 8 UnifOn
10 isusp.2 . . . . . . . . . 10 UnifSt
11 fvex 5889 . . . . . . . . . 10 UnifSt
1210, 11eqeltri 2545 . . . . . . . . 9
1312elsnc 3984 . . . . . . . 8
149, 13syl6bb 269 . . . . . . 7 UnifOn
15 fvprc 5873 . . . . . . . . 9 UnifSt
1610, 15syl5eq 2517 . . . . . . . 8
1716eqeq1d 2473 . . . . . . 7
1814, 17bitrd 261 . . . . . 6 UnifOn
1918necon3bbid 2680 . . . . 5 UnifOn
202, 19mpbiri 241 . . . 4 UnifOn
2120con4i 135 . . 3 UnifOn
2221adantr 472 . 2 UnifOn unifTop
23 fveq2 5879 . . . . . 6 UnifSt UnifSt
2423, 10syl6eqr 2523 . . . . 5 UnifSt
25 fveq2 5879 . . . . . . 7
2625, 3syl6eqr 2523 . . . . . 6
2726fveq2d 5883 . . . . 5 UnifOn UnifOn
2824, 27eleq12d 2543 . . . 4 UnifSt UnifOn UnifOn
29 fveq2 5879 . . . . . 6
30 isusp.3 . . . . . 6
3129, 30syl6eqr 2523 . . . . 5
3224fveq2d 5883 . . . . 5 unifTopUnifSt unifTop
3331, 32eqeq12d 2486 . . . 4 unifTopUnifSt unifTop
3428, 33anbi12d 725 . . 3 UnifSt UnifOn unifTopUnifSt UnifOn unifTop
35 df-usp 21350 . . 3 UnifSp UnifSt UnifOn unifTopUnifSt
3634, 35elab2g 3175 . 2 UnifSp UnifOn unifTop
371, 22, 36pm5.21nii 360 1 UnifSp UnifOn unifTop
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 189   wa 376   wceq 1452   wcel 1904   wne 2641  cvv 3031  c0 3722  csn 3959  cfv 5589  cbs 15199  ctopn 15398  UnifOncust 21292  unifTopcutop 21323  UnifStcuss 21346  UnifSpcusp 21347 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-res 4851  df-iota 5553  df-fun 5591  df-fv 5597  df-ust 21293  df-usp 21350 This theorem is referenced by:  ressust  21357  ressusp  21358  tususp  21365  uspreg  21367  ucncn  21378  neipcfilu  21389  ucnextcn  21397  xmsusp  21662
 Copyright terms: Public domain W3C validator