This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mreriincl

Description: The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion mreriincl 
|- ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) -> ( X i^i |^|_ y e. I S ) e. C )

Proof

Step Hyp Ref Expression
1 riin0 
 |-  ( I = (/) -> ( X i^i |^|_ y e. I S ) = X )
2 1 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I = (/) ) -> ( X i^i |^|_ y e. I S ) = X )
3 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
4 3 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I = (/) ) -> X e. C )
5 2 4 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I = (/) ) -> ( X i^i |^|_ y e. I S ) e. C )
6 mress 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> S C_ X )
7 6 ex 
 |-  ( C e. ( Moore ` X ) -> ( S e. C -> S C_ X ) )
8 7 ralimdv 
 |-  ( C e. ( Moore ` X ) -> ( A. y e. I S e. C -> A. y e. I S C_ X ) )
9 8 imp 
 |-  ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) -> A. y e. I S C_ X )
10 riinn0 
 |-  ( ( A. y e. I S C_ X /\ I =/= (/) ) -> ( X i^i |^|_ y e. I S ) = |^|_ y e. I S )
11 9 10 sylan 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> ( X i^i |^|_ y e. I S ) = |^|_ y e. I S )
12 simpll 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> C e. ( Moore ` X ) )
13 simpr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> I =/= (/) )
14 simplr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> A. y e. I S e. C )
15 mreiincl 
 |-  ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> |^|_ y e. I S e. C )
16 12 13 14 15 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> |^|_ y e. I S e. C )
17 11 16 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) /\ I =/= (/) ) -> ( X i^i |^|_ y e. I S ) e. C )
18 5 17 pm2.61dane 
 |-  ( ( C e. ( Moore ` X ) /\ A. y e. I S e. C ) -> ( X i^i |^|_ y e. I S ) e. C )