Metamath Proof Explorer


Theorem f1o3d

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

Ref Expression
Hypotheses f1o3d.1 φ F = x A C
f1o3d.2 φ x A C B
f1o3d.3 φ y B D A
f1o3d.4 φ x A y B x = D y = C
Assertion f1o3d φ F : A 1-1 onto B F -1 = y B D

Proof

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