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

Metamath Proof Explorer

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