Metamath Proof Explorer

Theorem fompt

Description: Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 fompt.1 
 |-  F = ( x e. A |-> C )
2 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
3 1 fmpt 
 |-  ( A. x e. A C e. B <-> F : A --> B )
4 2 3 sylibr 
 |-  ( F : A -onto-> B -> A. x e. A C e. B )
5 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
6 1 5 nfcxfr 
 |-  F/_ x F
7 6 foelrnf 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A y = ( F ` x ) )
8 nfcv 
 |-  F/_ x A
9 nfcv 
 |-  F/_ x B
10 6 8 9 nffo 
 |-  F/ x F : A -onto-> B
11 simpr 
 |-  ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = ( F ` x ) )
12 simpr 
 |-  ( ( F : A -onto-> B /\ x e. A ) -> x e. A )
13 4 r19.21bi 
 |-  ( ( F : A -onto-> B /\ x e. A ) -> C e. B )
14 1 fvmpt2 
 |-  ( ( x e. A /\ C e. B ) -> ( F ` x ) = C )
15 12 13 14 syl2anc 
 |-  ( ( F : A -onto-> B /\ x e. A ) -> ( F ` x ) = C )
16 15 adantr 
 |-  ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> ( F ` x ) = C )
17 11 16 eqtrd 
 |-  ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = C )
18 17 exp31 
 |-  ( F : A -onto-> B -> ( x e. A -> ( y = ( F ` x ) -> y = C ) ) )
19 10 18 reximdai 
 |-  ( F : A -onto-> B -> ( E. x e. A y = ( F ` x ) -> E. x e. A y = C ) )
20 19 adantr 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> ( E. x e. A y = ( F ` x ) -> E. x e. A y = C ) )
21 7 20 mpd 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A y = C )
22 21 ralrimiva 
 |-  ( F : A -onto-> B -> A. y e. B E. x e. A y = C )
23 4 22 jca 
 |-  ( F : A -onto-> B -> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )
24 3 biimpi 
 |-  ( A. x e. A C e. B -> F : A --> B )
25 24 adantr 
 |-  ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A --> B )
26 nfv 
 |-  F/ y A. x e. A C e. B
27 nfra1 
 |-  F/ y A. y e. B E. x e. A y = C
28 26 27 nfan 
 |-  F/ y ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C )
29 simpll 
 |-  ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> A. x e. A C e. B )
30 rspa 
 |-  ( ( A. y e. B E. x e. A y = C /\ y e. B ) -> E. x e. A y = C )
31 30 adantll 
 |-  ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> E. x e. A y = C )
32 nfra1 
 |-  F/ x A. x e. A C e. B
33 simp3 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = C )
34 simpr 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> x e. A )
35 rspa 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> C e. B )
36 34 35 14 syl2anc 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> ( F ` x ) = C )
37 36 eqcomd 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> C = ( F ` x ) )
38 37 3adant3 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> C = ( F ` x ) )
39 33 38 eqtrd 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = ( F ` x ) )
40 39 3exp 
 |-  ( A. x e. A C e. B -> ( x e. A -> ( y = C -> y = ( F ` x ) ) ) )
41 32 40 reximdai 
 |-  ( A. x e. A C e. B -> ( E. x e. A y = C -> E. x e. A y = ( F ` x ) ) )
42 29 31 41 sylc 
 |-  ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> E. x e. A y = ( F ` x ) )
43 28 42 ralrimia 
 |-  ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> A. y e. B E. x e. A y = ( F ` x ) )
44 6 dffo3f 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
45 25 43 44 sylanbrc 
 |-  ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A -onto-> B )
46 23 45 impbii 
 |-  ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )