Metamath Proof Explorer


Theorem fliftfun

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 F = ran x X A B
flift.2 φ x X A R
flift.3 φ x X B S
fliftfun.4 x = y A = C
fliftfun.5 x = y B = D
Assertion fliftfun φ Fun F x X y X A = C B = D

Proof

Step Hyp Ref Expression
1 flift.1 F = ran x X A B
2 flift.2 φ x X A R
3 flift.3 φ x X B S
4 fliftfun.4 x = y A = C
5 fliftfun.5 x = y B = D
6 nfv x φ
7 nfmpt1 _ x x X A B
8 7 nfrn _ x ran x X A B
9 1 8 nfcxfr _ x F
10 9 nffun x Fun F
11 fveq2 A = C F A = F C
12 simplr φ Fun F x X y X Fun F
13 1 2 3 fliftel1 φ x X A F B
14 13 ad2ant2r φ Fun F x X y X A F B
15 funbrfv Fun F A F B F A = B
16 12 14 15 sylc φ Fun F x X y X F A = B
17 simprr φ Fun F x X y X y X
18 eqidd φ Fun F x X y X C = C
19 eqidd φ Fun F x X y X D = D
20 4 eqeq2d x = y C = A C = C
21 5 eqeq2d x = y D = B D = D
22 20 21 anbi12d x = y C = A D = B C = C D = D
23 22 rspcev y X C = C D = D x X C = A D = B
24 17 18 19 23 syl12anc φ Fun F x X y X x X C = A D = B
25 1 2 3 fliftel φ C F D x X C = A D = B
26 25 ad2antrr φ Fun F x X y X C F D x X C = A D = B
27 24 26 mpbird φ Fun F x X y X C F D
28 funbrfv Fun F C F D F C = D
29 12 27 28 sylc φ Fun F x X y X F C = D
30 16 29 eqeq12d φ Fun F x X y X F A = F C B = D
31 11 30 syl5ib φ Fun F x X y X A = C B = D
32 31 anassrs φ Fun F x X y X A = C B = D
33 32 ralrimiva φ Fun F x X y X A = C B = D
34 33 exp31 φ Fun F x X y X A = C B = D
35 6 10 34 ralrimd φ Fun F x X y X A = C B = D
36 1 2 3 fliftel φ z F u x X z = A u = B
37 1 2 3 fliftel φ z F v x X z = A v = B
38 4 eqeq2d x = y z = A z = C
39 5 eqeq2d x = y v = B v = D
40 38 39 anbi12d x = y z = A v = B z = C v = D
41 40 cbvrexvw x X z = A v = B y X z = C v = D
42 37 41 bitrdi φ z F v y X z = C v = D
43 36 42 anbi12d φ z F u z F v x X z = A u = B y X z = C v = D
44 43 biimpd φ z F u z F v x X z = A u = B y X z = C v = D
45 reeanv x X y X z = A u = B z = C v = D x X z = A u = B y X z = C v = D
46 r19.29 x X y X A = C B = D x X y X z = A u = B z = C v = D x X y X A = C B = D y X z = A u = B z = C v = D
47 r19.29 y X A = C B = D y X z = A u = B z = C v = D y X A = C B = D z = A u = B z = C v = D
48 eqtr2 z = A z = C A = C
49 48 ad2ant2r z = A u = B z = C v = D A = C
50 49 imim1i A = C B = D z = A u = B z = C v = D B = D
51 50 imp A = C B = D z = A u = B z = C v = D B = D
52 simprlr A = C B = D z = A u = B z = C v = D u = B
53 simprrr A = C B = D z = A u = B z = C v = D v = D
54 51 52 53 3eqtr4d A = C B = D z = A u = B z = C v = D u = v
55 54 rexlimivw y X A = C B = D z = A u = B z = C v = D u = v
56 47 55 syl y X A = C B = D y X z = A u = B z = C v = D u = v
57 56 rexlimivw x X y X A = C B = D y X z = A u = B z = C v = D u = v
58 46 57 syl x X y X A = C B = D x X y X z = A u = B z = C v = D u = v
59 58 ex x X y X A = C B = D x X y X z = A u = B z = C v = D u = v
60 45 59 syl5bir x X y X A = C B = D x X z = A u = B y X z = C v = D u = v
61 44 60 syl9 φ x X y X A = C B = D z F u z F v u = v
62 61 alrimdv φ x X y X A = C B = D v z F u z F v u = v
63 62 alrimdv φ x X y X A = C B = D u v z F u z F v u = v
64 63 alrimdv φ x X y X A = C B = D z u v z F u z F v u = v
65 1 2 3 fliftrel φ F R × S
66 relxp Rel R × S
67 relss F R × S Rel R × S Rel F
68 65 66 67 mpisyl φ Rel F
69 dffun2 Fun F Rel F z u v z F u z F v u = v
70 69 baib Rel F Fun F z u v z F u z F v u = v
71 68 70 syl φ Fun F z u v z F u z F v u = v
72 64 71 sylibrd φ x X y X A = C B = D Fun F
73 35 72 impbid φ Fun F x X y X A = C B = D