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

Theorem istopg 19862
Description: Express the predicate " J 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  T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
Assertion
Ref Expression
istopg  |-  ( J  e.  A  ->  ( J  e.  Top  <->  ( A. x ( x  C_  J  ->  U. x  e.  J
)  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
) ) )
Distinct variable groups:    x, y, J    x, A
Allowed substitution hint:    A( y)

Proof of Theorem istopg
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 pweq 3922 . . . . 5  |-  ( z  =  J  ->  ~P z  =  ~P J
)
2 eleq2 2490 . . . . 5  |-  ( z  =  J  ->  ( U. x  e.  z  <->  U. x  e.  J ) )
31, 2raleqbidv 2973 . . . 4  |-  ( z  =  J  ->  ( A. x  e.  ~P  z U. x  e.  z  <->  A. x  e.  ~P  J U. x  e.  J
) )
4 eleq2 2490 . . . . . 6  |-  ( z  =  J  ->  (
( x  i^i  y
)  e.  z  <->  ( x  i^i  y )  e.  J
) )
54raleqbi1dv 2967 . . . . 5  |-  ( z  =  J  ->  ( A. y  e.  z 
( x  i^i  y
)  e.  z  <->  A. y  e.  J  ( x  i^i  y )  e.  J
) )
65raleqbi1dv 2967 . . . 4  |-  ( z  =  J  ->  ( A. x  e.  z  A. y  e.  z 
( x  i^i  y
)  e.  z  <->  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
) )
73, 6anbi12d 715 . . 3  |-  ( z  =  J  ->  (
( A. x  e. 
~P  z U. x  e.  z  /\  A. x  e.  z  A. y  e.  z  ( x  i^i  y )  e.  z )  <->  ( A. x  e.  ~P  J U. x  e.  J  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
) ) )
8 df-top 19858 . . 3  |-  Top  =  { z  |  ( A. x  e.  ~P  z U. x  e.  z  /\  A. x  e.  z  A. y  e.  z  ( x  i^i  y )  e.  z ) }
97, 8elab2g 3157 . 2  |-  ( J  e.  A  ->  ( J  e.  Top  <->  ( A. x  e.  ~P  J U. x  e.  J  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y
)  e.  J ) ) )
10 df-ral 2714 . . . 4  |-  ( A. x  e.  ~P  J U. x  e.  J  <->  A. x ( x  e. 
~P J  ->  U. x  e.  J ) )
11 elpw2g 4525 . . . . . 6  |-  ( J  e.  A  ->  (
x  e.  ~P J  <->  x 
C_  J ) )
1211imbi1d 318 . . . . 5  |-  ( J  e.  A  ->  (
( x  e.  ~P J  ->  U. x  e.  J
)  <->  ( x  C_  J  ->  U. x  e.  J
) ) )
1312albidv 1761 . . . 4  |-  ( J  e.  A  ->  ( A. x ( x  e. 
~P J  ->  U. x  e.  J )  <->  A. x
( x  C_  J  ->  U. x  e.  J
) ) )
1410, 13syl5bb 260 . . 3  |-  ( J  e.  A  ->  ( A. x  e.  ~P  J U. x  e.  J  <->  A. x ( x  C_  J  ->  U. x  e.  J
) ) )
1514anbi1d 709 . 2  |-  ( J  e.  A  ->  (
( A. x  e. 
~P  J U. x  e.  J  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
)  <->  ( A. x
( x  C_  J  ->  U. x  e.  J
)  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
) ) )
169, 15bitrd 256 1  |-  ( J  e.  A  ->  ( J  e.  Top  <->  ( A. x ( x  C_  J  ->  U. x  e.  J
)  /\  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1872   A.wral 2709    i^i cin 3373    C_ wss 3374   ~Pcpw 3919   U.cuni 4157   Topctop 19854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714  df-v 3019  df-in 3381  df-ss 3388  df-pw 3921  df-top 19858
This theorem is referenced by:  istop2g  19863  uniopn  19864  inopn  19866  tgcl  19922  distop  19948  indistopon  19953  fctop  19956  cctop  19958  ppttop  19959  epttop  19961  mretopd  20045  toponmre  20046  neiptoptop  20084  kgentopon  20490  qtoptop2  20651  filcon  20835  utoptop  21186  neibastop1  30959
  Copyright terms: Public domain W3C validator