Metamath Proof Explorer

Theorem dffo3f

Description: An onto mapping expressed in terms of function values. As dffo3 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 dffo3f.1 
 |-  F/_ x F
2 dffo2 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )
3 ffn 
 |-  ( F : A --> B -> F Fn A )
4 fnrnfv 
 |-  ( F Fn A -> ran F = { y | E. w e. A y = ( F ` w ) } )
5 nfcv 
 |-  F/_ x w
6 1 5 nffv 
 |-  F/_ x ( F ` w )
7 6 nfeq2 
 |-  F/ x y = ( F ` w )
8 nfv 
 |-  F/ w y = ( F ` x )
9 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
10 9 eqeq2d 
 |-  ( w = x -> ( y = ( F ` w ) <-> y = ( F ` x ) ) )
11 7 8 10 cbvrexw 
 |-  ( E. w e. A y = ( F ` w ) <-> E. x e. A y = ( F ` x ) )
12 11 abbii 
 |-  { y | E. w e. A y = ( F ` w ) } = { y | E. x e. A y = ( F ` x ) }
13 4 12 eqtrdi 
 |-  ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
14 13 eqeq1d 
 |-  ( F Fn A -> ( ran F = B <-> { y | E. x e. A y = ( F ` x ) } = B ) )
15 3 14 syl 
 |-  ( F : A --> B -> ( ran F = B <-> { y | E. x e. A y = ( F ` x ) } = B ) )
16 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 ) ) ) )
17 nfcv 
 |-  F/_ x A
18 nfcv 
 |-  F/_ x B
19 1 17 18 nff 
 |-  F/ x F : A --> B
20 nfv 
 |-  F/ x y e. B
21 simpr 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = ( F ` x ) )
22 ffvelcdm 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
23 22 adantr 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> ( F ` x ) e. B )
24 21 23 eqeltrd 
 |-  ( ( ( F : A --> B /\ x e. A ) /\ y = ( F ` x ) ) -> y e. B )
25 24 exp31 
 |-  ( F : A --> B -> ( x e. A -> ( y = ( F ` x ) -> y e. B ) ) )
26 19 20 25 rexlimd 
 |-  ( F : A --> B -> ( E. x e. A y = ( F ` x ) -> y e. B ) )
27 26 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 ) ) ) ) )
28 16 27 bitr4id 
 |-  ( F : A --> B -> ( ( E. x e. A y = ( F ` x ) <-> y e. B ) <-> ( y e. B -> E. x e. A y = ( F ` x ) ) ) )
29 28 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 ) ) ) )
30 eqabcb 
 |-  ( { y | E. x e. A y = ( F ` x ) } = B <-> A. y ( E. x e. A y = ( F ` x ) <-> y e. B ) )
31 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 ) ) )
32 29 30 31 3bitr4g 
 |-  ( F : A --> B -> ( { y | E. x e. A y = ( F ` x ) } = B <-> A. y e. B E. x e. A y = ( F ` x ) ) )
33 15 32 bitrd 
 |-  ( F : A --> B -> ( ran F = B <-> A. y e. B E. x e. A y = ( F ` x ) ) )
34 33 pm5.32i 
 |-  ( ( F : A --> B /\ ran F = B ) <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
35 2 34 bitri 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )