Metamath Proof Explorer

Theorem foeqcnvco

Description: Condition for function equality in terms of vanishing of the composition with the converse.EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 fococnv2 
 |-  ( F : A -onto-> B -> ( F o. `' F ) = ( _I |` B ) )
2 cnveq 
 |-  ( F = G -> `' F = `' G )
3 2 coeq2d 
 |-  ( F = G -> ( F o. `' F ) = ( F o. `' G ) )
4 3 eqeq1d 
 |-  ( F = G -> ( ( F o. `' F ) = ( _I |` B ) <-> ( F o. `' G ) = ( _I |` B ) ) )
5 1 4 syl5ibcom 
 |-  ( F : A -onto-> B -> ( F = G -> ( F o. `' G ) = ( _I |` B ) ) )
6 5 adantr 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> ( F = G -> ( F o. `' G ) = ( _I |` B ) ) )
7 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
8 7 ad2antrr 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) -> F Fn A )
9 fofn 
 |-  ( G : A -onto-> B -> G Fn A )
10 9 ad2antlr 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) -> G Fn A )
11 9 adantl 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> G Fn A )
12 fnopfv 
 |-  ( ( G Fn A /\ x e. A ) -> <. x , ( G ` x ) >. e. G )
13 11 12 sylan 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> <. x , ( G ` x ) >. e. G )
14 fvex 
 |-  ( G ` x ) e. _V
15 vex 
 |-  x e. _V
16 14 15 brcnv 
 |-  ( ( G ` x ) `' G x <-> x G ( G ` x ) )
17 df-br 
 |-  ( x G ( G ` x ) <-> <. x , ( G ` x ) >. e. G )
18 16 17 bitri 
 |-  ( ( G ` x ) `' G x <-> <. x , ( G ` x ) >. e. G )
19 13 18 sylibr 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> ( G ` x ) `' G x )
20 7 adantr 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> F Fn A )
21 fnopfv 
 |-  ( ( F Fn A /\ x e. A ) -> <. x , ( F ` x ) >. e. F )
22 20 21 sylan 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> <. x , ( F ` x ) >. e. F )
23 df-br 
 |-  ( x F ( F ` x ) <-> <. x , ( F ` x ) >. e. F )
24 22 23 sylibr 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> x F ( F ` x ) )
25 breq2 
 |-  ( y = x -> ( ( G ` x ) `' G y <-> ( G ` x ) `' G x ) )
26 breq1 
 |-  ( y = x -> ( y F ( F ` x ) <-> x F ( F ` x ) ) )
27 25 26 anbi12d 
 |-  ( y = x -> ( ( ( G ` x ) `' G y /\ y F ( F ` x ) ) <-> ( ( G ` x ) `' G x /\ x F ( F ` x ) ) ) )
28 15 27 spcev 
 |-  ( ( ( G ` x ) `' G x /\ x F ( F ` x ) ) -> E. y ( ( G ` x ) `' G y /\ y F ( F ` x ) ) )
29 19 24 28 syl2anc 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> E. y ( ( G ` x ) `' G y /\ y F ( F ` x ) ) )
30 fvex 
 |-  ( F ` x ) e. _V
31 14 30 brco 
 |-  ( ( G ` x ) ( F o. `' G ) ( F ` x ) <-> E. y ( ( G ` x ) `' G y /\ y F ( F ` x ) ) )
32 29 31 sylibr 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> ( G ` x ) ( F o. `' G ) ( F ` x ) )
33 32 adantlr 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( G ` x ) ( F o. `' G ) ( F ` x ) )
34 breq 
 |-  ( ( F o. `' G ) = ( _I |` B ) -> ( ( G ` x ) ( F o. `' G ) ( F ` x ) <-> ( G ` x ) ( _I |` B ) ( F ` x ) ) )
35 34 ad2antlr 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( ( G ` x ) ( F o. `' G ) ( F ` x ) <-> ( G ` x ) ( _I |` B ) ( F ` x ) ) )
36 33 35 mpbid 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( G ` x ) ( _I |` B ) ( F ` x ) )
37 fof 
 |-  ( G : A -onto-> B -> G : A --> B )
38 37 adantl 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> G : A --> B )
39 38 ffvelcdmda 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> ( G ` x ) e. B )
40 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
41 40 adantr 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> F : A --> B )
42 41 ffvelcdmda 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> ( F ` x ) e. B )
43 resieq 
 |-  ( ( ( G ` x ) e. B /\ ( F ` x ) e. B ) -> ( ( G ` x ) ( _I |` B ) ( F ` x ) <-> ( G ` x ) = ( F ` x ) ) )
44 39 42 43 syl2anc 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ x e. A ) -> ( ( G ` x ) ( _I |` B ) ( F ` x ) <-> ( G ` x ) = ( F ` x ) ) )
45 44 adantlr 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( ( G ` x ) ( _I |` B ) ( F ` x ) <-> ( G ` x ) = ( F ` x ) ) )
46 36 45 mpbid 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( G ` x ) = ( F ` x ) )
47 46 eqcomd 
 |-  ( ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
48 8 10 47 eqfnfvd 
 |-  ( ( ( F : A -onto-> B /\ G : A -onto-> B ) /\ ( F o. `' G ) = ( _I |` B ) ) -> F = G )
49 48 ex 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> ( ( F o. `' G ) = ( _I |` B ) -> F = G ) )
50 6 49 impbid 
 |-  ( ( F : A -onto-> B /\ G : A -onto-> B ) -> ( F = G <-> ( F o. `' G ) = ( _I |` B ) ) )