Metamath Proof Explorer

Theorem dffo4

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dffo4 
|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )

Proof

Step Hyp Ref Expression
1 dffo2 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )
2 simpl 
 |-  ( ( F : A --> B /\ ran F = B ) -> F : A --> B )
3 vex 
 |-  y e. _V
4 3 elrn 
 |-  ( y e. ran F <-> E. x x F y )
5 eleq2 
 |-  ( ran F = B -> ( y e. ran F <-> y e. B ) )
6 4 5 bitr3id 
 |-  ( ran F = B -> ( E. x x F y <-> y e. B ) )
7 6 biimpar 
 |-  ( ( ran F = B /\ y e. B ) -> E. x x F y )
8 7 adantll 
 |-  ( ( ( F : A --> B /\ ran F = B ) /\ y e. B ) -> E. x x F y )
9 ffn 
 |-  ( F : A --> B -> F Fn A )
10 fnbr 
 |-  ( ( F Fn A /\ x F y ) -> x e. A )
11 10 ex 
 |-  ( F Fn A -> ( x F y -> x e. A ) )
12 9 11 syl 
 |-  ( F : A --> B -> ( x F y -> x e. A ) )
13 12 ancrd 
 |-  ( F : A --> B -> ( x F y -> ( x e. A /\ x F y ) ) )
14 13 eximdv 
 |-  ( F : A --> B -> ( E. x x F y -> E. x ( x e. A /\ x F y ) ) )
15 df-rex 
 |-  ( E. x e. A x F y <-> E. x ( x e. A /\ x F y ) )
16 14 15 syl6ibr 
 |-  ( F : A --> B -> ( E. x x F y -> E. x e. A x F y ) )
17 16 ad2antrr 
 |-  ( ( ( F : A --> B /\ ran F = B ) /\ y e. B ) -> ( E. x x F y -> E. x e. A x F y ) )
18 8 17 mpd 
 |-  ( ( ( F : A --> B /\ ran F = B ) /\ y e. B ) -> E. x e. A x F y )
19 18 ralrimiva 
 |-  ( ( F : A --> B /\ ran F = B ) -> A. y e. B E. x e. A x F y )
20 2 19 jca 
 |-  ( ( F : A --> B /\ ran F = B ) -> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
21 1 20 sylbi 
 |-  ( F : A -onto-> B -> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
22 fnbrfvb 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
23 22 biimprd 
 |-  ( ( F Fn A /\ x e. A ) -> ( x F y -> ( F ` x ) = y ) )
24 eqcom 
 |-  ( ( F ` x ) = y <-> y = ( F ` x ) )
25 23 24 syl6ib 
 |-  ( ( F Fn A /\ x e. A ) -> ( x F y -> y = ( F ` x ) ) )
26 9 25 sylan 
 |-  ( ( F : A --> B /\ x e. A ) -> ( x F y -> y = ( F ` x ) ) )
27 26 reximdva 
 |-  ( F : A --> B -> ( E. x e. A x F y -> E. x e. A y = ( F ` x ) ) )
28 27 ralimdv 
 |-  ( F : A --> B -> ( A. y e. B E. x e. A x F y -> A. y e. B E. x e. A y = ( F ` x ) ) )
29 28 imdistani 
 |-  ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) -> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
30 dffo3 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
31 29 30 sylibr 
 |-  ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) -> F : A -onto-> B )
32 21 31 impbii 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )