Metamath Proof Explorer


Theorem fnexALT

Description: Alternate proof of fnex , derived using the Axiom of Replacement in the form of funimaexg . This version uses ax-pow and ax-un , whereas fnex does not. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fnexALT FFnAABFV

Proof

Step Hyp Ref Expression
1 fnrel FFnARelF
2 relssdmrn RelFFdomF×ranF
3 1 2 syl FFnAFdomF×ranF
4 3 adantr FFnAABFdomF×ranF
5 fndm FFnAdomF=A
6 5 eleq1d FFnAdomFBAB
7 6 biimpar FFnAABdomFB
8 fnfun FFnAFunF
9 funimaexg FunFABFAV
10 8 9 sylan FFnAABFAV
11 imadmrn FdomF=ranF
12 5 imaeq2d FFnAFdomF=FA
13 11 12 eqtr3id FFnAranF=FA
14 13 eleq1d FFnAranFVFAV
15 14 biimpar FFnAFAVranFV
16 10 15 syldan FFnAABranFV
17 xpexg domFBranFVdomF×ranFV
18 7 16 17 syl2anc FFnAABdomF×ranFV
19 ssexg FdomF×ranFdomF×ranFVFV
20 4 18 19 syl2anc FFnAABFV