Theorem uniopn 19533

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 19531	. . . . 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 4619	. . . . . . . 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 3520	. . . . . . . . 9 |- ( x = A -> ( x C_ J <-> A C_ J ) )
7		unieq 4259	. . . . . . . . . 10 |- ( x = A -> U. x = U. A )
8	7	eleq1d 2526	. . . . . . . . 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 3194	. . . . . . 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 1393   = wceq 1395   e. wcel 1819   A.wral 2807   i^i cin 3470   C_ wss 3471   ~Pcpw 4015   U.cuni 4251   Topctop 19521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3478  df-ss 3485  df-pw 4017  df-uni 4252  df-top 19526

This theorem is referenced by:  iunopn  19534  unopn  19539  0opn  19540  topopn  19542  tgtop  19602  ntropn  19677  toponmre  19721  neips  19741  txcmplem1  20268  unimopn  21125  metrest  21153  locfinreflem  28004  cvmscld  28915  mblfinlem3  30258  mblfinlem4  30259  ismblfin  30260  cnopn  31639