Metamath Proof Explorer

Theorem foeqcnvco

Description: Condition for function equality in terms of vanishing of the composition with the converse.EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015)

Ref Expression
Assertion foeqcnvco ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fococnv2 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐵 ) )
2 cnveq ⊢ ( 𝐹 = 𝐺 → ◡ 𝐹 = ◡ 𝐺 )
3 2 coeq2d ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ∘ ◡ 𝐹 ) = ( 𝐹 ∘ ◡ 𝐺 ) )
4 3 eqeq1d ⊢ ( 𝐹 = 𝐺 → ( ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐵 ) ↔ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )
5 1 4 syl5ibcom ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 = 𝐺 → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )
6 5 adantr ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 = 𝐺 → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )
7 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
8 7 ad2antrr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 Fn 𝐴 )
9 fofn ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐺 Fn 𝐴 )
10 9 ad2antlr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐺 Fn 𝐴 )
11 9 adantl ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐺 Fn 𝐴 )
12 fnopfv ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ 𝐺 )
13 11 12 sylan ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ 𝐺 )
14 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
15 vex ⊢ 𝑥 ∈ V
16 14 15 brcnv ⊢ ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 ↔ 𝑥 𝐺 ( 𝐺 ‘ 𝑥 ) )
17 df-br ⊢ ( 𝑥 𝐺 ( 𝐺 ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ 𝐺 )
18 16 17 bitri ⊢ ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 ↔ ⟨ 𝑥 , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ 𝐺 )
19 13 18 sylibr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 )
20 7 adantr ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐹 Fn 𝐴 )
21 fnopfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
22 20 21 sylan ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
23 df-br ⊢ ( 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
24 22 23 sylibr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) )
25 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑦 ↔ ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 ) )
26 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝐹 ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
27 25 26 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑦 ∧ 𝑦 𝐹 ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 ∧ 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ) ) )
28 15 27 spcev ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑥 ∧ 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑦 ∧ 𝑦 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
29 19 24 28 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑦 ∧ 𝑦 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
30 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
31 14 30 brco ⊢ ( ( 𝐺 ‘ 𝑥 ) ( 𝐹 ∘ ◡ 𝐺 ) ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑦 ( ( 𝐺 ‘ 𝑥 ) ◡ 𝐺 𝑦 ∧ 𝑦 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
32 29 31 sylibr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ( 𝐹 ∘ ◡ 𝐺 ) ( 𝐹 ‘ 𝑥 ) )
33 32 adantlr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ( 𝐹 ∘ ◡ 𝐺 ) ( 𝐹 ‘ 𝑥 ) )
34 breq ⊢ ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) → ( ( 𝐺 ‘ 𝑥 ) ( 𝐹 ∘ ◡ 𝐺 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) ) )
35 34 ad2antlr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ( 𝐹 ∘ ◡ 𝐺 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) ) )
36 33 35 mpbid ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) )
37 fof ⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 → 𝐺 : 𝐴 ⟶ 𝐵 )
38 37 adantl ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
39 38 ffvelcdmda ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 )
40 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
41 40 adantr ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
42 41 ffvelcdmda ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
43 resieq ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
44 39 42 43 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
45 44 adantlr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ( I ↾ 𝐵 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
46 36 45 mpbid ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
47 46 eqcomd ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
48 8 10 47 eqfnfvd ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 = 𝐺 )
49 48 ex ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) → 𝐹 = 𝐺 ) )
50 6 49 impbid ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )