This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )