Metamath Proof Explorer

Theorem f1eqcocnv

Description: Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015) (Proof shortened by Wolf Lammen, 29-May-2024)

Ref Expression
Assertion f1eqcocnv ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 f1cocnv1 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
2 coeq2 ⊢ ( 𝐹 = 𝐺 → ( ◡ 𝐹 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐺 ) )
3 2 eqeq1d ⊢ ( 𝐹 = 𝐺 → ( ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )
4 1 3 syl5ibcom ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 = 𝐺 → ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )
5 4 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 = 𝐺 → ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )
6 f1fn ⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 → 𝐺 Fn 𝐴 )
7 6 adantl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → 𝐺 Fn 𝐴 )
8 7 adantr ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐺 Fn 𝐴 )
9 f1fn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
10 9 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → 𝐹 Fn 𝐴 )
11 10 adantr ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐹 Fn 𝐴 )
12 equid ⊢ 𝑥 = 𝑥
13 resieq ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( I ↾ 𝐴 ) 𝑥 ↔ 𝑥 = 𝑥 ) )
14 12 13 mpbiri ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ( I ↾ 𝐴 ) 𝑥 )
15 14 anidms ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ( I ↾ 𝐴 ) 𝑥 )
16 15 adantl ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ( I ↾ 𝐴 ) 𝑥 )
17 breq ⊢ ( ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 ↔ 𝑥 ( I ↾ 𝐴 ) 𝑥 ) )
18 17 ad2antlr ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 ↔ 𝑥 ( I ↾ 𝐴 ) 𝑥 ) )
19 16 18 mpbird ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 )
20 fnfun ⊢ ( 𝐺 Fn 𝐴 → Fun 𝐺 )
21 7 20 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → Fun 𝐺 )
22 7 fndmd ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → dom 𝐺 = 𝐴 )
23 22 eleq2d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝐴 ) )
24 23 biimpar ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐺 )
25 funopfvb ⊢ ( ( Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
26 21 24 25 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
27 26 bicomd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝐺 ‘ 𝑥 ) = 𝑦 ) )
28 df-br ⊢ ( 𝑥 𝐺 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 )
29 eqcom ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = 𝑦 )
30 27 28 29 3bitr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐺 𝑦 ↔ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
31 30 biimpd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐺 𝑦 → 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
32 df-br ⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
33 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
34 10 33 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → Fun 𝐹 )
35 10 fndmd ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 = 𝐴 )
36 35 eleq2d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
37 36 biimpar ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 )
38 funopfvb ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
39 34 37 38 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
40 32 39 bitr4id ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐹 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
41 vex ⊢ 𝑦 ∈ V
42 vex ⊢ 𝑥 ∈ V
43 41 42 brcnv ⊢ ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝑦 )
44 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
45 40 43 44 3bitr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
46 45 biimpd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ◡ 𝐹 𝑥 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
47 31 46 anim12d ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
48 47 eximdv ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) → ∃ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
49 42 42 brco ⊢ ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 ↔ ∃ 𝑦 ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) )
50 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
51 50 eqvinc ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
52 48 49 51 3imtr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
53 52 adantlr ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
54 19 53 mpd ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
55 8 11 54 eqfnfvd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐺 = 𝐹 )
56 55 eqcomd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐹 = 𝐺 )
57 56 ex ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) → 𝐹 = 𝐺 ) )
58 5 57 impbid ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )