Metamath Proof Explorer

Theorem 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 syl6ib 
 |-  ( 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 syl6ibr 
 |-  ( 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 )