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

Metamath Proof Explorer

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