Theorem 4atlem12 38352

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

Hypotheses

Ref	Expression
4at.l	⊢ ≤ = (le‘𝐾)
4at.j	⊢ ∨ = (join‘𝐾)
4at.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
4atlem12	⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))

Proof of Theorem 4atlem12

Step	Hyp	Ref	Expression
1		simpl11 1248	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ HL)
2	1	hllatd 38103	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ Lat)
3		simpl12 1249	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑃 ∈ 𝐴)
4		eqid 2732	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
5		4at.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
6	4, 5	atbase 38028	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
7	3, 6	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑃 ∈ (Base‘𝐾))
8		simpl13 1250	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑄 ∈ 𝐴)
9	4, 5	atbase 38028	. . . . . 6 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
10	8, 9	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑄 ∈ (Base‘𝐾))
11		simpl23 1253	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑇 ∈ 𝐴)
12		simpl31 1254	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑈 ∈ 𝐴)
13		4at.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
14	4, 13, 5	hlatjcl 38106	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
15	1, 11, 12, 14	syl3anc 1371	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
16		simpl32 1255	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑉 ∈ 𝐴)
17		simpl33 1256	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑊 ∈ 𝐴)
18	4, 13, 5	hlatjcl 38106	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) → (𝑉 ∨ 𝑊) ∈ (Base‘𝐾))
19	1, 16, 17, 18	syl3anc 1371	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑉 ∨ 𝑊) ∈ (Base‘𝐾))
20	4, 13	latjcl 18376	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑉 ∨ 𝑊) ∈ (Base‘𝐾)) → ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))
21	2, 15, 19, 20	syl3anc 1371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))
22		4at.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
23	4, 22, 13	latjle12 18387	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))) → ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑃 ∨ 𝑄) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
24	2, 7, 10, 21, 23	syl13anc 1372	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑃 ∨ 𝑄) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
25		simpl21 1251	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ 𝐴)
26	4, 5	atbase 38028	. . . . . 6 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ (Base‘𝐾))
28		simpl22 1252	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ 𝐴)
29	4, 5	atbase 38028	. . . . . 6 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ (Base‘𝐾))
31	4, 22, 13	latjle12 18387	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))) → ((𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑅 ∨ 𝑆) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
32	2, 27, 30, 21, 31	syl13anc 1372	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑅 ∨ 𝑆) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
33	24, 32	anbi12d 631	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) ↔ ((𝑃 ∨ 𝑄) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
34		simpl1 1191	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
35	4, 13, 5	hlatjcl 38106	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
36	34, 35	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
37	4, 13, 5	hlatjcl 38106	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
38	1, 25, 28, 37	syl3anc 1371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
39	4, 22, 13	latjle12 18387	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑄) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
40	2, 36, 38, 21, 39	syl13anc 1372	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
41	33, 40	bitrd 278	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
42		simp1l 1197	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
43		simp1r 1198	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
44		simp2 1137	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))
45		simp3 1138	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
46	22, 13, 5	4atlem12b 38351	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
47	42, 43, 44, 45, 46	syl121anc 1375	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
48	47	3exp 1119	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
49	4, 13	latj4rot 18427	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑃)) = ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)))
50	2, 10, 27, 30, 7, 49	syl122anc 1379	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑃)) = ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)))
51	50	3ad2ant1 1133	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑃)) = ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)))
52	1, 8, 25	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
53	28, 3, 11	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
54		simpl3 1193	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴))
55	52, 53, 54	3jca 1128	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
56	55	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
57		simpr 485	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
58	22, 13, 5	4noncolr3 38193	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)))
59	34, 25, 28, 57, 58	syl121anc 1375	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)))
60	59	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)))
61		simp2 1137	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))
62		simprlr 778	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
63		simprrl 779	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
64	62, 63	jca 512	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
65		simprrr 780	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
66		simprll 777	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
67	64, 65, 66	jca32 516	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
68	67	3adant2 1131	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
69	22, 13, 5	4atlem12b 38351	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∧ ((𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑃)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
70	56, 60, 61, 68, 69	syl121anc 1375	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑃)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
71	51, 70	eqtr3d 2774	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
72	71	3exp 1119	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
73	48, 72	jaod 857	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
74	4, 13	latjcom 18384	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑅 ∨ 𝑆) ∨ (𝑃 ∨ 𝑄)))
75	2, 36, 38, 74	syl3anc 1371	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑅 ∨ 𝑆) ∨ (𝑃 ∨ 𝑄)))
76	75	3ad2ant1 1133	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑅 ∨ 𝑆) ∨ (𝑃 ∨ 𝑄)))
77	1, 25, 28	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
78	3, 8, 11	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
79	77, 78, 54	3jca 1128	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
80	79	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
81	22, 13, 5	4noncolr2 38194	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑆) ∧ ¬ 𝑄 ≤ ((𝑅 ∨ 𝑆) ∨ 𝑃)))
82	34, 25, 28, 57, 81	syl121anc 1375	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑆) ∧ ¬ 𝑄 ≤ ((𝑅 ∨ 𝑆) ∨ 𝑃)))
83	82	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑆) ∧ ¬ 𝑄 ≤ ((𝑅 ∨ 𝑆) ∨ 𝑃)))
84		simp2 1137	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))
85		simprr 771	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
86		simprl 769	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
87	85, 86	jca 512	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
88	87	3adant2 1131	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
89	22, 13, 5	4atlem12b 38351	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑆) ∧ ¬ 𝑄 ≤ ((𝑅 ∨ 𝑆) ∨ 𝑃)) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∧ ((𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑅 ∨ 𝑆) ∨ (𝑃 ∨ 𝑄)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
90	80, 83, 84, 88, 89	syl121anc 1375	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑅 ∨ 𝑆) ∨ (𝑃 ∨ 𝑄)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
91	76, 90	eqtrd 2772	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
92	91	3exp 1119	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
93	4, 13	latj4rot 18427	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)))
94	2, 7, 10, 27, 30, 93	syl122anc 1379	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)))
95	94	3ad2ant1 1133	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)))
96	1, 28, 3	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴))
97	8, 25, 11	3jca 1128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
98	96, 97, 54	3jca 1128	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
99	98	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
100	22, 13, 5	4noncolr1 38195	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)))
101	34, 25, 28, 57, 100	syl121anc 1375	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)))
102	101	3ad2ant1 1133	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)))
103		simp2 1137	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))
104	65, 66	jca 512	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → (𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
105	104, 62, 63	jca32 516	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
106	105	3adant2 1131	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
107	22, 13, 5	4atlem12b 38351	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∧ ((𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
108	99, 102, 103, 106, 107	syl121anc 1375	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
109	95, 108	eqtrd 2772	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
110	109	3exp 1119	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
111	92, 110	jaod 857	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
112	25, 28, 12	3jca 1128	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
113	16, 17	jca 512	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴))
114	22, 13, 5	4atlem3 38336	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∨ (¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))))
115	34, 112, 113, 57, 114	syl31anc 1373	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑄 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∨ (¬ 𝑅 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊))))
116	73, 111, 115	mpjaod 858	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
117	41, 116	sylbird 259	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940   class class class wbr 5142  ‘cfv 6533  (class class class)co 7394  Basecbs 17128  lecple 17188  joincjn 18248  Latclat 18368  Atomscatm 38002  HLchlt 38089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-proset 18232  df-poset 18250  df-plt 18267  df-lub 18283  df-glb 18284  df-join 18285  df-meet 18286  df-p0 18362  df-lat 18369  df-clat 18436  df-oposet 37915  df-ol 37917  df-oml 37918  df-covers 38005  df-ats 38006  df-atl 38037  df-cvlat 38061  df-hlat 38090  df-llines 38238  df-lplanes 38239  df-lvols 38240

This theorem is referenced by:  4at  38353