Theorem 2fvidinvd

Description: Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019)

	Ref	Expression
Hypotheses	2fvcoidd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	2fvcoidd.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
	2fvcoidd.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 )
	2fvidf1od.i	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) = 𝑏 )
Assertion	2fvidinvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		2fvcoidd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		2fvcoidd.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3		2fvcoidd.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 )
4		2fvidf1od.i	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑏 ) ) = 𝑏 )
5	1 2 3	2fvcoidd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
6	2 1 4	2fvcoidd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
7	1 2 5 6	2fcoidinvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )