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	|- ~P x e. _V
2	1	pwex	|- ~P ~P x e. _V
3	2	rabex	|- { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } e. _V
4		df-mre	|- Moore = ( x e. _V |-> { c e. ~P ~P x | ( x e. c /\ A. s e. ~P c ( s =/= (/) -> |^| s e. c ) ) } )
5	3 4	fnmpti	|- Moore Fn _V