Theorem f1ocnvd

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	f1od.1	|- F = ( x e. A |-> C )
	f1od.2	|- ( ( ph /\ x e. A ) -> C e. W )
	f1od.3	|- ( ( ph /\ y e. B ) -> D e. X )
	f1od.4	|- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
Assertion	f1ocnvd	|- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )

Proof

Step	Hyp	Ref	Expression
1		f1od.1	|- F = ( x e. A |-> C )
2		f1od.2	|- ( ( ph /\ x e. A ) -> C e. W )
3		f1od.3	|- ( ( ph /\ y e. B ) -> D e. X )
4		f1od.4	|- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
5	2	ralrimiva	|- ( ph -> A. x e. A C e. W )
6	1	fnmpt	|- ( A. x e. A C e. W -> F Fn A )
7	5 6	syl	|- ( ph -> F Fn A )
8	3	ralrimiva	|- ( ph -> A. y e. B D e. X )
9		eqid	|- ( y e. B |-> D ) = ( y e. B |-> D )
10	9	fnmpt	|- ( A. y e. B D e. X -> ( y e. B |-> D ) Fn B )
11	8 10	syl	|- ( ph -> ( y e. B |-> D ) Fn B )
12	4	opabbidv	|- ( ph -> { <. y , x >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( y e. B /\ x = D ) } )
13		df-mpt	|- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
14	1 13	eqtri	|- F = { <. x , y >. | ( x e. A /\ y = C ) }
15	14	cnveqi	|- `' F = `' { <. x , y >. | ( x e. A /\ y = C ) }
16		cnvopab	|- `' { <. x , y >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( x e. A /\ y = C ) }
17	15 16	eqtri	|- `' F = { <. y , x >. | ( x e. A /\ y = C ) }
18		df-mpt	|- ( y e. B |-> D ) = { <. y , x >. | ( y e. B /\ x = D ) }
19	12 17 18	3eqtr4g	|- ( ph -> `' F = ( y e. B |-> D ) )
20	19	fneq1d	|- ( ph -> ( `' F Fn B <-> ( y e. B |-> D ) Fn B ) )
21	11 20	mpbird	|- ( ph -> `' F Fn B )
22		dff1o4	|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
23	7 21 22	sylanbrc	|- ( ph -> F : A -1-1-onto-> B )
24	23 19	jca	|- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )