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

Theorem inopn 18512
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 18508 . . . . 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 241 . . . 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 463 . . 3  |-  ( J  e.  Top  ->  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
)
4 ineq1 3545 . . . . 5  |-  ( x  =  A  ->  (
x  i^i  y )  =  ( A  i^i  y ) )
54eleq1d 2509 . . . 4  |-  ( x  =  A  ->  (
( x  i^i  y
)  e.  J  <->  ( A  i^i  y )  e.  J
) )
6 ineq2 3546 . . . . 5  |-  ( y  =  B  ->  ( A  i^i  y )  =  ( A  i^i  B
) )
76eleq1d 2509 . . . 4  |-  ( y  =  B  ->  (
( A  i^i  y
)  e.  J  <->  ( A  i^i  B )  e.  J
) )
85, 7rspc2v 3079 . . 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 30 . 2  |-  ( J  e.  Top  ->  (
( A  e.  J  /\  B  e.  J
)  ->  ( A  i^i  B )  e.  J
) )
1093impib 1185 1  |-  ( ( J  e.  Top  /\  A  e.  J  /\  B  e.  J )  ->  ( A  i^i  B
)  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965   A.wal 1367    = wceq 1369    e. wcel 1756   A.wral 2715    i^i cin 3327    C_ wss 3328   U.cuni 4091   Topctop 18498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-v 2974  df-in 3335  df-ss 3342  df-pw 3862  df-top 18503
This theorem is referenced by:  fitop  18513  tgclb  18575  topbas  18577  difopn  18638  uncld  18645  ntrin  18665  toponmre  18697  innei  18729  restopnb  18779  ordtopn3  18800  cnprest  18893  islly2  19088  kgentopon  19111  llycmpkgen2  19123  ptbasin  19150  txcnp  19193  txcnmpt  19197  qtoptop2  19272  opnfbas  19415  hauspwpwf1  19560  mopnin  20072  reconnlem2  20404  lmxrge0  26382  cvmsss2  27163  cvmcov2  27164
  Copyright terms: Public domain W3C validator