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 )