Metamath Proof Explorer

Theorem f11o

Description: Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998)

Ref Expression
Hypothesis f11o.1 
|- F e. _V
Assertion f11o 
|- ( F : A -1-1-> B <-> E. x ( F : A -1-1-onto-> x /\ x C_ B ) )

Proof

Step Hyp Ref Expression
1 f11o.1 
 |-  F e. _V
2 1 ffoss 
 |-  ( F : A --> B <-> E. x ( F : A -onto-> x /\ x C_ B ) )
3 2 anbi1i 
 |-  ( ( F : A --> B /\ Fun `' F ) <-> ( E. x ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
4 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
5 dff1o3 
 |-  ( F : A -1-1-onto-> x <-> ( F : A -onto-> x /\ Fun `' F ) )
6 5 anbi1i 
 |-  ( ( F : A -1-1-onto-> x /\ x C_ B ) <-> ( ( F : A -onto-> x /\ Fun `' F ) /\ x C_ B ) )
7 an32 
 |-  ( ( ( F : A -onto-> x /\ Fun `' F ) /\ x C_ B ) <-> ( ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
8 6 7 bitri 
 |-  ( ( F : A -1-1-onto-> x /\ x C_ B ) <-> ( ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
9 8 exbii 
 |-  ( E. x ( F : A -1-1-onto-> x /\ x C_ B ) <-> E. x ( ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
10 19.41v 
 |-  ( E. x ( ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) <-> ( E. x ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
11 9 10 bitri 
 |-  ( E. x ( F : A -1-1-onto-> x /\ x C_ B ) <-> ( E. x ( F : A -onto-> x /\ x C_ B ) /\ Fun `' F ) )
12 3 4 11 3bitr4i 
 |-  ( F : A -1-1-> B <-> E. x ( F : A -1-1-onto-> x /\ x C_ B ) )