Theorem mrcval

Description: Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Fan Zheng, 6-Jun-2016)

	Ref	Expression
Hypothesis	mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrcval	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	mrcfval	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
3	2	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝐹 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
4		sseq1	⊢ ( 𝑥 = 𝑈 → ( 𝑥 ⊆ 𝑠 ↔ 𝑈 ⊆ 𝑠 ) )
5	4	rabbidv	⊢ ( 𝑥 = 𝑈 → { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
6	5	inteqd	⊢ ( 𝑥 = 𝑈 → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
7	6	adantl	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) ∧ 𝑥 = 𝑈 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
8		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
9		elpw2g	⊢ ( 𝑋 ∈ 𝐶 → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
10	8 9	syl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
11	10	biimpar	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ∈ 𝒫 𝑋 )
12		sseq2	⊢ ( 𝑠 = 𝑋 → ( 𝑈 ⊆ 𝑠 ↔ 𝑈 ⊆ 𝑋 ) )
13	8	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑋 ∈ 𝐶 )
14		simpr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 )
15	12 13 14	elrabd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑋 ∈ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
16	15	ne0d	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ≠ ∅ )
17		intex	⊢ ( { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ≠ ∅ ↔ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ∈ V )
18	16 17	sylib	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ∈ V )
19	3 7 11 18	fvmptd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )