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 syl5eq
 |-  ( F Fn X -> ( `' F " ran F ) = X )
9 5 8 eqtr3id
 |-  ( F Fn X -> ( `' F " dom `' F ) = X )
10 3 9 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 )