Metamath Proof Explorer

Theorem mreintcl

Description: A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 elpw2g 
 |-  ( C e. ( Moore ` X ) -> ( S e. ~P C <-> S C_ C ) )
2 1 biimpar 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C ) -> S e. ~P C )
3 2 3adant3 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> S e. ~P C )
4 ismre 
 |-  ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
5 4 simp3bi 
 |-  ( C e. ( Moore ` X ) -> A. s e. ~P C ( s =/= (/) -> |^| s e. C ) )
6 5 3ad2ant1 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> A. s e. ~P C ( s =/= (/) -> |^| s e. C ) )
7 simp3 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> S =/= (/) )
8 neeq1 
 |-  ( s = S -> ( s =/= (/) <-> S =/= (/) ) )
9 inteq 
 |-  ( s = S -> |^| s = |^| S )
10 9 eleq1d 
 |-  ( s = S -> ( |^| s e. C <-> |^| S e. C ) )
11 8 10 imbi12d 
 |-  ( s = S -> ( ( s =/= (/) -> |^| s e. C ) <-> ( S =/= (/) -> |^| S e. C ) ) )
12 11 rspcva 
 |-  ( ( S e. ~P C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) -> ( S =/= (/) -> |^| S e. C ) )
13 12 3impia 
 |-  ( ( S e. ~P C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) /\ S =/= (/) ) -> |^| S e. C )
14 3 6 7 13 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C /\ S =/= (/) ) -> |^| S e. C )