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

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 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