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 = c ∈ ⋃ ran ⁡ Moore ⟼ x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s
2 1 fnmpt ⊢ ∀ c ∈ ⋃ ran ⁡ Moore x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ∈ V → mrCls Fn ⋃ ran ⁡ Moore
3 mreunirn ⊢ c ∈ ⋃ ran ⁡ Moore ↔ c ∈ Moore ⁡ ⋃ c
4 mrcflem ⊢ c ∈ Moore ⁡ ⋃ c → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s : 𝒫 ⋃ c ⟶ c
5 fssxp ⊢ x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s : 𝒫 ⋃ c ⟶ c → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ⊆ 𝒫 ⋃ c × c
6 4 5 syl ⊢ c ∈ Moore ⁡ ⋃ c → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ⊆ 𝒫 ⋃ c × c
7 vuniex ⊢ ⋃ c ∈ V
8 7 pwex ⊢ 𝒫 ⋃ c ∈ V
9 vex ⊢ c ∈ V
10 8 9 xpex ⊢ 𝒫 ⋃ c × c ∈ V
11 ssexg ⊢ x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ⊆ 𝒫 ⋃ c × c ∧ 𝒫 ⋃ c × c ∈ V → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ∈ V
12 6 10 11 sylancl ⊢ c ∈ Moore ⁡ ⋃ c → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ∈ V
13 3 12 sylbi ⊢ c ∈ ⋃ ran ⁡ Moore → x ∈ 𝒫 ⋃ c ⟼ ⋂ s ∈ c | x ⊆ s ∈ V
14 2 13 mprg ⊢ mrCls Fn ⋃ ran ⁡ Moore