Theorem mapexOLD

Description: Obsolete version of mapex as of 17-Jun-2025. (Contributed by Raph Levien, 4-Dec-2003) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	mapexOLD	|- ( ( 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 )