Metamath Proof Explorer

Theorem mrerintcl

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

Ref Expression
Assertion mrerintcl 
|- ( ( C e. ( Moore ` X ) /\ S C_ C ) -> ( X i^i |^| S ) e. C )

Proof

Step Hyp Ref Expression
1 rint0 
 |-  ( S = (/) -> ( X i^i |^| S ) = X )
2 1 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ S C_ C ) /\ S = (/) ) -> ( X i^i |^| S ) = X )
3 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
4 3 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ S C_ C ) /\ S = (/) ) -> X e. C )
5 2 4 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ S C_ C ) /\ S = (/) ) -> ( X i^i |^| S ) e. C )
6 simp2 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> S C_ C )
7 mresspw 
 |-  ( C e. ( Moore ` X ) -> C C_ ~P X )
8 7 3ad2ant1 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> C C_ ~P X )
9 6 8 sstrd 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> S C_ ~P X )
10 simp3 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> S =/= (/) )
11 rintn0 
 |-  ( ( S C_ ~P X /\ S =/= (/) ) -> ( X i^i |^| S ) = |^| S )
12 9 10 11 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> ( X i^i |^| S ) = |^| S )
13 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> |^| S e. C )
14 12 13 eqeltrd 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> ( X i^i |^| S ) e. C )
15 14 3expa 
 |-  ( ( ( C e. ( Moore ` X ) /\ S C_ C ) /\ S =/= (/) ) -> ( X i^i |^| S ) e. C )
16 5 15 pm2.61dane 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C ) -> ( X i^i |^| S ) e. C )