# 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 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → 𝑦𝐼 𝑆𝐶 )

### Proof

Step Hyp Ref Expression
1 dfiin2g ( ∀ 𝑦𝐼 𝑆𝐶 𝑦𝐼 𝑆 = { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } )
2 1 3ad2ant3 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → 𝑦𝐼 𝑆 = { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } )
3 simp1 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
4 uniiunlem ( ∀ 𝑦𝐼 𝑆𝐶 → ( ∀ 𝑦𝐼 𝑆𝐶 ↔ { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ⊆ 𝐶 ) )
5 4 ibi ( ∀ 𝑦𝐼 𝑆𝐶 → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ⊆ 𝐶 )
6 5 3ad2ant3 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ⊆ 𝐶 )
7 n0 ( 𝐼 ≠ ∅ ↔ ∃ 𝑦 𝑦𝐼 )
8 nfra1 𝑦𝑦𝐼 𝑆𝐶
9 nfre1 𝑦𝑦𝐼 𝑠 = 𝑆
10 9 nfab 𝑦 { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 }
11 nfcv 𝑦
12 10 11 nfne 𝑦 { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅
13 8 12 nfim 𝑦 ( ∀ 𝑦𝐼 𝑆𝐶 → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ )
14 rsp ( ∀ 𝑦𝐼 𝑆𝐶 → ( 𝑦𝐼𝑆𝐶 ) )
15 14 com12 ( 𝑦𝐼 → ( ∀ 𝑦𝐼 𝑆𝐶𝑆𝐶 ) )
16 elisset ( 𝑆𝐶 → ∃ 𝑠 𝑠 = 𝑆 )
17 rspe ( ( 𝑦𝐼 ∧ ∃ 𝑠 𝑠 = 𝑆 ) → ∃ 𝑦𝐼𝑠 𝑠 = 𝑆 )
18 17 ex ( 𝑦𝐼 → ( ∃ 𝑠 𝑠 = 𝑆 → ∃ 𝑦𝐼𝑠 𝑠 = 𝑆 ) )
19 16 18 syl5 ( 𝑦𝐼 → ( 𝑆𝐶 → ∃ 𝑦𝐼𝑠 𝑠 = 𝑆 ) )
20 rexcom4 ( ∃ 𝑦𝐼𝑠 𝑠 = 𝑆 ↔ ∃ 𝑠𝑦𝐼 𝑠 = 𝑆 )
21 19 20 syl6ib ( 𝑦𝐼 → ( 𝑆𝐶 → ∃ 𝑠𝑦𝐼 𝑠 = 𝑆 ) )
22 15 21 syld ( 𝑦𝐼 → ( ∀ 𝑦𝐼 𝑆𝐶 → ∃ 𝑠𝑦𝐼 𝑠 = 𝑆 ) )
23 abn0 ( { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ ↔ ∃ 𝑠𝑦𝐼 𝑠 = 𝑆 )
24 22 23 syl6ibr ( 𝑦𝐼 → ( ∀ 𝑦𝐼 𝑆𝐶 → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ ) )
25 13 24 exlimi ( ∃ 𝑦 𝑦𝐼 → ( ∀ 𝑦𝐼 𝑆𝐶 → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ ) )
26 7 25 sylbi ( 𝐼 ≠ ∅ → ( ∀ 𝑦𝐼 𝑆𝐶 → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ ) )
27 26 imp ( ( 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ )
28 27 3adant1 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ )
29 mreintcl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ⊆ 𝐶 ∧ { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ≠ ∅ ) → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ∈ 𝐶 )
30 3 6 28 29 syl3anc ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → { 𝑠 ∣ ∃ 𝑦𝐼 𝑠 = 𝑆 } ∈ 𝐶 )
31 2 30 eqeltrd ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦𝐼 𝑆𝐶 ) → 𝑦𝐼 𝑆𝐶 )