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 )