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

Metamath Proof Explorer

Theorem dffo5

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

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

Proof

Step Hyp Ref Expression
1 dffo4 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
2 rexex 
 |-  ( E. x e. A x F y -> E. x x F y )
3 2 ralimi 
 |-  ( A. y e. B E. x e. A x F y -> A. y e. B E. x x F y )
4 3 anim2i 
 |-  ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) -> ( F : A --> B /\ A. y e. B E. x x F y ) )
5 ffn 
 |-  ( F : A --> B -> F Fn A )
6 fnbr 
 |-  ( ( F Fn A /\ x F y ) -> x e. A )
7 6 ex 
 |-  ( F Fn A -> ( x F y -> x e. A ) )
8 5 7 syl 
 |-  ( F : A --> B -> ( x F y -> x e. A ) )
9 8 ancrd 
 |-  ( F : A --> B -> ( x F y -> ( x e. A /\ x F y ) ) )
10 9 eximdv 
 |-  ( F : A --> B -> ( E. x x F y -> E. x ( x e. A /\ x F y ) ) )
11 df-rex 
 |-  ( E. x e. A x F y <-> E. x ( x e. A /\ x F y ) )
12 10 11 imbitrrdi 
 |-  ( F : A --> B -> ( E. x x F y -> E. x e. A x F y ) )
13 12 ralimdv 
 |-  ( F : A --> B -> ( A. y e. B E. x x F y -> A. y e. B E. x e. A x F y ) )
14 13 imdistani 
 |-  ( ( F : A --> B /\ A. y e. B E. x x F y ) -> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
15 4 14 impbii 
 |-  ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) <-> ( F : A --> B /\ A. y e. B E. x x F y ) )
16 1 15 bitri 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x x F y ) )