Metamath Proof Explorer

Theorem ffoss

Description: Relationship between a mapping and an onto mapping. Figure 38 of Enderton p. 145. (Contributed by NM, 10-May-1998)

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

Proof

Step Hyp Ref Expression
1 f11o.1 
 |-  F e. _V
2 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
3 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
4 3 anbi1i 
 |-  ( ( F Fn A /\ ran F C_ B ) <-> ( F : A -onto-> ran F /\ ran F C_ B ) )
5 2 4 bitri 
 |-  ( F : A --> B <-> ( F : A -onto-> ran F /\ ran F C_ B ) )
6 1 rnex 
 |-  ran F e. _V
7 foeq3 
 |-  ( x = ran F -> ( F : A -onto-> x <-> F : A -onto-> ran F ) )
8 sseq1 
 |-  ( x = ran F -> ( x C_ B <-> ran F C_ B ) )
9 7 8 anbi12d 
 |-  ( x = ran F -> ( ( F : A -onto-> x /\ x C_ B ) <-> ( F : A -onto-> ran F /\ ran F C_ B ) ) )
10 6 9 spcev 
 |-  ( ( F : A -onto-> ran F /\ ran F C_ B ) -> E. x ( F : A -onto-> x /\ x C_ B ) )
11 5 10 sylbi 
 |-  ( F : A --> B -> E. x ( F : A -onto-> x /\ x C_ B ) )
12 fof 
 |-  ( F : A -onto-> x -> F : A --> x )
13 fss 
 |-  ( ( F : A --> x /\ x C_ B ) -> F : A --> B )
14 12 13 sylan 
 |-  ( ( F : A -onto-> x /\ x C_ B ) -> F : A --> B )
15 14 exlimiv 
 |-  ( E. x ( F : A -onto-> x /\ x C_ B ) -> F : A --> B )
16 11 15 impbii 
 |-  ( F : A --> B <-> E. x ( F : A -onto-> x /\ x C_ B ) )