Theorem uniopn 8867

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

Step	Hyp	Ref	Expression
1		istopg 8865	. . . . 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 652	. . . 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	simplld 348	. . 3 |- (J e. Top -> A.x(x C_ J -> U.x e. J))
4		elpw2g 3463	. . . . . . . 8 |- (J e. Top -> (A e. ~PJ <-> A C_ J))
5	4	biimpar 461	. . . . . . 7 |- ((J e. Top /\ A C_ J) -> A e. ~PJ)
6		sseq1 2637	. . . . . . . . 9 |- (x = A -> (x C_ J <-> A C_ J))
7		unieq 3185	. . . . . . . . . 10 |- (x = A -> U.x = U.A)
8	7	eleq1d 1963	. . . . . . . . 9 |- (x = A -> (U.x e. J <-> U.A e. J))
9	6, 8	imbi12d 688	. . . . . . . 8 |- (x = A -> ((x C_ J -> U.x e. J) <-> (A C_ J -> U.A e. J)))
10	9	cla4gv 2364	. . . . . . 7 |- (A e. ~PJ -> (A.x(x C_ J -> U.x e. J) -> (A C_ J -> U.A e. J)))
11	5, 10	syl 12	. . . . . 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 36	. . . . 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 402	. . . 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 79	. . 3 |- (J e. Top -> (A C_ J -> (A.x(x C_ J -> U.x e. J) -> U.A e. J)))
15	3, 14	mpid 58	. 2 |- (J e. Top -> (A C_ J -> U.A e. J))
16	15	imp 377	1 |- ((J e. Top /\ A C_ J) -> U.A e. J)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105   i^i cin 2592   C_ wss 2593  ~Pcpw 3032  U.cuni 3177  Topctop 8857

This theorem is referenced by:  iunopn 8868  0opn 8870  topopn 8871  tgval3 8895  tgtop 8898  basgen2 8909  subtop 8916  ntropn 8960  neiint 8995  neips 9003  cncnplem4 9054  clicls 10183  clint3 10184  subtopmet 10256  toplat 14638  inttop2 14863  qusp 14908  comppfsc 15517  topmtcl 15525  unopn 15835  txsubsp 15912

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-pw 3035  df-uni 3178  df-top 8861

Copyright terms: Public domain