Metamath Proof Explorer

Theorem mrcfval

Description: Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 fvssunirn ⊢ ( Moore ‘ 𝑋 ) ⊆ ∪ ran Moore
3 2 sseli ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ∈ ∪ ran Moore )
4 unieq ⊢ ( 𝑐 = 𝐶 → ∪ 𝑐 = ∪ 𝐶 )
5 4 pweqd ⊢ ( 𝑐 = 𝐶 → 𝒫 ∪ 𝑐 = 𝒫 ∪ 𝐶 )
6 rabeq ⊢ ( 𝑐 = 𝐶 → { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } = { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } )
7 6 inteqd ⊢ ( 𝑐 = 𝐶 → ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } )
8 5 7 mpteq12dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) = ( 𝑥 ∈ 𝒫 ∪ 𝐶 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
9 df-mrc ⊢ mrCls = ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )
10 mreunirn ⊢ ( 𝑐 ∈ ∪ ran Moore ↔ 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) )
11 mrcflem ⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 )
12 10 11 sylbi ⊢ ( 𝑐 ∈ ∪ ran Moore → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 )
13 fssxp ⊢ ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
14 12 13 syl ⊢ ( 𝑐 ∈ ∪ ran Moore → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
15 vuniex ⊢ ∪ 𝑐 ∈ V
16 15 pwex ⊢ 𝒫 ∪ 𝑐 ∈ V
17 vex ⊢ 𝑐 ∈ V
18 16 17 xpex ⊢ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V
19 ssexg ⊢ ( ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∧ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
20 14 18 19 sylancl ⊢ ( 𝑐 ∈ ∪ ran Moore → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
21 8 9 20 fvmpt3 ⊢ ( 𝐶 ∈ ∪ ran Moore → ( mrCls ‘ 𝐶 ) = ( 𝑥 ∈ 𝒫 ∪ 𝐶 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
22 3 21 syl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( mrCls ‘ 𝐶 ) = ( 𝑥 ∈ 𝒫 ∪ 𝐶 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
23 mreuni ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )
24 23 pweqd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝒫 ∪ 𝐶 = 𝒫 𝑋 )
25 24 mpteq1d ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑥 ∈ 𝒫 ∪ 𝐶 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
26 22 25 eqtrd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( mrCls ‘ 𝐶 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )
27 1 26 syl5eq ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) )