Metamath Proof Explorer

Theorem atexchltN

Description: Atom exchange property. Version of hlatexch2 with less-than ordering. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	atexchlt.s	$⊢ \underset{˙}{<} = <_{K}$
		atexchlt.j	$⊢ \underset{˙}{\lor} = join (K)$
		atexchlt.a	$⊢ A = Atoms (K)$
	Assertion	atexchltN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to Q \underset{˙}{<} (P \underset{˙}{\lor} R))$

Proof

Step	Hyp	Ref	Expression
1		atexchlt.s	$⊢ \underset{˙}{<} = <_{K}$
2		atexchlt.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atexchlt.a	$⊢ A = Atoms (K)$
4		eqid	$⊢ ⋖_{K} = ⋖_{K}$
5	2 3 4	atexchcvrN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P ⋖_{K} (Q \underset{˙}{\lor} R) \to Q ⋖_{K} (P \underset{˙}{\lor} R))$
6	1 2 3 4	atltcvr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \leftrightarrow P ⋖_{K} (Q \underset{˙}{\lor} R))$
7	6	3adant3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \leftrightarrow P ⋖_{K} (Q \underset{˙}{\lor} R))$
8		simpl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in HL$
9		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
10		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
11		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
12	1 2 3 4	atltcvr	$⊢ (K \in HL \land (Q \in A \land P \in A \land R \in A)) \to (Q \underset{˙}{<} (P \underset{˙}{\lor} R) \leftrightarrow Q ⋖_{K} (P \underset{˙}{\lor} R))$
13	8 9 10 11 12	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (Q \underset{˙}{<} (P \underset{˙}{\lor} R) \leftrightarrow Q ⋖_{K} (P \underset{˙}{\lor} R))$
14	13	3adant3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (Q \underset{˙}{<} (P \underset{˙}{\lor} R) \leftrightarrow Q ⋖_{K} (P \underset{˙}{\lor} R))$
15	5 7 14	3imtr4d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to Q \underset{˙}{<} (P \underset{˙}{\lor} R))$