Metamath Proof Explorer


Theorem riincld

Description: An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypothesis clscld.1
|- X = U. J
Assertion riincld
|- ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 clscld.1
 |-  X = U. J
2 riin0
 |-  ( A = (/) -> ( X i^i |^|_ x e. A B ) = X )
3 2 adantl
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A = (/) ) -> ( X i^i |^|_ x e. A B ) = X )
4 1 topcld
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
5 4 ad2antrr
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A = (/) ) -> X e. ( Clsd ` J ) )
6 3 5 eqeltrd
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A = (/) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )
7 4 ad2antrr
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A =/= (/) ) -> X e. ( Clsd ` J ) )
8 simpr
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A =/= (/) ) -> A =/= (/) )
9 simplr
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A =/= (/) ) -> A. x e. A B e. ( Clsd ` J ) )
10 iincld
 |-  ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B e. ( Clsd ` J ) )
11 8 9 10 syl2anc
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A =/= (/) ) -> |^|_ x e. A B e. ( Clsd ` J ) )
12 incld
 |-  ( ( X e. ( Clsd ` J ) /\ |^|_ x e. A B e. ( Clsd ` J ) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )
13 7 11 12 syl2anc
 |-  ( ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) /\ A =/= (/) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )
14 6 13 pm2.61dane
 |-  ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )