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

Theorem inopn 20006
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 20002 . . . . 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 249 . . . 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 470 . . 3  |-  ( J  e.  Top  ->  A. x  e.  J  A. y  e.  J  ( x  i^i  y )  e.  J
)
4 ineq1 3618 . . . . 5  |-  ( x  =  A  ->  (
x  i^i  y )  =  ( A  i^i  y ) )
54eleq1d 2533 . . . 4  |-  ( x  =  A  ->  (
( x  i^i  y
)  e.  J  <->  ( A  i^i  y )  e.  J
) )
6 ineq2 3619 . . . . 5  |-  ( y  =  B  ->  ( A  i^i  y )  =  ( A  i^i  B
) )
76eleq1d 2533 . . . 4  |-  ( y  =  B  ->  (
( A  i^i  y
)  e.  J  <->  ( A  i^i  B )  e.  J
) )
85, 7rspc2v 3147 . . 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 1229 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 376    /\ w3a 1007   A.wal 1450    = wceq 1452    e. wcel 1904   A.wral 2756    i^i cin 3389    C_ wss 3390   U.cuni 4190   Topctop 19994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518
This theorem depends on definitions:  df-bi 190  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-v 3033  df-in 3397  df-ss 3404  df-pw 3944  df-top 19998
This theorem is referenced by:  fitop  20007  tgclb  20063  topbas  20065  difopn  20126  uncld  20133  ntrin  20153  toponmre  20186  innei  20218  restopnb  20268  ordtopn3  20289  cnprest  20382  islly2  20576  kgentopon  20630  llycmpkgen2  20642  ptbasin  20669  txcnp  20712  txcnmpt  20716  qtoptop2  20791  opnfbas  20935  hauspwpwf1  21080  mopnin  21590  reconnlem2  21923  lmxrge0  28832  cvmsss2  30069  cvmcov2  30070  icccncfext  37862
  Copyright terms: Public domain W3C validator