# 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}=\mathrm{ran}\left({x}\in {X}⟼⟨{A},{B}⟩\right)$
flift.2 ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in {R}$
flift.3 ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in {S}$
fliftfun.4 ${⊢}{x}={y}\to {A}={C}$
fliftfun.5 ${⊢}{x}={y}\to {B}={D}$
Assertion fliftfun ${⊢}{\phi }\to \left(\mathrm{Fun}{F}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({A}={C}\to {B}={D}\right)\right)$

### Proof

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