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