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

Metamath Proof Explorer

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 )