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 F : B 1-1 C G : A 1-1 B F G : A 1-1 C

Proof

Step Hyp Ref Expression
1 df-f1 F : B 1-1 C F : B C Fun F -1
2 df-f1 G : A 1-1 B G : A B Fun G -1
3 fco F : B C G : A B F G : A C
4 funco Fun G -1 Fun F -1 Fun G -1 F -1
5 cnvco F G -1 = G -1 F -1
6 5 funeqi Fun F G -1 Fun G -1 F -1
7 4 6 sylibr Fun G -1 Fun F -1 Fun F G -1
8 7 ancoms Fun F -1 Fun G -1 Fun F G -1
9 3 8 anim12i F : B C G : A B Fun F -1 Fun G -1 F G : A C Fun F G -1
10 9 an4s F : B C Fun F -1 G : A B Fun G -1 F G : A C Fun F G -1
11 1 2 10 syl2anb F : B 1-1 C G : A 1-1 B F G : A C Fun F G -1
12 df-f1 F G : A 1-1 C F G : A C Fun F G -1
13 11 12 sylibr F : B 1-1 C G : A 1-1 B F G : A 1-1 C