Theorem fcof1od

Description: A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 and fcofo . Formerly part of proof of fcof1o . (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	fcof1od	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fcof1od.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcof1od.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3		fcof1od.a	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
4		fcof1od.b	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
5		fcof1	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
6	1 3 5	syl2anc	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
7		fcofo	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐴 –onto→ 𝐵 )
8	1 2 4 7	syl3anc	⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )
9		df-f1o	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
10	6 8 9	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )