ltrniotaval

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

	Ref	Expression
Hypotheses	ltrniotaval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrniotaval.a	$⊢ A = Atoms (K)$
	ltrniotaval.h	$⊢ H = LHyp (K)$
	ltrniotaval.t	$⊢ T = LTrn (K) (W)$
	ltrniotaval.f	$⊢ F = (ι f \in T \| f (P) = Q)$
Assertion	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) = Q$

Step	Hyp	Ref	Expression
1		ltrniotaval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrniotaval.a	$⊢ A = Atoms (K)$
3		ltrniotaval.h	$⊢ H = LHyp (K)$
4		ltrniotaval.t	$⊢ T = LTrn (K) (W)$
5		ltrniotaval.f	$⊢ F = (ι f \in T \| f (P) = Q)$
6	1 2 3 4	cdleme	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \exists! f \in T f (P) = Q$
7		nfriota1	$⊢ \underline{Ⅎ} f (ι f \in T \| f (P) = Q)$
8	5 7	nfcxfr	$⊢ \underline{Ⅎ} f F$
9		nfcv	$⊢ \underline{Ⅎ} f P$
10	8 9	nffv	$⊢ \underline{Ⅎ} f F (P)$
11	10	nfeq1	$⊢ Ⅎ f F (P) = Q$
12		fveq1	$⊢ f = F \to f (P) = F (P)$
13	12	eqeq1d	$⊢ f = F \to (f (P) = Q \leftrightarrow F (P) = Q)$
14	11 5 13	riotaprop	$⊢ \exists! f \in T f (P) = Q \to (F \in T \land F (P) = Q)$
15	14	simprd	$⊢ \exists! f \in T f (P) = Q \to F (P) = Q$
16	6 15	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) = Q$

Metamath Proof Explorer