This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrdi ⊢ ( 𝑦 ∈ 𝐼 → ( 𝑆 ∈ 𝐶 → ∃ 𝑠 ∃ 𝑦 ∈ 𝐼 𝑠 = 𝑆 ) )
22 15 21 syld ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → ∃ 𝑠 ∃ 𝑦 ∈ 𝐼 𝑠 = 𝑆 ) )
23 abn0 ⊢ ( { 𝑠 ∣ ∃ 𝑦 ∈ 𝐼 𝑠 = 𝑆 } ≠ ∅ ↔ ∃ 𝑠 ∃ 𝑦 ∈ 𝐼 𝑠 = 𝑆 )
24 22 23 imbitrrdi ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → { 𝑠 ∣ ∃ 𝑦 ∈ 𝐼 𝑠 = 𝑆 } ≠ ∅ ) )
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 ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 )