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

Theorem uniopn 19275
Description: The union of a subset of a topology is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
Assertion
Ref Expression
uniopn  |-  ( ( J  e.  Top  /\  A  C_  J )  ->  U. A  e.  J
)

Proof of Theorem uniopn
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istopg 19273 . . . . 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
) )
32simpld 459 . . 3  |-  ( J  e.  Top  ->  A. x
( x  C_  J  ->  U. x  e.  J
) )
4 elpw2g 4616 . . . . . . . 8  |-  ( J  e.  Top  ->  ( A  e.  ~P J  <->  A 
C_  J ) )
54biimpar 485 . . . . . . 7  |-  ( ( J  e.  Top  /\  A  C_  J )  ->  A  e.  ~P J
)
6 sseq1 3530 . . . . . . . . 9  |-  ( x  =  A  ->  (
x  C_  J  <->  A  C_  J
) )
7 unieq 4259 . . . . . . . . . 10  |-  ( x  =  A  ->  U. x  =  U. A )
87eleq1d 2536 . . . . . . . . 9  |-  ( x  =  A  ->  ( U. x  e.  J  <->  U. A  e.  J ) )
96, 8imbi12d 320 . . . . . . . 8  |-  ( x  =  A  ->  (
( x  C_  J  ->  U. x  e.  J
)  <->  ( A  C_  J  ->  U. A  e.  J
) ) )
109spcgv 3203 . . . . . . 7  |-  ( A  e.  ~P J  -> 
( A. x ( x  C_  J  ->  U. x  e.  J )  ->  ( A  C_  J  ->  U. A  e.  J
) ) )
115, 10syl 16 . . . . . 6  |-  ( ( J  e.  Top  /\  A  C_  J )  -> 
( A. x ( x  C_  J  ->  U. x  e.  J )  ->  ( A  C_  J  ->  U. A  e.  J
) ) )
1211com23 78 . . . . 5  |-  ( ( J  e.  Top  /\  A  C_  J )  -> 
( A  C_  J  ->  ( A. x ( x  C_  J  ->  U. x  e.  J )  ->  U. A  e.  J
) ) )
1312ex 434 . . . 4  |-  ( J  e.  Top  ->  ( A  C_  J  ->  ( A  C_  J  ->  ( A. x ( x  C_  J  ->  U. x  e.  J
)  ->  U. A  e.  J ) ) ) )
1413pm2.43d 48 . . 3  |-  ( J  e.  Top  ->  ( A  C_  J  ->  ( A. x ( x  C_  J  ->  U. x  e.  J
)  ->  U. A  e.  J ) ) )
153, 14mpid 41 . 2  |-  ( J  e.  Top  ->  ( A  C_  J  ->  U. A  e.  J ) )
1615imp 429 1  |-  ( ( J  e.  Top  /\  A  C_  J )  ->  U. A  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1377    = wceq 1379    e. wcel 1767   A.wral 2817    i^i cin 3480    C_ wss 3481   ~Pcpw 4016   U.cuni 4251   Topctop 19263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-v 3120  df-in 3488  df-ss 3495  df-pw 4018  df-uni 4252  df-top 19268
This theorem is referenced by:  iunopn  19276  unopn  19281  0opn  19282  topopn  19284  tgtop  19343  ntropn  19418  toponmre  19462  neips  19482  txcmplem1  20010  unimopn  20867  metrest  20895  locfinreflem  27668  cvmscld  28543  mblfinlem3  29980  mblfinlem4  29981  ismblfin  29982  cnopn  31341  dvasinbx  31573
  Copyright terms: Public domain W3C validator