Metamath Proof Explorer

Theorem uncld

Description: The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of Munkres p. 93. (Contributed by NM, 5-Oct-2006)

Ref Expression
Assertion uncld 
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A u. B ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 difundi 
 |-  ( U. J \ ( A u. B ) ) = ( ( U. J \ A ) i^i ( U. J \ B ) )
2 cldrcl 
 |-  ( A e. ( Clsd ` J ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 3 cldopn 
 |-  ( A e. ( Clsd ` J ) -> ( U. J \ A ) e. J )
5 3 cldopn 
 |-  ( B e. ( Clsd ` J ) -> ( U. J \ B ) e. J )
6 inopn 
 |-  ( ( J e. Top /\ ( U. J \ A ) e. J /\ ( U. J \ B ) e. J ) -> ( ( U. J \ A ) i^i ( U. J \ B ) ) e. J )
7 2 4 5 6 syl2an3an 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( ( U. J \ A ) i^i ( U. J \ B ) ) e. J )
8 1 7 eqeltrid 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( U. J \ ( A u. B ) ) e. J )
9 3 cldss 
 |-  ( A e. ( Clsd ` J ) -> A C_ U. J )
10 3 cldss 
 |-  ( B e. ( Clsd ` J ) -> B C_ U. J )
11 9 10 anim12i 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A C_ U. J /\ B C_ U. J ) )
12 unss 
 |-  ( ( A C_ U. J /\ B C_ U. J ) <-> ( A u. B ) C_ U. J )
13 11 12 sylib 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A u. B ) C_ U. J )
14 3 iscld2 
 |-  ( ( J e. Top /\ ( A u. B ) C_ U. J ) -> ( ( A u. B ) e. ( Clsd ` J ) <-> ( U. J \ ( A u. B ) ) e. J ) )
15 2 13 14 syl2an2r 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( ( A u. B ) e. ( Clsd ` J ) <-> ( U. J \ ( A u. B ) ) e. J ) )
16 8 15 mpbird 
 |-  ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A u. B ) e. ( Clsd ` J ) )