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 ) )