Theorem uniopn 19939

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 19937	. . . . 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 245	. . . 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 461	. . 3 |- ( J e. Top -> A. x ( x C_ J -> U. x e. J ) )
4		elpw2g 4569	. . . . . . . 8 |- ( J e. Top -> ( A e. ~P J <-> A C_ J ) )
5	4	biimpar 488	. . . . . . 7 |- ( ( J e. Top /\ A C_ J ) -> A e. ~P J )
6		sseq1 3455	. . . . . . . . 9 |- ( x = A -> ( x C_ J <-> A C_ J ) )
7		unieq 4209	. . . . . . . . . 10 |- ( x = A -> U. x = U. A )
8	7	eleq1d 2515	. . . . . . . . 9 |- ( x = A -> ( U. x e. J <-> U. A e. J ) )
9	6, 8	imbi12d 322	. . . . . . . 8 |- ( x = A -> ( ( x C_ J -> U. x e. J ) <-> ( A C_ J -> U. A e. J ) ) )
10	9	spcgv 3136	. . . . . . 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 81	. . . . 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 436	. . . 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 50	. . 3 |- ( J e. Top -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) )
15	3, 14	mpid 42	. 2 |- ( J e. Top -> ( A C_ J -> U. A e. J ) )
16	15	imp 431	1 |- ( ( J e. Top /\ A C_ J ) -> U. A e. J )

Syntax hints:   -> wi 4   /\ wa 371   A.wal 1444   = wceq 1446   e. wcel 1889   A.wral 2739   i^i cin 3405   C_ wss 3406   ~Pcpw 3953   U.cuni 4201   Topctop 19929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rex 2745  df-v 3049  df-in 3413  df-ss 3420  df-pw 3955  df-uni 4202  df-top 19933

This theorem is referenced by:  iunopn  19940  unopn  19945  0opn  19946  topopn  19948  tgtop  20001  ntropn  20076  toponmre  20121  neips  20141  txcmplem1  20668  unimopn  21523  metrest  21551  locfinreflem  28679  cvmscld  30008  mblfinlem3  31991  mblfinlem4  31992  ismblfin  31993  cnopn  37385