Theorem ltrniotaval

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

	Ref	Expression
Hypotheses	ltrniotaval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	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	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to F\left(P\right)=Q$$

Proof

Step	Hyp	Ref	Expression
1		ltrniotaval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
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	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \exists !f\in Tf\left(P\right)=Q$$
7		nfriota1	$$⊢\underset{\_}{Ⅎ}f\left(\iota f\in T|f\left(P\right)=Q\right)$$
8	5 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}fF$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}fP$$
10	8 9	nffv	$$⊢\underset{\_}{Ⅎ}fF\left(P\right)$$
11	10	nfeq1	$$⊢ℲfF\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\leftrightarrow F\left(P\right)=Q\right)$$
14	11 5 13	riotaprop	$$⊢\exists !f\in Tf\left(P\right)=Q\to \left(F\in T\wedge F\left(P\right)=Q\right)$$
15	14	simprd	$$⊢\exists !f\in Tf\left(P\right)=Q\to F\left(P\right)=Q$$
16	6 15	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to F\left(P\right)=Q$$