mreiincl

Description: A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015)

		Ref	Expression
	Assertion	mreiincl	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> \|^\|_ y e. I S e. C )

Proof

Step	Hyp	Ref	Expression
1		dfiin2g	\|- ( A. y e. I S e. C -> \|^\|_ y e. I S = \|^\| { s \| E. y e. I s = S } )
2	1	3ad2ant3	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> \|^\|_ y e. I S = \|^\| { s \| E. y e. I s = S } )
3		simp1	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> C e. ( Moore ` X ) )
4		uniiunlem	\|- ( A. y e. I S e. C -> ( A. y e. I S e. C <-> { s \| E. y e. I s = S } C_ C ) )
5	4	ibi	\|- ( A. y e. I S e. C -> { s \| E. y e. I s = S } C_ C )
6	5	3ad2ant3	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> { s \| E. y e. I s = S } C_ C )
7		n0	\|- ( I =/= (/) <-> E. y y e. I )
8		nfra1	\|- F/ y A. y e. I S e. C
9		nfre1	\|- F/ y E. y e. I s = S
10	9	nfab	\|- F/_ y { s \| E. y e. I s = S }
11		nfcv	\|- F/_ y (/)
12	10 11	nfne	\|- F/ y { s \| E. y e. I s = S } =/= (/)
13	8 12	nfim	\|- F/ y ( A. y e. I S e. C -> { s \| E. y e. I s = S } =/= (/) )
14		rsp	\|- ( A. y e. I S e. C -> ( y e. I -> S e. C ) )
15	14	com12	\|- ( y e. I -> ( A. y e. I S e. C -> S e. C ) )
16		elisset	\|- ( S e. C -> E. s s = S )
17		rspe	\|- ( ( y e. I /\ E. s s = S ) -> E. y e. I E. s s = S )
18	17	ex	\|- ( y e. I -> ( E. s s = S -> E. y e. I E. s s = S ) )
19	16 18	syl5	\|- ( y e. I -> ( S e. C -> E. y e. I E. s s = S ) )
20		rexcom4	\|- ( E. y e. I E. s s = S <-> E. s E. y e. I s = S )
21	19 20	imbitrdi	\|- ( y e. I -> ( S e. C -> E. s E. y e. I s = S ) )
22	15 21	syld	\|- ( y e. I -> ( A. y e. I S e. C -> E. s E. y e. I s = S ) )
23		abn0	\|- ( { s \| E. y e. I s = S } =/= (/) <-> E. s E. y e. I s = S )
24	22 23	imbitrrdi	\|- ( y e. I -> ( A. y e. I S e. C -> { s \| E. y e. I s = S } =/= (/) ) )
25	13 24	exlimi	\|- ( E. y y e. I -> ( A. y e. I S e. C -> { s \| E. y e. I s = S } =/= (/) ) )
26	7 25	sylbi	\|- ( I =/= (/) -> ( A. y e. I S e. C -> { s \| E. y e. I s = S } =/= (/) ) )
27	26	imp	\|- ( ( I =/= (/) /\ A. y e. I S e. C ) -> { s \| E. y e. I s = S } =/= (/) )
28	27	3adant1	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> { s \| E. y e. I s = S } =/= (/) )
29		mreintcl	\|- ( ( C e. ( Moore ` X ) /\ { s \| E. y e. I s = S } C_ C /\ { s \| E. y e. I s = S } =/= (/) ) -> \|^\| { s \| E. y e. I s = S } e. C )
30	3 6 28 29	syl3anc	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> \|^\| { s \| E. y e. I s = S } e. C )
31	2 30	eqeltrd	\|- ( ( C e. ( Moore ` X ) /\ I =/= (/) /\ A. y e. I S e. C ) -> \|^\|_ y e. I S e. C )

Metamath Proof Explorer

Theorem mreiincl

Proof