ltrniotavalbN

Description: Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ltrniotavalb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrniotavalb.a	$⊢ A = Atoms (K)$
	ltrniotavalb.h	$⊢ H = LHyp (K)$
	ltrniotavalb.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrniotavalbN	$⊢ ((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)) \land F \in T) \to (F (P) = Q \leftrightarrow F = (ι f \in T \| f (P) = Q))$

Proof

Step	Hyp	Ref	Expression
1		ltrniotavalb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrniotavalb.a	$⊢ A = Atoms (K)$
3		ltrniotavalb.h	$⊢ H = LHyp (K)$
4		ltrniotavalb.t	$⊢ T = LTrn (K) (W)$
5		simpl1	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to (K \in HL \land W \in H)$
6		simpl3	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to F \in T$
7		simpl2l	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simpl2r	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
9		eqid	$⊢ (ι f \in T \| f (P) = Q) = (ι f \in T \| f (P) = Q)$
10	1 2 3 4 9	ltrniotacl	$⊢ ((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 \in T \| f (P) = Q) \in T$
11	5 7 8 10	syl3anc	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to (ι f \in T \| f (P) = Q) \in T$
12		simpr	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to F (P) = Q$
13	1 2 3 4 9	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 \in T \| f (P) = Q) (P) = Q$
14	5 7 8 13	syl3anc	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to (ι f \in T \| f (P) = Q) (P) = Q$
15	12 14	eqtr4d	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to F (P) = (ι f \in T \| f (P) = Q) (P)$
16	1 2 3 4	cdlemd	$⊢ (((K \in HL \land W \in H) \land F \in T \land (ι f \in T \| f (P) = Q) \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = (ι f \in T \| f (P) = Q) (P)) \to F = (ι f \in T \| f (P) = Q)$
17	5 6 11 7 15 16	syl311anc	$⊢ (((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)) \land F \in T) \land F (P) = Q) \to F = (ι f \in T \| f (P) = Q)$
18		fveq1	$⊢ F = (ι f \in T \| f (P) = Q) \to F (P) = (ι f \in T \| f (P) = Q) (P)$
19		simp1	$⊢ ((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)) \land F \in T) \to (K \in HL \land W \in H)$
20		simp2l	$⊢ ((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)) \land F \in T) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21		simp2r	$⊢ ((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)) \land F \in T) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
22	19 20 21 13	syl3anc	$⊢ ((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)) \land F \in T) \to (ι f \in T \| f (P) = Q) (P) = Q$
23	18 22	sylan9eqr	$⊢ (((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)) \land F \in T) \land F = (ι f \in T \| f (P) = Q)) \to F (P) = Q$
24	17 23	impbida	$⊢ ((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)) \land F \in T) \to (F (P) = Q \leftrightarrow F = (ι f \in T \| f (P) = Q))$

Metamath Proof Explorer

Theorem ltrniotavalbN

Proof