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

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	⊢ 𝒫 𝑥 ∈ V
2	1	pwex	⊢ 𝒫 𝒫 𝑥 ∈ V
3	2	rabex	⊢ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } ∈ V
4		df-mre	⊢ Moore = ( 𝑥 ∈ V ↦ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥 ∈ 𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐 ) ) } )
5	3 4	fnmpti	⊢ Moore Fn V