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)

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 fndm ⊢ ( 𝐺 Fn 𝐴 → dom 𝐺 = 𝐴 )
23 7 22 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → dom 𝐺 = 𝐴 )
24 23 eleq2d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝐴 ) )
25 24 biimpar ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐺 )
26 funopfvb ⊢ ( ( Fun 𝐺 ∧ 𝑥 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
27 21 25 26 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
28 27 bicomd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝐺 ‘ 𝑥 ) = 𝑦 ) )
29 df-br ⊢ ( 𝑥 𝐺 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 )
30 eqcom ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = 𝑦 )
31 28 29 30 3bitr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐺 𝑦 ↔ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
32 31 biimpd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐺 𝑦 → 𝑦 = ( 𝐺 ‘ 𝑥 ) ) )
33 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
34 10 33 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → Fun 𝐹 )
35 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
36 10 35 syl ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 = 𝐴 )
37 36 eleq2d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
38 37 biimpar ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 )
39 funopfvb ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
40 34 38 39 syl2an2r ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
41 df-br ⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
42 40 41 syl6rbbr ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐹 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
43 vex ⊢ 𝑦 ∈ V
44 vex ⊢ 𝑥 ∈ V
45 43 44 brcnv ⊢ ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝑦 )
46 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
47 42 45 46 3bitr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
48 47 biimpd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ◡ 𝐹 𝑥 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
49 32 48 anim12d ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
50 49 eximdv ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) → ∃ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
51 44 44 brco ⊢ ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 ↔ ∃ 𝑦 ( 𝑥 𝐺 𝑦 ∧ 𝑦 ◡ 𝐹 𝑥 ) )
52 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
53 52 eqvinc ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
54 50 51 53 3imtr4g ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
55 54 adantlr ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ◡ 𝐹 ∘ 𝐺 ) 𝑥 → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
56 19 55 mpd ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
57 8 11 56 eqfnfvd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐺 = 𝐹 )
58 57 eqcomd ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐹 = 𝐺 )
59 58 ex ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) → 𝐹 = 𝐺 ) )
60 5 59 impbid ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( ◡ 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐴 ) ) )