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