Metamath Proof Explorer

Theorem fcoinver

Description: Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr . (Contributed by Thierry Arnoux, 3-Jan-2020)

Ref Expression
Assertion fcoinver 
|- ( F Fn X -> ( `' F o. F ) Er X )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( `' F o. F )
2 1 a1i 
 |-  ( F Fn X -> Rel ( `' F o. F ) )
3 dmco 
 |-  dom ( `' F o. F ) = ( `' F " dom `' F )
4 df-rn 
 |-  ran F = dom `' F
5 4 imaeq2i 
 |-  ( `' F " ran F ) = ( `' F " dom `' F )
6 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
7 fndm 
 |-  ( F Fn X -> dom F = X )
8 6 7 eqtrid 
 |-  ( F Fn X -> ( `' F " ran F ) = X )
9 5 8 eqtr3id 
 |-  ( F Fn X -> ( `' F " dom `' F ) = X )
10 3 9 eqtrid 
 |-  ( F Fn X -> dom ( `' F o. F ) = X )
11 cnvco 
 |-  `' ( `' F o. F ) = ( `' F o. `' `' F )
12 cnvcnvss 
 |-  `' `' F C_ F
13 coss2 
 |-  ( `' `' F C_ F -> ( `' F o. `' `' F ) C_ ( `' F o. F ) )
14 12 13 ax-mp 
 |-  ( `' F o. `' `' F ) C_ ( `' F o. F )
15 11 14 eqsstri 
 |-  `' ( `' F o. F ) C_ ( `' F o. F )
16 15 a1i 
 |-  ( F Fn X -> `' ( `' F o. F ) C_ ( `' F o. F ) )
17 coass 
 |-  ( ( `' F o. F ) o. ( `' F o. F ) ) = ( `' F o. ( F o. ( `' F o. F ) ) )
18 coass 
 |-  ( ( F o. `' F ) o. F ) = ( F o. ( `' F o. F ) )
19 fnfun 
 |-  ( F Fn X -> Fun F )
20 funcocnv2 
 |-  ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )
21 19 20 syl 
 |-  ( F Fn X -> ( F o. `' F ) = ( _I |` ran F ) )
22 21 coeq1d 
 |-  ( F Fn X -> ( ( F o. `' F ) o. F ) = ( ( _I |` ran F ) o. F ) )
23 dffn3 
 |-  ( F Fn X <-> F : X --> ran F )
24 fcoi2 
 |-  ( F : X --> ran F -> ( ( _I |` ran F ) o. F ) = F )
25 23 24 sylbi 
 |-  ( F Fn X -> ( ( _I |` ran F ) o. F ) = F )
26 22 25 eqtrd 
 |-  ( F Fn X -> ( ( F o. `' F ) o. F ) = F )
27 18 26 eqtr3id 
 |-  ( F Fn X -> ( F o. ( `' F o. F ) ) = F )
28 27 coeq2d 
 |-  ( F Fn X -> ( `' F o. ( F o. ( `' F o. F ) ) ) = ( `' F o. F ) )
29 17 28 eqtrid 
 |-  ( F Fn X -> ( ( `' F o. F ) o. ( `' F o. F ) ) = ( `' F o. F ) )
30 ssid 
 |-  ( `' F o. F ) C_ ( `' F o. F )
31 29 30 eqsstrdi 
 |-  ( F Fn X -> ( ( `' F o. F ) o. ( `' F o. F ) ) C_ ( `' F o. F ) )
32 16 31 unssd 
 |-  ( F Fn X -> ( `' ( `' F o. F ) u. ( ( `' F o. F ) o. ( `' F o. F ) ) ) C_ ( `' F o. F ) )
33 df-er 
 |-  ( ( `' F o. F ) Er X <-> ( Rel ( `' F o. F ) /\ dom ( `' F o. F ) = X /\ ( `' ( `' F o. F ) u. ( ( `' F o. F ) o. ( `' F o. F ) ) ) C_ ( `' F o. F ) ) )
34 2 10 32 33 syl3anbrc 
 |-  ( F Fn X -> ( `' F o. F ) Er X )