Metamath Proof Explorer


Theorem fsuppcolem

Description: Lemma for fsuppco . Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses fsuppcolem.f φ F -1 V Z Fin
fsuppcolem.g φ G : X 1-1 Y
Assertion fsuppcolem φ F G -1 V Z Fin

Proof

Step Hyp Ref Expression
1 fsuppcolem.f φ F -1 V Z Fin
2 fsuppcolem.g φ G : X 1-1 Y
3 cnvco F G -1 = G -1 F -1
4 3 imaeq1i F G -1 V Z = G -1 F -1 V Z
5 imaco G -1 F -1 V Z = G -1 F -1 V Z
6 4 5 eqtri F G -1 V Z = G -1 F -1 V Z
7 df-f1 G : X 1-1 Y G : X Y Fun G -1
8 7 simprbi G : X 1-1 Y Fun G -1
9 2 8 syl φ Fun G -1
10 imafi Fun G -1 F -1 V Z Fin G -1 F -1 V Z Fin
11 9 1 10 syl2anc φ G -1 F -1 V Z Fin
12 6 11 eqeltrid φ F G -1 V Z Fin