Theorem mrcflem

Description: The domain and range 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 )