Theorem f1o3d

Description: Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		f1o3d.1	|- ( ph -> F = ( x e. A |-> C ) )
2		f1o3d.2	|- ( ( ph /\ x e. A ) -> C e. B )
3		f1o3d.3	|- ( ( ph /\ y e. B ) -> D e. A )
4		f1o3d.4	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
5	2	ralrimiva	|- ( ph -> A. x e. A C e. B )
6		eqid	|- ( x e. A |-> C ) = ( x e. A |-> C )
7	6	fnmpt	|- ( A. x e. A C e. B -> ( x e. A |-> C ) Fn A )
8	5 7	syl	|- ( ph -> ( x e. A |-> C ) Fn A )
9	1	fneq1d	|- ( ph -> ( F Fn A <-> ( x e. A |-> C ) Fn A ) )
10	8 9	mpbird	|- ( ph -> F Fn A )
11	3	ralrimiva	|- ( ph -> A. y e. B D e. A )
12		eqid	|- ( y e. B |-> D ) = ( y e. B |-> D )
13	12	fnmpt	|- ( A. y e. B D e. A -> ( y e. B |-> D ) Fn B )
14	11 13	syl	|- ( ph -> ( y e. B |-> D ) Fn B )
15		eleq1a	|- ( C e. B -> ( y = C -> y e. B ) )
16	2 15	syl	|- ( ( ph /\ x e. A ) -> ( y = C -> y e. B ) )
17	16	impr	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> y e. B )
18	4	biimpar	|- ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ y = C ) -> x = D )
19	18	exp42	|- ( ph -> ( x e. A -> ( y e. B -> ( y = C -> x = D ) ) ) )
20	19	com34	|- ( ph -> ( x e. A -> ( y = C -> ( y e. B -> x = D ) ) ) )
21	20	imp32	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B -> x = D ) )
22	17 21	jcai	|- ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B /\ x = D ) )
23		eleq1a	|- ( D e. A -> ( x = D -> x e. A ) )
24	3 23	syl	|- ( ( ph /\ y e. B ) -> ( x = D -> x e. A ) )
25	24	impr	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> x e. A )
26	4	biimpa	|- ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ x = D ) -> y = C )
27	26	exp42	|- ( ph -> ( x e. A -> ( y e. B -> ( x = D -> y = C ) ) ) )
28	27	com23	|- ( ph -> ( y e. B -> ( x e. A -> ( x = D -> y = C ) ) ) )
29	28	com34	|- ( ph -> ( y e. B -> ( x = D -> ( x e. A -> y = C ) ) ) )
30	29	imp32	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A -> y = C ) )
31	25 30	jcai	|- ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A /\ y = C ) )
32	22 31	impbida	|- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
33	32	opabbidv	|- ( ph -> { <. y , x >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( y e. B /\ x = D ) } )
34		df-mpt	|- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
35	1 34	eqtrdi	|- ( ph -> F = { <. x , y >. | ( x e. A /\ y = C ) } )
36	35	cnveqd	|- ( ph -> `' F = `' { <. x , y >. | ( x e. A /\ y = C ) } )
37		cnvopab	|- `' { <. x , y >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( x e. A /\ y = C ) }
38	36 37	eqtrdi	|- ( ph -> `' F = { <. y , x >. | ( x e. A /\ y = C ) } )
39		df-mpt	|- ( y e. B |-> D ) = { <. y , x >. | ( y e. B /\ x = D ) }
40	39	a1i	|- ( ph -> ( y e. B |-> D ) = { <. y , x >. | ( y e. B /\ x = D ) } )
41	33 38 40	3eqtr4d	|- ( ph -> `' F = ( y e. B |-> D ) )
42	41	fneq1d	|- ( ph -> ( `' F Fn B <-> ( y e. B |-> D ) Fn B ) )
43	14 42	mpbird	|- ( ph -> `' F Fn B )
44		dff1o4	|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
45	10 43 44	sylanbrc	|- ( ph -> F : A -1-1-onto-> B )
46	45 41	jca	|- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )