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

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 )