Theorem f1cof1

Description: Composition of two one-to-one functions. Generalization of f1co . (Contributed by AV, 18-Sep-2024)

	Ref	Expression
Assertion	f1cof1	⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝐷 ∧ 𝐺 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐶 ) –1-1→ 𝐷 )

Proof

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