Metamath Proof Explorer

Theorem ltrneq3

Description: Two translations agree at any atom not under the fiducial co-atom W iff they are equal. (Contributed by NM, 25-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemd.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd.a	$⊢ A = Atoms (K)$
3		cdlemd.h	$⊢ H = LHyp (K)$
4		cdlemd.t	$⊢ T = LTrn (K) (W)$
5		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to (K \in HL \land W \in H)$
6		simpl2l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to F \in T$
7		simpl2r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to G \in T$
8		simpl3	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to F (P) = G (P)$
10	1 2 3 4	cdlemd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F = G$
11	5 6 7 8 9 10	syl311anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = G (P)) \to F = G$
12		fveq1	$⊢ F = G \to F (P) = G (P)$
13	12	adantl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = G) \to F (P) = G (P)$
14	11 13	impbida	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) = G (P) \leftrightarrow F = G)$