Metamath Proof Explorer

Theorem resfunexgALT

Description: Alternate proof of resfunexg , shorter but requiring ax-pow and ax-un . (Contributed by NM, 7-Apr-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion resfunexgALT 
|- ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )

Proof

Step Hyp Ref Expression
1 dmresexg 
 |-  ( B e. C -> dom ( A |` B ) e. _V )
2 1 adantl 
 |-  ( ( Fun A /\ B e. C ) -> dom ( A |` B ) e. _V )
3 df-ima 
 |-  ( A " B ) = ran ( A |` B )
4 funimaexg 
 |-  ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V )
5 3 4 eqeltrrid 
 |-  ( ( Fun A /\ B e. C ) -> ran ( A |` B ) e. _V )
6 2 5 jca 
 |-  ( ( Fun A /\ B e. C ) -> ( dom ( A |` B ) e. _V /\ ran ( A |` B ) e. _V ) )
7 xpexg 
 |-  ( ( dom ( A |` B ) e. _V /\ ran ( A |` B ) e. _V ) -> ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V )
8 relres 
 |-  Rel ( A |` B )
9 relssdmrn 
 |-  ( Rel ( A |` B ) -> ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) ) )
10 8 9 ax-mp 
 |-  ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) )
11 ssexg 
 |-  ( ( ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) ) /\ ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V ) -> ( A |` B ) e. _V )
12 10 11 mpan 
 |-  ( ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V -> ( A |` B ) e. _V )
13 6 7 12 3syl 
 |-  ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )