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	syl6eqr	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( I ↾ 𝐴 ) )
15	5 14	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )