Metamath Proof Explorer


Theorem f1ocan2fv

Description: Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion f1ocan2fv Fun F G : A 1-1 onto B X A F G -1 G X = F X

Proof

Step Hyp Ref Expression
1 f1orel G : A 1-1 onto B Rel G
2 dfrel2 Rel G G -1 -1 = G
3 1 2 sylib G : A 1-1 onto B G -1 -1 = G
4 3 3ad2ant2 Fun F G : A 1-1 onto B X A G -1 -1 = G
5 4 fveq1d Fun F G : A 1-1 onto B X A G -1 -1 X = G X
6 5 fveq2d Fun F G : A 1-1 onto B X A F G -1 G -1 -1 X = F G -1 G X
7 f1ocnv G : A 1-1 onto B G -1 : B 1-1 onto A
8 f1ocan1fv Fun F G -1 : B 1-1 onto A X A F G -1 G -1 -1 X = F X
9 7 8 syl3an2 Fun F G : A 1-1 onto B X A F G -1 G -1 -1 X = F X
10 6 9 eqtr3d Fun F G : A 1-1 onto B X A F G -1 G X = F X