This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 )