Metamath Proof Explorer


Theorem fcnvres

Description: The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998)

Ref Expression
Assertion fcnvres
|- ( F : A --> B -> `' ( F |` A ) = ( `' F |` B ) )

Proof

Step Hyp Ref Expression
1 relcnv
 |-  Rel `' ( F |` A )
2 relres
 |-  Rel ( `' F |` B )
3 opelf
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> ( x e. A /\ y e. B ) )
4 3 simpld
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> x e. A )
5 4 ex
 |-  ( F : A --> B -> ( <. x , y >. e. F -> x e. A ) )
6 5 pm4.71rd
 |-  ( F : A --> B -> ( <. x , y >. e. F <-> ( x e. A /\ <. x , y >. e. F ) ) )
7 vex
 |-  y e. _V
8 vex
 |-  x e. _V
9 7 8 opelcnv
 |-  ( <. y , x >. e. `' ( F |` A ) <-> <. x , y >. e. ( F |` A ) )
10 7 opelresi
 |-  ( <. x , y >. e. ( F |` A ) <-> ( x e. A /\ <. x , y >. e. F ) )
11 9 10 bitri
 |-  ( <. y , x >. e. `' ( F |` A ) <-> ( x e. A /\ <. x , y >. e. F ) )
12 6 11 bitr4di
 |-  ( F : A --> B -> ( <. x , y >. e. F <-> <. y , x >. e. `' ( F |` A ) ) )
13 3 simprd
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> y e. B )
14 13 ex
 |-  ( F : A --> B -> ( <. x , y >. e. F -> y e. B ) )
15 14 pm4.71rd
 |-  ( F : A --> B -> ( <. x , y >. e. F <-> ( y e. B /\ <. x , y >. e. F ) ) )
16 8 opelresi
 |-  ( <. y , x >. e. ( `' F |` B ) <-> ( y e. B /\ <. y , x >. e. `' F ) )
17 7 8 opelcnv
 |-  ( <. y , x >. e. `' F <-> <. x , y >. e. F )
18 17 anbi2i
 |-  ( ( y e. B /\ <. y , x >. e. `' F ) <-> ( y e. B /\ <. x , y >. e. F ) )
19 16 18 bitri
 |-  ( <. y , x >. e. ( `' F |` B ) <-> ( y e. B /\ <. x , y >. e. F ) )
20 15 19 bitr4di
 |-  ( F : A --> B -> ( <. x , y >. e. F <-> <. y , x >. e. ( `' F |` B ) ) )
21 12 20 bitr3d
 |-  ( F : A --> B -> ( <. y , x >. e. `' ( F |` A ) <-> <. y , x >. e. ( `' F |` B ) ) )
22 1 2 21 eqrelrdv
 |-  ( F : A --> B -> `' ( F |` A ) = ( `' F |` B ) )