This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions 2fcoidinvd
Description: Show that a function is the inverse of a function if their compositions
are the identity functions. (Contributed by Mario Carneiro , 21-Mar-2015) (Revised by AV , 15-Dec-2019)
Ref
Expression
Hypotheses
fcof1od.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fcof1od.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
fcof1od.a ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
fcof1od.b ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
Assertion
2fcoidinvd ⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )
Proof
Step
Hyp
Ref
Expression
1
fcof1od.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2
fcof1od.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3
fcof1od.a ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
4
fcof1od.b ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
5
1 2 3 4
fcof1od ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1 -onto → 𝐵 )
6
5 2 4
fcof1oinvd ⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )