Metamath Proof Explorer

Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

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

Proof

Step Hyp Ref Expression
1 dffo2 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )
2 ffn 
 |-  ( F : A --> B -> F Fn A )
3 fnrnfv 
 |-  ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
4 3 eqeq1d 
 |-  ( F Fn A -> ( ran F = B <-> { y | E. x e. A y = ( F ` x ) } = B ) )
5 2 4 syl 
 |-  ( F : A --> B -> ( ran F = B <-> { y | E. x e. A y = ( F ` x ) } = B ) )
6 dfbi2 
 |-  ( ( E. x e. A y = ( F ` x ) <-> y e. B ) <-> ( ( E. x e. A y = ( F ` x ) -> y e. B ) /\ ( y e. B -> E. x e. A y = ( F ` x ) ) ) )
7 simpr 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = ( F ` x ) )
8 ffvelrn 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
9 8 adantr 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> ( F ` x ) e. B )
10 7 9 eqeltrd 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> y e. B )
11 10 rexlimdva2 
 |-  ( F : A --> B -> ( E. x e. A y = ( F ` x ) -> y e. B ) )
12 11 biantrurd 
 |-  ( F : A --> B -> ( ( y e. B -> E. x e. A y = ( F ` x ) ) <-> ( ( E. x e. A y = ( F ` x ) -> y e. B ) /\ ( y e. B -> E. x e. A y = ( F ` x ) ) ) ) )
13 6 12 bitr4id 
 |-  ( F : A --> B -> ( ( E. x e. A y = ( F ` x ) <-> y e. B ) <-> ( y e. B -> E. x e. A y = ( F ` x ) ) ) )
14 13 albidv 
 |-  ( F : A --> B -> ( A. y ( E. x e. A y = ( F ` x ) <-> y e. B ) <-> A. y ( y e. B -> E. x e. A y = ( F ` x ) ) ) )
15 abeq1 
 |-  ( { y | E. x e. A y = ( F ` x ) } = B <-> A. y ( E. x e. A y = ( F ` x ) <-> y e. B ) )
16 df-ral 
 |-  ( A. y e. B E. x e. A y = ( F ` x ) <-> A. y ( y e. B -> E. x e. A y = ( F ` x ) ) )
17 14 15 16 3bitr4g 
 |-  ( F : A --> B -> ( { y | E. x e. A y = ( F ` x ) } = B <-> A. y e. B E. x e. A y = ( F ` x ) ) )
18 5 17 bitrd 
 |-  ( F : A --> B -> ( ran F = B <-> A. y e. B E. x e. A y = ( F ` x ) ) )
19 18 pm5.32i 
 |-  ( ( F : A --> B /\ ran F = B ) <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
20 1 19 bitri 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )