Metamath Proof Explorer


Theorem f1coOLD

Description: Obsolete version of f1co as of 20-Sep-2024. (Contributed by NM, 28-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion f1coOLD ( ( 𝐹 : 𝐵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𝐶 )