# Metamath Proof Explorer

## Theorem ltrniotaval

Description: Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014)

Ref Expression
Hypotheses ltrniotaval.l
ltrniotaval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
ltrniotaval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
ltrniotaval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
ltrniotaval.f ${⊢}{F}=\left(\iota {f}\in {T}|{f}\left({P}\right)={Q}\right)$
Assertion ltrniotaval

### Proof

Step Hyp Ref Expression
1 ltrniotaval.l
2 ltrniotaval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 ltrniotaval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 ltrniotaval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 ltrniotaval.f ${⊢}{F}=\left(\iota {f}\in {T}|{f}\left({P}\right)={Q}\right)$
6 1 2 3 4 cdleme
7 nfriota1 ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}\left(\iota {f}\in {T}|{f}\left({P}\right)={Q}\right)$
8 5 7 nfcxfr ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{F}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{P}$
10 8 9 nffv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{F}\left({P}\right)$
11 10 nfeq1 ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{F}\left({P}\right)={Q}$
12 fveq1 ${⊢}{f}={F}\to {f}\left({P}\right)={F}\left({P}\right)$
13 12 eqeq1d ${⊢}{f}={F}\to \left({f}\left({P}\right)={Q}↔{F}\left({P}\right)={Q}\right)$
14 11 5 13 riotaprop ${⊢}\exists !{f}\in {T}\phantom{\rule{.4em}{0ex}}{f}\left({P}\right)={Q}\to \left({F}\in {T}\wedge {F}\left({P}\right)={Q}\right)$
15 14 simprd ${⊢}\exists !{f}\in {T}\phantom{\rule{.4em}{0ex}}{f}\left({P}\right)={Q}\to {F}\left({P}\right)={Q}$
16 6 15 syl