Metamath Proof Explorer


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 ( 𝜑 𝐹 = 𝐺 )