Metamath Proof Explorer


Theorem f1ocnvfv2

Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

Ref Expression
Assertion f1ocnvfv2 F : A 1-1 onto B C B F F -1 C = C

Proof

Step Hyp Ref Expression
1 f1ococnv2 F : A 1-1 onto B F F -1 = I B
2 1 fveq1d F : A 1-1 onto B F F -1 C = I B C
3 2 adantr F : A 1-1 onto B C B F F -1 C = I B C
4 f1ocnv F : A 1-1 onto B F -1 : B 1-1 onto A
5 f1of F -1 : B 1-1 onto A F -1 : B A
6 4 5 syl F : A 1-1 onto B F -1 : B A
7 fvco3 F -1 : B A C B F F -1 C = F F -1 C
8 6 7 sylan F : A 1-1 onto B C B F F -1 C = F F -1 C
9 fvresi C B I B C = C
10 9 adantl F : A 1-1 onto B C B I B C = C
11 3 8 10 3eqtr3d F : A 1-1 onto B C B F F -1 C = C