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.

Step	Hyp	Ref	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 ) ) )
2	1	ibi 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 ) )
3	2	simpld 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 ) )
5	4	biimpar 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 )
8	7	eleq1d 2536	. . . . . . . . 9 |- ( x = A -> ( U. x e. J <-> U. A e. J ) )
9	6, 8	imbi12d 320	. . . . . . . 8 |- ( x = A -> ( ( x C_ J -> U. x e. J ) <-> ( A C_ J -> U. A e. J ) ) )
10	9	spcgv 3203	. . . . . . 7 |- ( A e. ~P J -> ( A. x ( x C_ J -> U. x e. J ) -> ( A C_ J -> U. A e. J ) ) )
11	5, 10	syl 16	. . . . . 6 |- ( ( J e. Top /\ A C_ J ) -> ( A. x ( x C_ J -> U. x e. J ) -> ( A C_ J -> U. A e. J ) ) )
12	11	com23 78	. . . . 5 |- ( ( J e. Top /\ A C_ J ) -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) )
13	12	ex 434	. . . 4 |- ( J e. Top -> ( A C_ J -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) ) )
14	13	pm2.43d 48	. . 3 |- ( J e. Top -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) )
15	3, 14	mpid 41	. 2 |- ( J e. Top -> ( A C_ J -> U. A e. J ) )
16	15	imp 429	1 |- ( ( J e. Top /\ A C_ J ) -> U. A e. J )

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