ltrnateq

Description: If any atom (under W ) is not equal to its translation, so is any other atom. (Contributed by NM, 6-May-2013)

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

Step	Hyp	Ref	Expression
1		ltrn2eq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrn2eq.a	$⊢ A = Atoms (K)$
3		ltrn2eq.h	$⊢ H = LHyp (K)$
4		ltrn2eq.t	$⊢ T = LTrn (K) (W)$
5	1 2 3 4	ltrn2ateq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (F (P) = P \leftrightarrow F (Q) = Q)$
6	5	biimp3a	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F (P) = P) \to F (Q) = Q$

Metamath Proof Explorer