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 birani 
 |-  ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A --> B )
25 nfv 
 |-  F/ y A. x e. A C e. B
26 nfra1 
 |-  F/ y A. y e. B E. x e. A y = C
27 25 26 nfan 
 |-  F/ y ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C )
28 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 )
29 rspa 
 |-  ( ( A. y e. B E. x e. A y = C /\ y e. B ) -> E. x e. A y = C )
30 29 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 )
31 nfra1 
 |-  F/ x A. x e. A C e. B
32 simp3 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = C )
33 simpr 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> x e. A )
34 rspa 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> C e. B )
35 33 34 14 syl2anc 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> ( F ` x ) = C )
36 35 eqcomd 
 |-  ( ( A. x e. A C e. B /\ x e. A ) -> C = ( F ` x ) )
37 36 3adant3 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> C = ( F ` x ) )
38 32 37 eqtrd 
 |-  ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = ( F ` x ) )
39 38 3exp 
 |-  ( A. x e. A C e. B -> ( x e. A -> ( y = C -> y = ( F ` x ) ) ) )
40 31 39 reximdai 
 |-  ( A. x e. A C e. B -> ( E. x e. A y = C -> E. x e. A y = ( F ` x ) ) )
41 28 30 40 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 ) )
42 27 41 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 ) )
43 6 dffo3f 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
44 24 42 43 sylanbrc 
 |-  ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A -onto-> B )
45 23 44 impbii 
 |-  ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )