Theorem fnmrc

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

	Ref	Expression
Assertion	fnmrc	|- mrCls Fn U. ran Moore

Proof

Step	Hyp	Ref	Expression
1		df-mrc	|- mrCls = ( c e. U. ran Moore |-> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) )
2	1	fnmpt	|- ( A. c e. U. ran Moore ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V -> mrCls Fn U. ran Moore )
3		mreunirn	|- ( c e. U. ran Moore <-> c e. ( Moore ` U. c ) )
4		mrcflem	|- ( c e. ( Moore ` U. c ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) : ~P U. c --> c )
5		fssxp	|- ( ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) : ~P U. c --> c -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) )
6	4 5	syl	|- ( c e. ( Moore ` U. c ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) )
7		vuniex	|- U. c e. _V
8	7	pwex	|- ~P U. c e. _V
9		vex	|- c e. _V
10	8 9	xpex	|- ( ~P U. c X. c ) e. _V
11		ssexg	|- ( ( ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) C_ ( ~P U. c X. c ) /\ ( ~P U. c X. c ) e. _V ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V )
12	6 10 11	sylancl	|- ( c e. ( Moore ` U. c ) -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V )
13	3 12	sylbi	|- ( c e. U. ran Moore -> ( x e. ~P U. c |-> |^| { s e. c | x C_ s } ) e. _V )
14	2 13	mprg	|- mrCls Fn U. ran Moore