This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝐹 Fn 𝑋 → ( ◡ 𝐹 “ ran 𝐹 ) = 𝑋 )
9 5 8 eqtr3id ⊢ ( 𝐹 Fn 𝑋 → ( ◡ 𝐹 “ dom ◡ 𝐹 ) = 𝑋 )
10 3 9 eqtrid ⊢ ( 𝐹 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 eqtrid ⊢ ( 𝐹 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 𝑋 )