Theorem f1co

Description: Composition of one-to-one functions. Exercise 30 of TakeutiZaring p. 25. (Contributed by NM, 28-May-1998)

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

Proof

Step	Hyp	Ref	Expression
1		df-f1	⊢ ( 𝐹 : 𝐵 –1-1→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ Fun ◡ 𝐹 ) )
2		df-f1	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐺 ) )
3		fco	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
4		funco	⊢ ( ( Fun ◡ 𝐺 ∧ Fun ◡ 𝐹 ) → Fun ( ◡ 𝐺 ∘ ◡ 𝐹 ) )
5		cnvco	⊢ ◡ ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 ∘ ◡ 𝐹 )
6	5	funeqi	⊢ ( Fun ◡ ( 𝐹 ∘ 𝐺 ) ↔ Fun ( ◡ 𝐺 ∘ ◡ 𝐹 ) )
7	4 6	sylibr	⊢ ( ( Fun ◡ 𝐺 ∧ Fun ◡ 𝐹 ) → Fun ◡ ( 𝐹 ∘ 𝐺 ) )
8	7	ancoms	⊢ ( ( Fun ◡ 𝐹 ∧ Fun ◡ 𝐺 ) → Fun ◡ ( 𝐹 ∘ 𝐺 ) )
9	3 8	anim12i	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) ∧ ( Fun ◡ 𝐹 ∧ Fun ◡ 𝐺 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ Fun ◡ ( 𝐹 ∘ 𝐺 ) ) )
10	9	an4s	⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ Fun ◡ 𝐹 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐺 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ Fun ◡ ( 𝐹 ∘ 𝐺 ) ) )
11	1 2 10	syl2anb	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ Fun ◡ ( 𝐹 ∘ 𝐺 ) ) )
12		df-f1	⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ↔ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ Fun ◡ ( 𝐹 ∘ 𝐺 ) ) )
13	11 12	sylibr	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 )