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

Theorem inopn 16645
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 16641 . . . . 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 3363 . . . . 5  |-  ( x  =  A  ->  (
x  i^i  y )  =  ( A  i^i  y ) )
54eleq1d 2349 . . . 4  |-  ( x  =  A  ->  (
( x  i^i  y
)  e.  J  <->  ( A  i^i  y )  e.  J
) )
6 ineq2 3364 . . . . 5  |-  ( y  =  B  ->  ( A  i^i  y )  =  ( A  i^i  B
) )
76eleq1d 2349 . . . 4  |-  ( y  =  B  ->  (
( A  i^i  y
)  e.  J  <->  ( A  i^i  B )  e.  J
) )
85, 7rspc2v 2890 . . 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 1527    = wceq 1623    e. wcel 1684   A.wral 2543    i^i cin 3151    C_ wss 3152   U.cuni 3827   Topctop 16631
This theorem is referenced by:  fitop  16646  tgclb  16708  topbas  16710  difopn  16771  uncld  16778  ntrin  16798  toponmre  16830  innei  16862  restopnb  16906  ordtopn3  16926  cnprest  17017  islly2  17210  kgentopon  17233  llycmpkgen2  17245  ptbasin  17272  txcnp  17314  txcnmpt  17318  qtoptop2  17390  opnfbas  17537  hauspwpwf1  17682  mopnin  18043  reconnlem2  18332  lmxrge0  23375  cvmsss2  23805  cvmcov2  23806  toplat  25290  inttop2  25515  qusp  25542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-top 16636
  Copyright terms: Public domain W3C validator