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 ( 𝐹 Fn 𝑋 → ( 𝐹𝐹 ) Er 𝑋 )

Proof

Step Hyp Ref Expression
1 relco Rel ( 𝐹𝐹 )
2 1 a1i ( 𝐹 Fn 𝑋 → Rel ( 𝐹𝐹 ) )
3 dmco dom ( 𝐹𝐹 ) = ( 𝐹 “ dom 𝐹 )
4 df-rn ran 𝐹 = dom 𝐹
5 4 imaeq2i ( 𝐹 “ ran 𝐹 ) = ( 𝐹 “ dom 𝐹 )
6 cnvimarndm ( 𝐹 “ ran 𝐹 ) = dom 𝐹
7 fndm ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
8 6 7 syl5eq ( 𝐹 Fn 𝑋 → ( 𝐹 “ ran 𝐹 ) = 𝑋 )
9 5 8 eqtr3id ( 𝐹 Fn 𝑋 → ( 𝐹 “ dom 𝐹 ) = 𝑋 )
10 3 9 syl5eq ( 𝐹 Fn 𝑋 → dom ( 𝐹𝐹 ) = 𝑋 )
11 cnvco ( 𝐹𝐹 ) = ( 𝐹 𝐹 )
12 cnvcnvss 𝐹𝐹
13 coss2 ( 𝐹𝐹 → ( 𝐹 𝐹 ) ⊆ ( 𝐹𝐹 ) )
14 12 13 ax-mp ( 𝐹 𝐹 ) ⊆ ( 𝐹𝐹 )
15 11 14 eqsstri ( 𝐹𝐹 ) ⊆ ( 𝐹𝐹 )
16 15 a1i ( 𝐹 Fn 𝑋 ( 𝐹𝐹 ) ⊆ ( 𝐹𝐹 ) )
17 coass ( ( 𝐹𝐹 ) ∘ ( 𝐹𝐹 ) ) = ( 𝐹 ∘ ( 𝐹 ∘ ( 𝐹𝐹 ) ) )
18 coass ( ( 𝐹 𝐹 ) ∘ 𝐹 ) = ( 𝐹 ∘ ( 𝐹𝐹 ) )
19 fnfun ( 𝐹 Fn 𝑋 → Fun 𝐹 )
20 funcocnv2 ( Fun 𝐹 → ( 𝐹 𝐹 ) = ( I ↾ ran 𝐹 ) )
21 19 20 syl ( 𝐹 Fn 𝑋 → ( 𝐹 𝐹 ) = ( I ↾ ran 𝐹 ) )
22 21 coeq1d ( 𝐹 Fn 𝑋 → ( ( 𝐹 𝐹 ) ∘ 𝐹 ) = ( ( I ↾ ran 𝐹 ) ∘ 𝐹 ) )
23 dffn3 ( 𝐹 Fn 𝑋𝐹 : 𝑋 ⟶ ran 𝐹 )
24 fcoi2 ( 𝐹 : 𝑋 ⟶ ran 𝐹 → ( ( I ↾ ran 𝐹 ) ∘ 𝐹 ) = 𝐹 )
25 23 24 sylbi ( 𝐹 Fn 𝑋 → ( ( I ↾ ran 𝐹 ) ∘ 𝐹 ) = 𝐹 )
26 22 25 eqtrd ( 𝐹 Fn 𝑋 → ( ( 𝐹 𝐹 ) ∘ 𝐹 ) = 𝐹 )
27 18 26 eqtr3id ( 𝐹 Fn 𝑋 → ( 𝐹 ∘ ( 𝐹𝐹 ) ) = 𝐹 )
28 27 coeq2d ( 𝐹 Fn 𝑋 → ( 𝐹 ∘ ( 𝐹 ∘ ( 𝐹𝐹 ) ) ) = ( 𝐹𝐹 ) )
29 17 28 syl5eq ( 𝐹 Fn 𝑋 → ( ( 𝐹𝐹 ) ∘ ( 𝐹𝐹 ) ) = ( 𝐹𝐹 ) )
30 ssid ( 𝐹𝐹 ) ⊆ ( 𝐹𝐹 )
31 29 30 eqsstrdi ( 𝐹 Fn 𝑋 → ( ( 𝐹𝐹 ) ∘ ( 𝐹𝐹 ) ) ⊆ ( 𝐹𝐹 ) )
32 16 31 unssd ( 𝐹 Fn 𝑋 → ( ( 𝐹𝐹 ) ∪ ( ( 𝐹𝐹 ) ∘ ( 𝐹𝐹 ) ) ) ⊆ ( 𝐹𝐹 ) )
33 df-er ( ( 𝐹𝐹 ) Er 𝑋 ↔ ( Rel ( 𝐹𝐹 ) ∧ dom ( 𝐹𝐹 ) = 𝑋 ∧ ( ( 𝐹𝐹 ) ∪ ( ( 𝐹𝐹 ) ∘ ( 𝐹𝐹 ) ) ) ⊆ ( 𝐹𝐹 ) ) )
34 2 10 32 33 syl3anbrc ( 𝐹 Fn 𝑋 → ( 𝐹𝐹 ) Er 𝑋 )