Metamath Proof Explorer

Theorem fnmre

Description: The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion fnmre ⊢ Moore Fn V

Proof

Step Hyp Ref Expression
1 vpwex ⊢ 𝒫 x ∈ V
2 1 pwex ⊢ 𝒫 𝒫 x ∈ V
3 2 rabex ⊢ c ∈ 𝒫 𝒫 x | x ∈ c ∧ ∀ s ∈ 𝒫 c s ≠ ∅ → ⋂ s ∈ c ∈ V
4 df-mre ⊢ Moore = x ∈ V ⟼ c ∈ 𝒫 𝒫 x | x ∈ c ∧ ∀ s ∈ 𝒫 c s ≠ ∅ → ⋂ s ∈ c
5 3 4 fnmpti ⊢ Moore Fn V