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

Metamath Proof Explorer

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 ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )