Metamath Proof Explorer

Theorem f1eqcocnv

Description: Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015) (Proof shortened by Wolf Lammen, 29-May-2024)

Ref Expression
Assertion f1eqcocnv 
|- ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( F = G <-> ( `' F o. G ) = ( _I |` A ) ) )

Proof

Step Hyp Ref Expression
1 f1cocnv1 
 |-  ( F : A -1-1-> B -> ( `' F o. F ) = ( _I |` A ) )
2 coeq2 
 |-  ( F = G -> ( `' F o. F ) = ( `' F o. G ) )
3 2 eqeq1d 
 |-  ( F = G -> ( ( `' F o. F ) = ( _I |` A ) <-> ( `' F o. G ) = ( _I |` A ) ) )
4 1 3 syl5ibcom 
 |-  ( F : A -1-1-> B -> ( F = G -> ( `' F o. G ) = ( _I |` A ) ) )
5 4 adantr 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( F = G -> ( `' F o. G ) = ( _I |` A ) ) )
6 f1fn 
 |-  ( G : A -1-1-> B -> G Fn A )
7 6 adantl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> G Fn A )
8 7 adantr 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> G Fn A )
9 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
10 9 adantr 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> F Fn A )
11 10 adantr 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> F Fn A )
12 equid 
 |-  x = x
13 resieq 
 |-  ( ( x e. A /\ x e. A ) -> ( x ( _I |` A ) x <-> x = x ) )
14 12 13 mpbiri 
 |-  ( ( x e. A /\ x e. A ) -> x ( _I |` A ) x )
15 14 anidms 
 |-  ( x e. A -> x ( _I |` A ) x )
16 15 adantl 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> x ( _I |` A ) x )
17 breq 
 |-  ( ( `' F o. G ) = ( _I |` A ) -> ( x ( `' F o. G ) x <-> x ( _I |` A ) x ) )
18 17 ad2antlr 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> ( x ( `' F o. G ) x <-> x ( _I |` A ) x ) )
19 16 18 mpbird 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> x ( `' F o. G ) x )
20 fnfun 
 |-  ( G Fn A -> Fun G )
21 7 20 syl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> Fun G )
22 7 fndmd 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> dom G = A )
23 22 eleq2d 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( x e. dom G <-> x e. A ) )
24 23 biimpar 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> x e. dom G )
25 funopfvb 
 |-  ( ( Fun G /\ x e. dom G ) -> ( ( G ` x ) = y <-> <. x , y >. e. G ) )
26 21 24 25 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( ( G ` x ) = y <-> <. x , y >. e. G ) )
27 26 bicomd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( <. x , y >. e. G <-> ( G ` x ) = y ) )
28 df-br 
 |-  ( x G y <-> <. x , y >. e. G )
29 eqcom 
 |-  ( y = ( G ` x ) <-> ( G ` x ) = y )
30 27 28 29 3bitr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x G y <-> y = ( G ` x ) ) )
31 30 biimpd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x G y -> y = ( G ` x ) ) )
32 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
33 fnfun 
 |-  ( F Fn A -> Fun F )
34 10 33 syl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> Fun F )
35 10 fndmd 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> dom F = A )
36 35 eleq2d 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( x e. dom F <-> x e. A ) )
37 36 biimpar 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> x e. dom F )
38 funopfvb 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
39 34 37 38 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
40 32 39 bitr4id 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x F y <-> ( F ` x ) = y ) )
41 vex 
 |-  y e. _V
42 vex 
 |-  x e. _V
43 41 42 brcnv 
 |-  ( y `' F x <-> x F y )
44 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
45 40 43 44 3bitr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( y `' F x <-> y = ( F ` x ) ) )
46 45 biimpd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( y `' F x -> y = ( F ` x ) ) )
47 31 46 anim12d 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( ( x G y /\ y `' F x ) -> ( y = ( G ` x ) /\ y = ( F ` x ) ) ) )
48 47 eximdv 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( E. y ( x G y /\ y `' F x ) -> E. y ( y = ( G ` x ) /\ y = ( F ` x ) ) ) )
49 42 42 brco 
 |-  ( x ( `' F o. G ) x <-> E. y ( x G y /\ y `' F x ) )
50 fvex 
 |-  ( G ` x ) e. _V
51 50 eqvinc 
 |-  ( ( G ` x ) = ( F ` x ) <-> E. y ( y = ( G ` x ) /\ y = ( F ` x ) ) )
52 48 49 51 3imtr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x ( `' F o. G ) x -> ( G ` x ) = ( F ` x ) ) )
53 52 adantlr 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> ( x ( `' F o. G ) x -> ( G ` x ) = ( F ` x ) ) )
54 19 53 mpd 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> ( G ` x ) = ( F ` x ) )
55 8 11 54 eqfnfvd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> G = F )
56 55 eqcomd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> F = G )
57 56 ex 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( ( `' F o. G ) = ( _I |` A ) -> F = G ) )
58 5 57 impbid 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( F = G <-> ( `' F o. G ) = ( _I |` A ) ) )