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