Metamath Proof Explorer

Theorem f1ofveu

Description: There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006)

Ref Expression
Assertion f1ofveu 
|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> E! x e. A ( F ` x ) = C )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
2 f1of 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B --> A )
3 1 2 syl 
 |-  ( F : A -1-1-onto-> B -> `' F : B --> A )
4 feu 
 |-  ( ( `' F : B --> A /\ C e. B ) -> E! x e. A <. C , x >. e. `' F )
5 3 4 sylan 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> E! x e. A <. C , x >. e. `' F )
6 f1ocnvfvb 
 |-  ( ( F : A -1-1-onto-> B /\ x e. A /\ C e. B ) -> ( ( F ` x ) = C <-> ( `' F ` C ) = x ) )
7 6 3com23 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B /\ x e. A ) -> ( ( F ` x ) = C <-> ( `' F ` C ) = x ) )
8 dff1o4 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
9 8 simprbi 
 |-  ( F : A -1-1-onto-> B -> `' F Fn B )
10 fnopfvb 
 |-  ( ( `' F Fn B /\ C e. B ) -> ( ( `' F ` C ) = x <-> <. C , x >. e. `' F ) )
11 10 3adant3 
 |-  ( ( `' F Fn B /\ C e. B /\ x e. A ) -> ( ( `' F ` C ) = x <-> <. C , x >. e. `' F ) )
12 9 11 syl3an1 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B /\ x e. A ) -> ( ( `' F ` C ) = x <-> <. C , x >. e. `' F ) )
13 7 12 bitrd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B /\ x e. A ) -> ( ( F ` x ) = C <-> <. C , x >. e. `' F ) )
14 13 3expa 
 |-  ( ( ( F : A -1-1-onto-> B /\ C e. B ) /\ x e. A ) -> ( ( F ` x ) = C <-> <. C , x >. e. `' F ) )
15 14 reubidva 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( E! x e. A ( F ` x ) = C <-> E! x e. A <. C , x >. e. `' F ) )
16 5 15 mpbird 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> E! x e. A ( F ` x ) = C )