4atlem11

Description: Lemma for 4at . Combine all three possible cases. (Contributed by NM, 10-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		3anass	$⊢ (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
5		simpl11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in HL$
6	5	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in Lat$
7		simpl2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in A$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
10	7 9	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in {Base}_{K}$
11		simpl2r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in A$
12	8 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
13	11 12	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in {Base}_{K}$
14		simpl12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in A$
15		simpl31	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to U \in A$
16	8 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
17	5 14 15 16	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\lor} U \in {Base}_{K}$
18		simpl32	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \in A$
19		simpl33	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to W \in A$
20	8 2 3	hlatjcl	$⊢ (K \in HL \land V \in A \land W \in A) \to V \underset{˙}{\lor} W \in {Base}_{K}$
21	5 18 19 20	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \underset{˙}{\lor} W \in {Base}_{K}$
22	8 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} U \in {Base}_{K} \land V \underset{˙}{\lor} W \in {Base}_{K}) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
23	6 17 21 22	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
24	8 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
25	6 10 13 23 24	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
26	25	anbi2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \leftrightarrow (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
27	4 26	syl5bb	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
28		simpl13	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in A$
29	8 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
30	28 29	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in {Base}_{K}$
31	8 2 3	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
32	5 7 11 31	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
33	8 1 2	latjle12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K} \land (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
34	6 30 32 23 33	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
35	27 34	bitrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
36		simpl1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land P \in A \land Q \in A)$
37		simpl2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \in A \land S \in A)$
38	18 19	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (V \in A \land W \in A)$
39		simpr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
40	1 2 3	4atlem3a	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W))$
41	36 37 38 39 40	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W))$
42		simp1l	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A))$
43		simp1r	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
44		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
45		simp3	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
46	1 2 3	4atlem11b	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
47	42 43 44 45 46	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
48	47	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
49	5	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to K \in HL$
50	14	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to P \in A$
51	28	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to Q \in A$
52	7	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to R \in A$
53	11	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to S \in A$
54	2 3	hlatj4	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S)$
55	49 50 51 52 53 54	syl122anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S)$
56	49 50 52	3jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (K \in HL \land P \in A \land R \in A)$
57	51 53	jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (Q \in A \land S \in A)$
58		simp1l3	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (U \in A \land V \in A \land W \in A)$
59		simp1r2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
60	1 2 3	4atlem0be	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq R$
61	49 50 51 52 59 60	syl131anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to P \neq R$
62		simp1r1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to P \neq Q$
63	1 2 3	4atlem0ae	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
64	49 50 51 52 62 59 63	syl132anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
65		simp1r3	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
66	2 3	hlatj32	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q$
67	49 50 51 52 66	syl13anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q$
68	67	breq2d	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q))$
69	65 68	mtbid	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q)$
70	61 64 69	3jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \neq R \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q))$
71		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
72		simp32	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
73		simp31	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
74		simp33	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
75	1 2 3	4atlem11b	$⊢ (((K \in HL \land P \in A \land R \in A) \land (Q \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq R \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
76	56 57 58 70 71 72 73 74 75	syl323anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
77	55 76	eqtrd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
78	77	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
79	8 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
80	14 79	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in {Base}_{K}$
81	8 2	latj4rot	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K}) \land (R \in {Base}_{K} \land S \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
82	6 80 30 10 13 81	syl122anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
83	2 3	hlatjcom	$⊢ (K \in HL \land S \in A \land P \in A) \to S \underset{˙}{\lor} P = P \underset{˙}{\lor} S$
84	5 11 14 83	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \underset{˙}{\lor} P = P \underset{˙}{\lor} S$
85	84	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
86	82 85	eqtrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
87	86	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
88	5 14 11	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land P \in A \land S \in A)$
89	28 7	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \in A \land R \in A)$
90		simpl3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (U \in A \land V \in A \land W \in A)$
91	88 89 90	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((K \in HL \land P \in A \land S \in A) \land (Q \in A \land R \in A) \land (U \in A \land V \in A \land W \in A))$
92	91	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to ((K \in HL \land P \in A \land S \in A) \land (Q \in A \land R \in A) \land (U \in A \land V \in A \land W \in A))$
93	1 2 3	4noncolr1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q))$
94	36 37 39 93	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q))$
95		necom	$⊢ S \neq P \leftrightarrow P \neq S$
96	95	a1i	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \neq P \leftrightarrow P \neq S)$
97	84	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \leftrightarrow Q \underset{˙}{\leq} (P \underset{˙}{\lor} S))$
98	97	notbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \leftrightarrow \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} S))$
99	84	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \underset{˙}{\lor} P) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q$
100	99	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q) \leftrightarrow R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q))$
101	100	notbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q) \leftrightarrow \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q))$
102	96 98 101	3anbi123d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q)) \leftrightarrow (P \neq S \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q)))$
103	94 102	mpbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \neq S \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q))$
104	103	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \neq S \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q))$
105		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
106		simpr3	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
107		simpr1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
108		simpr2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
109	106 107 108	3jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
110	109	3adant2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
111	1 2 3	4atlem11b	$⊢ (((K \in HL \land P \in A \land S \in A) \land (Q \in A \land R \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq S \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} Q)) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land (S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
112	92 104 105 110 111	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
113	87 112	eqtrd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land (Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
114	113	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
115	48 78 114	3jaod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
116	41 115	mpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
117	35 116	sylbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4atlem11

Proof