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

Theorem istopg 16973
 Description: Express the predicate " is a topology." Note: In the literature, a topology is often represented by a script letter T, which resembles the letter J. This confusion may have led to J being used by some authors - e.g. K. D. Joshi, Introduction to General Topology (1983), p. 114 - and it is convenient for us since we later use to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
Assertion
Ref Expression
istopg
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem istopg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pweq 3804 . . . . 5
2 eleq2 2499 . . . . 5
31, 2raleqbidv 2918 . . . 4
4 eleq2 2499 . . . . . 6
54raleqbi1dv 2914 . . . . 5
65raleqbi1dv 2914 . . . 4
73, 6anbi12d 693 . . 3
8 df-top 16968 . . 3
97, 8elab2g 3086 . 2
10 df-ral 2712 . . . 4
11 elpw2g 4366 . . . . . 6
1211imbi1d 310 . . . . 5
1312albidv 1636 . . . 4
1410, 13syl5bb 250 . . 3
1514anbi1d 687 . 2
169, 15bitrd 246 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wal 1550   wceq 1653   wcel 1726  wral 2707   cin 3321   wss 3322  cpw 3801  cuni 4017  ctop 16963 This theorem is referenced by:  istop2g  16974  uniopn  16975  inopn  16977  istps3OLD  16992  tgcl  17039  distop  17065  indistopon  17070  fctop  17073  cctop  17075  ppttop  17076  epttop  17078  mretopd  17161  toponmre  17162  neiptoptop  17200  kgentopon  17575  qtoptop2  17736  filcon  17920  utoptop  18269  neibastop1  26402 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 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803  df-top 16968
 Copyright terms: Public domain W3C validator