Metamath Proof Explorer

Theorem cdlemeiota

Description: A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg1c.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg1c.a	$⊢ A = Atoms (K)$
3		cdlemg1c.h	$⊢ H = LHyp (K)$
4		cdlemg1c.t	$⊢ T = LTrn (K) (W)$
5		eqidd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to F (P) = F (P)$
6		simp3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to F \in T$
7	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
8	7	3com23	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
9	1 2 3 4	cdleme	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to \exists! f \in T f (P) = F (P)$
10	8 9	syld3an3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to \exists! f \in T f (P) = F (P)$
11		fveq1	$⊢ f = F \to f (P) = F (P)$
12	11	eqeq1d	$⊢ f = F \to (f (P) = F (P) \leftrightarrow F (P) = F (P))$
13	12	riota2	$⊢ (F \in T \land \exists! f \in T f (P) = F (P)) \to (F (P) = F (P) \leftrightarrow (ι f \in T \| f (P) = F (P)) = F)$
14	6 10 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to (F (P) = F (P) \leftrightarrow (ι f \in T \| f (P) = F (P)) = F)$
15	5 14	mpbid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to (ι f \in T \| f (P) = F (P)) = F$
16	15	eqcomd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to F = (ι f \in T \| f (P) = F (P))$