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

Theorem inopn 16661
Description: The intersection of two open sets of a topology is also an open set. (Contributed by NM, 17-Jul-2006.)
Assertion
Ref Expression
inopn  |-  ( ( J  e.  Top  /\  A  e.  J  /\  B  e.  J )  ->  ( A  i^i  B
)  e.  J )

Proof of Theorem inopn
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istopg 16657 . . . . 5  |-  ( J  e.  Top  ->  ( 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
) ) )
21ibi 232 . . . 4  |-  ( 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
) )
32simprd 449 . . 3  |-  ( J  e.  Top  ->  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
)
4 ineq1 3376 . . . . 5  |-  ( x  =  A  ->  (
x  i^i  y )  =  ( A  i^i  y ) )
54eleq1d 2362 . . . 4  |-  ( x  =  A  ->  (
( x  i^i  y
)  e.  J  <->  ( A  i^i  y )  e.  J
) )
6 ineq2 3377 . . . . 5  |-  ( y  =  B  ->  ( A  i^i  y )  =  ( A  i^i  B
) )
76eleq1d 2362 . . . 4  |-  ( y  =  B  ->  (
( A  i^i  y
)  e.  J  <->  ( A  i^i  B )  e.  J
) )
85, 7rspc2v 2903 . . 3  |-  ( ( A  e.  J  /\  B  e.  J )  ->  ( A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J  ->  ( A  i^i  B
)  e.  J ) )
93, 8syl5com 26 . 2  |-  ( J  e.  Top  ->  (
( A  e.  J  /\  B  e.  J
)  ->  ( A  i^i  B )  e.  J
) )
1093impib 1149 1  |-  ( ( J  e.  Top  /\  A  e.  J  /\  B  e.  J )  ->  ( A  i^i  B
)  e.  J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934   A.wal 1530    = wceq 1632    e. wcel 1696   A.wral 2556    i^i cin 3164    C_ wss 3165   U.cuni 3843   Topctop 16647
This theorem is referenced by:  fitop  16662  tgclb  16724  topbas  16726  difopn  16787  uncld  16794  ntrin  16814  toponmre  16846  innei  16878  restopnb  16922  ordtopn3  16942  cnprest  17033  islly2  17226  kgentopon  17249  llycmpkgen2  17261  ptbasin  17288  txcnp  17330  txcnmpt  17334  qtoptop2  17406  opnfbas  17553  hauspwpwf1  17698  mopnin  18059  reconnlem2  18348  lmxrge0  23390  cvmsss2  23820  cvmcov2  23821  toplat  25393  inttop2  25618  qusp  25645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640  df-top 16652
  Copyright terms: Public domain W3C validator