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