Theorem 2fvidf1od

Description: A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019)

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

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	fcof1od	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )