paddasslem4

	Ref	Expression
Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddasslem.a	$⊢ A = Atoms (K)$
Assertion	paddasslem4	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \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		simpl11	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to K \in HL$
5		simpl21	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to x \in A$
6		simpl13	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to r \in A$
7		simpl22	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to y \in A$
8	5 6 7	3jca	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (x \in A \land r \in A \land y \in A)$
9		simpl12	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in A$
10		simpl23	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to z \in A$
11	9 10	jca	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (p \in A \land z \in A)$
12	4 8 11	3jca	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (K \in HL \land (x \in A \land r \in A \land y \in A) \land (p \in A \land z \in A))$
13		simpl32	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to x \neq y$
14		simpl33	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
15	1 2 3	paddasslem1	$⊢ ((K \in HL \land (x \in A \land r \in A \land y \in A) \land x \neq y) \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to \neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y)$
16	4 8 13 14 15	syl31anc	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to \neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y)$
17		simpl31	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \neq z$
18		simprl	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (x \underset{˙}{\lor} r)$
19		simpl2	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (x \in A \land y \in A \land z \in A)$
20		simprr	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
21	1 2 3	paddasslem2	$⊢ ((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))) \to z \underset{˙}{\leq} (r \underset{˙}{\lor} y)$
22	4 6 19 14 20 21	syl212anc	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to z \underset{˙}{\leq} (r \underset{˙}{\lor} y)$
23	18 22	jca	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y))$
24	16 17 23	jca31	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to ((\neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y) \land p \neq z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y)))$
25	1 2 3	paddasslem3	$⊢ (K \in HL \land (x \in A \land r \in A \land y \in A) \land (p \in A \land z \in A)) \to (((\neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y) \land p \neq z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))$
26	12 24 25	sylc	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))$

Metamath Proof Explorer

Theorem paddasslem4

Proof