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

Metamath Proof Explorer

Theorem mrcflem

Description: The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Assertion mrcflem 
|- ( C e. ( Moore ` X ) -> ( x e. ~P X |-> |^| { s e. C | x C_ s } ) : ~P X --> C )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> C e. ( Moore ` X ) )
2 ssrab2 
 |-  { s e. C | x C_ s } C_ C
3 2 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> { s e. C | x C_ s } C_ C )
4 sseq2 
 |-  ( s = X -> ( x C_ s <-> x C_ X ) )
5 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
6 5 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> X e. C )
7 elpwi 
 |-  ( x e. ~P X -> x C_ X )
8 7 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> x C_ X )
9 4 6 8 elrabd 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> X e. { s e. C | x C_ s } )
10 9 ne0d 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> { s e. C | x C_ s } =/= (/) )
11 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ { s e. C | x C_ s } C_ C /\ { s e. C | x C_ s } =/= (/) ) -> |^| { s e. C | x C_ s } e. C )
12 1 3 10 11 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ x e. ~P X ) -> |^| { s e. C | x C_ s } e. C )
13 12 fmpttd 
 |-  ( C e. ( Moore ` X ) -> ( x e. ~P X |-> |^| { s e. C | x C_ s } ) : ~P X --> C )