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
|- ( ( F Fn A /\ A e. B ) -> F e. _V )

Proof

Step Hyp Ref Expression
1 fnrel
 |-  ( F Fn A -> Rel F )
2 relssdmrn
 |-  ( Rel F -> F C_ ( dom F X. ran F ) )
3 1 2 syl
 |-  ( F Fn A -> F C_ ( dom F X. ran F ) )
4 3 adantr
 |-  ( ( F Fn A /\ A e. B ) -> F C_ ( dom F X. ran F ) )
5 fndm
 |-  ( F Fn A -> dom F = A )
6 5 eleq1d
 |-  ( F Fn A -> ( dom F e. B <-> A e. B ) )
7 6 biimpar
 |-  ( ( F Fn A /\ A e. B ) -> dom F e. B )
8 fnfun
 |-  ( F Fn A -> Fun F )
9 funimaexg
 |-  ( ( Fun F /\ A e. B ) -> ( F " A ) e. _V )
10 8 9 sylan
 |-  ( ( F Fn A /\ A e. B ) -> ( F " A ) e. _V )
11 imadmrn
 |-  ( F " dom F ) = ran F
12 5 imaeq2d
 |-  ( F Fn A -> ( F " dom F ) = ( F " A ) )
13 11 12 eqtr3id
 |-  ( F Fn A -> ran F = ( F " A ) )
14 13 eleq1d
 |-  ( F Fn A -> ( ran F e. _V <-> ( F " A ) e. _V ) )
15 14 biimpar
 |-  ( ( F Fn A /\ ( F " A ) e. _V ) -> ran F e. _V )
16 10 15 syldan
 |-  ( ( F Fn A /\ A e. B ) -> ran F e. _V )
17 xpexg
 |-  ( ( dom F e. B /\ ran F e. _V ) -> ( dom F X. ran F ) e. _V )
18 7 16 17 syl2anc
 |-  ( ( F Fn A /\ A e. B ) -> ( dom F X. ran F ) e. _V )
19 ssexg
 |-  ( ( F C_ ( dom F X. ran F ) /\ ( dom F X. ran F ) e. _V ) -> F e. _V )
20 4 18 19 syl2anc
 |-  ( ( F Fn A /\ A e. B ) -> F e. _V )