Theorem f1ocnv2d

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 )
	f1o2d.2	|- ( ( ph /\ x e. A ) -> C e. B )
	f1o2d.3	|- ( ( ph /\ y e. B ) -> D e. A )
	f1o2d.4	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
Assertion	f1ocnv2d	|- ( 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		f1o2d.2	|- ( ( ph /\ x e. A ) -> C e. B )
3		f1o2d.3	|- ( ( ph /\ y e. B ) -> D e. A )
4		f1o2d.4	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
5		eleq1a	|- ( C e. B -> ( y = C -> y e. B ) )
6	2 5	syl	|- ( ( ph /\ x e. A ) -> ( y = C -> y e. B ) )
7	6	impr	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> y e. B )
8	4	biimpar	|- ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ y = C ) -> x = D )
9	8	exp42	|- ( ph -> ( x e. A -> ( y e. B -> ( y = C -> x = D ) ) ) )
10	9	com34	|- ( ph -> ( x e. A -> ( y = C -> ( y e. B -> x = D ) ) ) )
11	10	imp32	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B -> x = D ) )
12	7 11	jcai	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B /\ x = D ) )
13		eleq1a	|- ( D e. A -> ( x = D -> x e. A ) )
14	3 13	syl	|- ( ( ph /\ y e. B ) -> ( x = D -> x e. A ) )
15	14	impr	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> x e. A )
16	4	biimpa	|- ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ x = D ) -> y = C )
17	16	exp42	|- ( ph -> ( x e. A -> ( y e. B -> ( x = D -> y = C ) ) ) )
18	17	com23	|- ( ph -> ( y e. B -> ( x e. A -> ( x = D -> y = C ) ) ) )
19	18	com34	|- ( ph -> ( y e. B -> ( x = D -> ( x e. A -> y = C ) ) ) )
20	19	imp32	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A -> y = C ) )
21	15 20	jcai	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A /\ y = C ) )
22	12 21	impbida	|- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
23	1 2 3 22	f1ocnvd	|- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )