Metamath Proof Explorer


Theorem 2fvcoidd

Description: Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019)

Ref Expression
Hypotheses 2fvcoidd.f ( 𝜑𝐹 : 𝐴𝐵 )
2fvcoidd.g ( 𝜑𝐺 : 𝐵𝐴 )
2fvcoidd.i ( 𝜑 → ∀ 𝑎𝐴 ( 𝐺 ‘ ( 𝐹𝑎 ) ) = 𝑎 )
Assertion 2fvcoidd ( 𝜑 → ( 𝐺𝐹 ) = ( I ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 2fvcoidd.f ( 𝜑𝐹 : 𝐴𝐵 )
2 2fvcoidd.g ( 𝜑𝐺 : 𝐵𝐴 )
3 2fvcoidd.i ( 𝜑 → ∀ 𝑎𝐴 ( 𝐺 ‘ ( 𝐹𝑎 ) ) = 𝑎 )
4 fcompt ( ( 𝐺 : 𝐵𝐴𝐹 : 𝐴𝐵 ) → ( 𝐺𝐹 ) = ( 𝑥𝐴 ↦ ( 𝐺 ‘ ( 𝐹𝑥 ) ) ) )
5 2 1 4 syl2anc ( 𝜑 → ( 𝐺𝐹 ) = ( 𝑥𝐴 ↦ ( 𝐺 ‘ ( 𝐹𝑥 ) ) ) )
6 2fveq3 ( 𝑎 = 𝑥 → ( 𝐺 ‘ ( 𝐹𝑎 ) ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
7 id ( 𝑎 = 𝑥𝑎 = 𝑥 )
8 6 7 eqeq12d ( 𝑎 = 𝑥 → ( ( 𝐺 ‘ ( 𝐹𝑎 ) ) = 𝑎 ↔ ( 𝐺 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
9 8 rspccv ( ∀ 𝑎𝐴 ( 𝐺 ‘ ( 𝐹𝑎 ) ) = 𝑎 → ( 𝑥𝐴 → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
10 3 9 syl ( 𝜑 → ( 𝑥𝐴 → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
11 10 imp ( ( 𝜑𝑥𝐴 ) → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
12 11 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐺 ‘ ( 𝐹𝑥 ) ) ) = ( 𝑥𝐴𝑥 ) )
13 mptresid ( I ↾ 𝐴 ) = ( 𝑥𝐴𝑥 )
14 12 13 eqtr4di ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐺 ‘ ( 𝐹𝑥 ) ) ) = ( I ↾ 𝐴 ) )
15 5 14 eqtrd ( 𝜑 → ( 𝐺𝐹 ) = ( I ↾ 𝐴 ) )