Metamath Proof Explorer

Theorem uniopn

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)

Ref Expression
Assertion uniopn 
|- ( ( J e. Top /\ A C_ J ) -> U. A e. J )

Proof

Step Hyp Ref Expression
1 istopg 
 |-  ( 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 
 |-  ( 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 
 |-  ( J e. Top -> A. x ( x C_ J -> U. x e. J ) )
4 elpw2g 
 |-  ( J e. Top -> ( A e. ~P J <-> A C_ J ) )
5 4 biimpar 
 |-  ( ( J e. Top /\ A C_ J ) -> A e. ~P J )
6 sseq1 
 |-  ( x = A -> ( x C_ J <-> A C_ J ) )
7 unieq 
 |-  ( x = A -> U. x = U. A )
8 7 eleq1d 
 |-  ( x = A -> ( U. x e. J <-> U. A e. J ) )
9 6 8 imbi12d 
 |-  ( x = A -> ( ( x C_ J -> U. x e. J ) <-> ( A C_ J -> U. A e. J ) ) )
10 9 spcgv 
 |-  ( A e. ~P J -> ( A. x ( x C_ J -> U. x e. J ) -> ( A C_ J -> U. A e. J ) ) )
11 5 10 syl 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( J e. Top -> ( A C_ J -> ( A. x ( x C_ J -> U. x e. J ) -> U. A e. J ) ) )
15 3 14 mpid 
 |-  ( J e. Top -> ( A C_ J -> U. A e. J ) )
16 15 imp 
 |-  ( ( J e. Top /\ A C_ J ) -> U. A e. J )