Metamath Proof Explorer

Theorem f1eqcocnvOLD

Description: Obsolete version of f1eqcocnv as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion f1eqcocnvOLD 
|- ( ( 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 fndm 
 |-  ( G Fn A -> dom G = A )
23 7 22 syl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> dom G = A )
24 23 eleq2d 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( x e. dom G <-> x e. A ) )
25 24 biimpar 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> x e. dom G )
26 funopfvb 
 |-  ( ( Fun G /\ x e. dom G ) -> ( ( G ` x ) = y <-> <. x , y >. e. G ) )
27 21 25 26 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( ( G ` x ) = y <-> <. x , y >. e. G ) )
28 27 bicomd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( <. x , y >. e. G <-> ( G ` x ) = y ) )
29 df-br 
 |-  ( x G y <-> <. x , y >. e. G )
30 eqcom 
 |-  ( y = ( G ` x ) <-> ( G ` x ) = y )
31 28 29 30 3bitr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x G y <-> y = ( G ` x ) ) )
32 31 biimpd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x G y -> y = ( G ` x ) ) )
33 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
34 fnfun 
 |-  ( F Fn A -> Fun F )
35 10 34 syl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> Fun F )
36 fndm 
 |-  ( F Fn A -> dom F = A )
37 10 36 syl 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> dom F = A )
38 37 eleq2d 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( x e. dom F <-> x e. A ) )
39 38 biimpar 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> x e. dom F )
40 funopfvb 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
41 35 39 40 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
42 33 41 bitr4id 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x F y <-> ( F ` x ) = y ) )
43 vex 
 |-  y e. _V
44 vex 
 |-  x e. _V
45 43 44 brcnv 
 |-  ( y `' F x <-> x F y )
46 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
47 42 45 46 3bitr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( y `' F x <-> y = ( F ` x ) ) )
48 47 biimpd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( y `' F x -> y = ( F ` x ) ) )
49 32 48 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 ) ) ) )
50 49 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 ) ) ) )
51 44 44 brco 
 |-  ( x ( `' F o. G ) x <-> E. y ( x G y /\ y `' F x ) )
52 fvex 
 |-  ( G ` x ) e. _V
53 52 eqvinc 
 |-  ( ( G ` x ) = ( F ` x ) <-> E. y ( y = ( G ` x ) /\ y = ( F ` x ) ) )
54 50 51 53 3imtr4g 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ x e. A ) -> ( x ( `' F o. G ) x -> ( G ` x ) = ( F ` x ) ) )
55 54 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 ) ) )
56 19 55 mpd 
 |-  ( ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) /\ x e. A ) -> ( G ` x ) = ( F ` x ) )
57 8 11 56 eqfnfvd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> G = F )
58 57 eqcomd 
 |-  ( ( ( F : A -1-1-> B /\ G : A -1-1-> B ) /\ ( `' F o. G ) = ( _I |` A ) ) -> F = G )
59 58 ex 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( ( `' F o. G ) = ( _I |` A ) -> F = G ) )
60 5 59 impbid 
 |-  ( ( F : A -1-1-> B /\ G : A -1-1-> B ) -> ( F = G <-> ( `' F o. G ) = ( _I |` A ) ) )