Theorem uniopn 20702

Description: The union of a subset of a topology (that is, the union of any family of open sets 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 20700	. . . . 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 256	. . . 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 475	. . 3 |- ( J e. Top -> A. x ( x C_ J -> U. x e. J ) )
4		elpw2g 4827	. . . . . . . 8 |- ( J e. Top -> ( A e. ~P J <-> A C_ J ) )
5	4	biimpar 502	. . . . . . 7 |- ( ( J e. Top /\ A C_ J ) -> A e. ~P J )
6		sseq1 3626	. . . . . . . . 9 |- ( x = A -> ( x C_ J <-> A C_ J ) )
7		unieq 4444	. . . . . . . . . 10 |- ( x = A -> U. x = U. A )
8	7	eleq1d 2686	. . . . . . . . 9 |- ( x = A -> ( U. x e. J <-> U. A e. J ) )
9	6, 8	imbi12d 334	. . . . . . . 8 |- ( x = A -> ( ( x C_ J -> U. x e. J ) <-> ( A C_ J -> U. A e. J ) ) )
10	9	spcgv 3293	. . . . . . 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 17	. . . . . 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 86	. . . . 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 450	. . . 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 53	. . 3 |- ( J e. Top -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) )
15	3, 14	mpid 44	. 2 |- ( J e. Top -> ( A C_ J -> U. A e. J ) )
16	15	imp 445	1 |- ( ( J e. Top /\ A C_ J ) -> U. A e. J )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   A.wral 2912   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   U.cuni 4436   Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437  df-top 20699

This theorem is referenced by:  iunopn  20703  unopn  20708  0opn  20709  topopn  20711  tgtop  20777  ntropn  20853  toponmre  20897  neips  20917  txcmplem1  21444  unimopn  22301  metrest  22329  cnopn  22590  locfinreflem  29907  cvmscld  31255  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450