This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltrnatneq

Description: If any atom (under W ) is not equal to its translation, so is any other atom. TODO: -. P .<_ W isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (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	ltrnatneq	$⊢ ((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) \neq P) \to F (Q) \neq Q$

Proof

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	necon3bid	$⊢ ((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) \neq P \leftrightarrow F (Q) \neq Q)$
7	6	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) \neq P) \to F (Q) \neq Q$