Metamath Proof Explorer

Theorem f1oco

Description: Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998)

Ref Expression
Assertion f1oco ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1-onto→ 𝐶 )

Proof

Step Hyp Ref Expression
1 df-f1o ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) )
2 df-f1o ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐺 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) )
3 f1co ⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 )
4 foco ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 )
5 3 4 anim12i ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) ∧ ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) )
6 5 an4s ⊢ ( ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝐺 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) )
7 1 2 6 syl2anb ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) )
8 df-f1o ⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1-onto→ 𝐶 ↔ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) )
9 7 8 sylibr ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1-onto→ 𝐶 )