Theorem f1co

Description: Composition of one-to-one functions when the codomain of the first matches the domain of the second. Exercise 30 of TakeutiZaring p. 25. (Contributed by NM, 28-May-1998) (Proof shortened by AV, 20-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		f1cof1	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –1-1→ 𝐶 )
2		f1f	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 → 𝐺 : 𝐴 ⟶ 𝐵 )
3		fimacnv	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )
4	2 3	syl	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )
5	4	adantl	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )
6	5	eqcomd	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → 𝐴 = ( ◡ 𝐺 “ 𝐵 ) )
7		f1eq2	⊢ ( 𝐴 = ( ◡ 𝐺 “ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –1-1→ 𝐶 ) )
8	6 7	syl	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) –1-1→ 𝐶 ) )
9	1 8	mpbird	⊢ ( ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –1-1→ 𝐶 )