Theorem mapex

Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003)

	Ref	Expression
Assertion	mapex	|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		fssxp	|- ( f : A --> B -> f C_ ( A X. B ) )
2	1	ss2abi	|- { f | f : A --> B } C_ { f | f C_ ( A X. B ) }
3		df-pw	|- ~P ( A X. B ) = { f | f C_ ( A X. B ) }
4	2 3	sseqtrri	|- { f | f : A --> B } C_ ~P ( A X. B )
5		xpexg	|- ( ( A e. C /\ B e. D ) -> ( A X. B ) e. _V )
6	5	pwexd	|- ( ( A e. C /\ B e. D ) -> ~P ( A X. B ) e. _V )
7		ssexg	|- ( ( { f | f : A --> B } C_ ~P ( A X. B ) /\ ~P ( A X. B ) e. _V ) -> { f | f : A --> B } e. _V )
8	4 6 7	sylancr	|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )