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

Metamath Proof Explorer

Theorem mreincl

Description: Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mreincl 
|- ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> ( A i^i B ) e. C )

Proof

Step Hyp Ref Expression
1 intprg 
 |-  ( ( A e. C /\ B e. C ) -> |^| { A , B } = ( A i^i B ) )
2 1 3adant1 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> |^| { A , B } = ( A i^i B ) )
3 simp1 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> C e. ( Moore ` X ) )
4 prssi 
 |-  ( ( A e. C /\ B e. C ) -> { A , B } C_ C )
5 4 3adant1 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> { A , B } C_ C )
6 prnzg 
 |-  ( A e. C -> { A , B } =/= (/) )
7 6 3ad2ant2 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> { A , B } =/= (/) )
8 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ { A , B } C_ C /\ { A , B } =/= (/) ) -> |^| { A , B } e. C )
9 3 5 7 8 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> |^| { A , B } e. C )
10 2 9 eqeltrrd 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C /\ B e. C ) -> ( A i^i B ) e. C )