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

Metamath Proof Explorer

Theorem fnmrc

Description: Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fnmrc mrCls Fn ∪ ran Moore

Proof

Step Hyp Ref Expression
1 df-mrc ⊢ mrCls = ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )
2 1 fnmpt ⊢ ( ∀ 𝑐 ∈ ∪ ran Moore ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V → mrCls Fn ∪ ran Moore )
3 mreunirn ⊢ ( 𝑐 ∈ ∪ ran Moore ↔ 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) )
4 mrcflem ⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 )
5 fssxp ⊢ ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
6 4 5 syl ⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
7 vuniex ⊢ ∪ 𝑐 ∈ V
8 7 pwex ⊢ 𝒫 ∪ 𝑐 ∈ V
9 vex ⊢ 𝑐 ∈ V
10 8 9 xpex ⊢ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V
11 ssexg ⊢ ( ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∧ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
12 6 10 11 sylancl ⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
13 3 12 sylbi ⊢ ( 𝑐 ∈ ∪ ran Moore → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
14 2 13 mprg ⊢ mrCls Fn ∪ ran Moore