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 )