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

Metamath Proof Explorer

Theorem f1dmex

Description: If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep . (Contributed by NM, 4-Sep-2004)

Ref Expression
Assertion f1dmex 
|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 1 frnd 
 |-  ( F : A -1-1-> B -> ran F C_ B )
3 ssexg 
 |-  ( ( ran F C_ B /\ B e. C ) -> ran F e. _V )
4 2 3 sylan 
 |-  ( ( F : A -1-1-> B /\ B e. C ) -> ran F e. _V )
5 4 ex 
 |-  ( F : A -1-1-> B -> ( B e. C -> ran F e. _V ) )
6 f1cnv 
 |-  ( F : A -1-1-> B -> `' F : ran F -1-1-onto-> A )
7 f1ofo 
 |-  ( `' F : ran F -1-1-onto-> A -> `' F : ran F -onto-> A )
8 6 7 syl 
 |-  ( F : A -1-1-> B -> `' F : ran F -onto-> A )
9 focdmex 
 |-  ( ran F e. _V -> ( `' F : ran F -onto-> A -> A e. _V ) )
10 5 8 9 syl6ci 
 |-  ( F : A -1-1-> B -> ( B e. C -> A e. _V ) )
11 10 imp 
 |-  ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )