Metamath Proof Explorer

Theorem paddasslem7

Description: Lemma for paddass . Combine paddasslem5 and paddasslem6 . (Contributed by NM, 9-Jan-2012)

		Ref	Expression
	Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
		paddasslem.a	$⊢ A = Atoms (K)$
	Assertion	paddasslem7	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (s \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddasslem.a	$⊢ A = Atoms (K)$
4		simpl1	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to K \in HL$
5		simpl21	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to p \in A$
6		simpl23	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to s \in A$
7	5 6	jca	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to (p \in A \land s \in A)$
8		simpl33	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to z \in A$
9		simpl22	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to r \in A$
10		simpl3	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to (x \in A \land y \in A \land z \in A)$
11		simprl	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
12	1 2 3	paddasslem5	$⊢ ((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \to s \neq z$
13	4 9 10 11 12	syl31anc	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to s \neq z$
14		simprr	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to s \underset{˙}{\leq} (p \underset{˙}{\lor} z)$
15	1 2 3	paddasslem6	$⊢ ((K \in HL \land (p \in A \land s \in A) \land z \in A) \land (s \neq z \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (s \underset{˙}{\lor} z)$
16	4 7 8 13 14 15	syl32anc	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (s \underset{˙}{\lor} z)$