Metamath Proof Explorer

Theorem iincld

Description: The indexed intersection of a collection B ( x ) of closed sets is closed. Theorem 6.1(2) of Munkres p. 93. (Contributed by NM, 5-Oct-2006) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iincld 
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 cldss 
 |-  ( B e. ( Clsd ` J ) -> B C_ U. J )
3 dfss4 
 |-  ( B C_ U. J <-> ( U. J \ ( U. J \ B ) ) = B )
4 2 3 sylib 
 |-  ( B e. ( Clsd ` J ) -> ( U. J \ ( U. J \ B ) ) = B )
5 4 ralimi 
 |-  ( A. x e. A B e. ( Clsd ` J ) -> A. x e. A ( U. J \ ( U. J \ B ) ) = B )
6 iineq2 
 |-  ( A. x e. A ( U. J \ ( U. J \ B ) ) = B -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B )
7 5 6 syl 
 |-  ( A. x e. A B e. ( Clsd ` J ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B )
8 7 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B )
9 iindif2 
 |-  ( A =/= (/) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = ( U. J \ U_ x e. A ( U. J \ B ) ) )
10 9 adantr 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = ( U. J \ U_ x e. A ( U. J \ B ) ) )
11 8 10 eqtr3d 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B = ( U. J \ U_ x e. A ( U. J \ B ) ) )
12 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> E. x e. A B e. ( Clsd ` J ) )
13 cldrcl 
 |-  ( B e. ( Clsd ` J ) -> J e. Top )
14 13 rexlimivw 
 |-  ( E. x e. A B e. ( Clsd ` J ) -> J e. Top )
15 12 14 syl 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> J e. Top )
16 1 cldopn 
 |-  ( B e. ( Clsd ` J ) -> ( U. J \ B ) e. J )
17 16 ralimi 
 |-  ( A. x e. A B e. ( Clsd ` J ) -> A. x e. A ( U. J \ B ) e. J )
18 17 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> A. x e. A ( U. J \ B ) e. J )
19 iunopn 
 |-  ( ( J e. Top /\ A. x e. A ( U. J \ B ) e. J ) -> U_ x e. A ( U. J \ B ) e. J )
20 15 18 19 syl2anc 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> U_ x e. A ( U. J \ B ) e. J )
21 1 opncld 
 |-  ( ( J e. Top /\ U_ x e. A ( U. J \ B ) e. J ) -> ( U. J \ U_ x e. A ( U. J \ B ) ) e. ( Clsd ` J ) )
22 15 20 21 syl2anc 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> ( U. J \ U_ x e. A ( U. J \ B ) ) e. ( Clsd ` J ) )
23 11 22 eqeltrd 
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B e. ( Clsd ` J ) )