Theorem dalawlem6 39853

Description: Lemma for dalaw 39863. First piece of dalawlem8 39855. (Contributed by NM, 6-Oct-2012.)

Hypotheses

Ref	Expression
dalawlem.l	⊢ ≤ = (le‘𝐾)
dalawlem.j	⊢ ∨ = (join‘𝐾)
dalawlem.m	⊢ ∧ = (meet‘𝐾)
dalawlem.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
dalawlem6	⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))

Proof of Theorem dalawlem6

Step	Hyp	Ref	Expression
1		eqid 2734	. 2 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		dalawlem.l	. 2 ⊢ ≤ = (le‘𝐾)
3		simp11 1203	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ HL)
4	3	hllatd 39340	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ Lat)
5		simp21 1206	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
6		simp22 1207	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
7		dalawlem.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
8		dalawlem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9	1, 7, 8	hlatjcl 39343	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
10	3, 5, 6, 9	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
11		simp32 1210	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑇 ∈ 𝐴)
12	1, 8	atbase 39265	. . . . 5 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾))
13	11, 12	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑇 ∈ (Base‘𝐾))
14	1, 7	latjcl 18454	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Base‘𝐾))
15	4, 10, 13, 14	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Base‘𝐾))
16		simp31 1209	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ∈ 𝐴)
17	1, 8	atbase 39265	. . . 4 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
18	16, 17	syl 17	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ∈ (Base‘𝐾))
19		dalawlem.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
20	1, 19	latmcl 18455	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Base‘𝐾))
21	4, 15, 18, 20	syl3anc 1372	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Base‘𝐾))
22		simp23 1208	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ∈ 𝐴)
23	1, 7, 8	hlatjcl 39343	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
24	3, 6, 22, 23	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
25		simp33 1211	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ 𝐴)
26	1, 8	atbase 39265	. . . . 5 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ (Base‘𝐾))
28	1, 19	latmcl 18455	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))
29	4, 24, 27, 28	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))
30	1, 7, 8	hlatjcl 39343	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
31	3, 22, 5, 30	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
32	1, 7, 8	hlatjcl 39343	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
33	3, 25, 16, 32	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
34	1, 19	latmcl 18455	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))
35	4, 31, 33, 34	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))
36	1, 7	latjcl 18454	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
37	4, 29, 35, 36	syl3anc 1372	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
38	1, 7, 8	hlatjcl 39343	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
39	3, 11, 25, 38	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
40	1, 19	latmcl 18455	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾))
41	4, 24, 39, 40	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾))
42	1, 7	latjcl 18454	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
43	4, 41, 35, 42	syl3anc 1372	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
44	1, 8	atbase 39265	. . . . . . . 8 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
45	5, 44	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ∈ (Base‘𝐾))
46	1, 7, 8	hlatjcl 39343	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
47	3, 5, 16, 46	syl3anc 1372	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
48	1, 7, 8	hlatjcl 39343	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
49	3, 6, 11, 48	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
50	1, 19	latmcl 18455	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
51	4, 24, 49, 50	syl3anc 1372	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
52	1, 19	latmcl 18455	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾))
53	4, 47, 51, 52	syl3anc 1372	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾))
54	1, 7	latjcl 18454	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ∈ (Base‘𝐾))
55	4, 45, 53, 54	syl3anc 1372	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ∈ (Base‘𝐾))
56	1, 8	atbase 39265	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
57	22, 56	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ∈ (Base‘𝐾))
58	1, 7	latjcl 18454	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾))
59	4, 57, 29, 58	syl3anc 1372	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾))
60	1, 7	latjcl 18454	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) ∈ (Base‘𝐾))
61	4, 45, 59, 60	syl3anc 1372	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) ∈ (Base‘𝐾))
62	1, 2, 7, 19	latmlej22 18496	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ 𝑆))
63	4, 18, 15, 45, 62	syl13anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ 𝑆))
64	1, 19	latmcl 18455	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
65	4, 49, 47, 64	syl3anc 1372	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
66	1, 7	latjcl 18454	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ∈ (Base‘𝐾))
67	4, 45, 65, 66	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ∈ (Base‘𝐾))
68	1, 7	latjcl 18454	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾))
69	4, 45, 51, 68	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾))
70	2, 7, 8	hlatlej2 39352	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → 𝑆 ≤ (𝑃 ∨ 𝑆))
71	3, 5, 16, 70	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ≤ (𝑃 ∨ 𝑆))
72	1, 7	latjcl 18454	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
73	4, 45, 49, 72	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
74	1, 2, 19	latmlem2 18485	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))) → (𝑆 ≤ (𝑃 ∨ 𝑆) → ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ 𝑆) ≤ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆))))
75	4, 18, 47, 73, 74	syl13anc 1373	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑆 ≤ (𝑃 ∨ 𝑆) → ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ 𝑆) ≤ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆))))
76	71, 75	mpd 15	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ 𝑆) ≤ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
77	7, 8	hlatjass 39346	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
78	3, 5, 6, 11, 77	syl13anc 1373	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
79	78	oveq1d 7428	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ 𝑆))
80	2, 7, 8	hlatlej1 39351	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑆))
81	3, 5, 16, 80	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ≤ (𝑃 ∨ 𝑆))
82	1, 2, 7, 19, 8	atmod1i1 39834	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑆)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
83	3, 5, 49, 47, 81, 82	syl131anc 1384	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
84	76, 79, 83	3brtr4d 5155	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))))
85	1, 19	latmcom 18478	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
86	4, 49, 47, 85	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
87		simp12 1204	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅))
88	86, 87	eqbrtrd 5145	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑅))
89	1, 2, 19	latmle1 18479	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇))
90	4, 49, 47, 89	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇))
91	1, 2, 19	latlem12 18481	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))) → ((((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) ↔ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))
92	4, 65, 24, 49, 91	syl13anc 1373	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) ↔ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))
93	88, 90, 92	mpbi2and 712	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))
94	1, 2, 7	latjlej2 18469	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
95	4, 65, 51, 45, 94	syl13anc 1373	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
96	93, 95	mpd 15	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))
97	1, 2, 4, 21, 67, 69, 84, 96	lattrd 18461	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))
98	1, 2, 19	latlem12 18481	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾))) → (((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ 𝑆) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))))
99	4, 21, 47, 69, 98	syl13anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ 𝑆) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))))))
100	63, 97, 99	mpbi2and 712	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
101	1, 2, 7, 19, 8	atmod3i1 39841	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑆)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
102	3, 5, 47, 51, 81, 101	syl131anc 1384	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
103	100, 102	breqtrrd 5151	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))))
104		simp13 1205	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈))
105	1, 19	latmcl 18455	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
106	4, 47, 49, 105	syl3anc 1372	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
107	1, 7, 8	hlatjcl 39343	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))
108	3, 22, 25, 107	syl3anc 1372	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))
109	1, 2, 19	latmlem2 18485	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈))))
110	4, 106, 108, 24, 109	syl13anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈))))
111	104, 110	mpd 15	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
112		hlol 39337	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
113	3, 112	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ OL)
114	1, 19	latm12 39206	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ ((𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))) → ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) = ((𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))))
115	113, 47, 24, 49, 114	syl13anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) = ((𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))))
116	2, 7, 8	hlatlej2 39352	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → 𝑅 ≤ (𝑄 ∨ 𝑅))
117	3, 6, 22, 116	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ≤ (𝑄 ∨ 𝑅))
118	1, 2, 7, 19, 8	atmod3i1 39841	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑅)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) = ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
119	3, 22, 24, 27, 117, 118	syl131anc 1384	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) = ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
120	111, 115, 119	3brtr4d 5155	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))
121	1, 2, 7	latjlej2 18469	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ∈ (Base‘𝐾) ∧ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))))
122	4, 53, 59, 45, 121	syl13anc 1373	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇))) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))))
123	120, 122	mpd 15	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑄 ∨ 𝑇)))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))))
124	1, 2, 4, 21, 55, 61, 103, 123	lattrd 18461	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))))
125	1, 7	latj13 18501	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) = (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
126	4, 45, 57, 29, 125	syl13anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) = (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
127	124, 126	breqtrd 5149	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
128	1, 2, 7, 19	latmlej22 18496	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆))
129	4, 18, 15, 27, 128	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆))
130	1, 7	latjcl 18454	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾))
131	4, 29, 31, 130	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾))
132	1, 2, 19	latlem12 18481	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Base‘𝐾) ∧ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))) → (((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆)) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆))))
133	4, 21, 131, 33, 132	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆)) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆))))
134	127, 129, 133	mpbi2and 712	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
135	1, 2, 7, 19	latmlej21 18495	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆))
136	4, 27, 24, 18, 135	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆))
137	1, 2, 7, 19, 8	atmod1i1m 39835	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) ∧ ((𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾)) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) = ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
138	3, 25, 24, 31, 33, 136, 137	syl231anc 1391	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) = ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
139	134, 138	breqtrrd 5151	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
140	2, 7, 8	hlatlej2 39352	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → 𝑈 ≤ (𝑇 ∨ 𝑈))
141	3, 11, 25, 140	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ≤ (𝑇 ∨ 𝑈))
142	1, 2, 19	latmlem2 18485	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑈 ≤ (𝑇 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))))
143	4, 27, 39, 24, 142	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ≤ (𝑇 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))))
144	141, 143	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)))
145	1, 2, 7	latjlej1 18468	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))))
146	4, 29, 41, 35, 145	syl13anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))))
147	144, 146	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
148	1, 2, 4, 21, 37, 43, 139, 147	lattrd 18461	1 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   class class class wbr 5123  ‘cfv 6541  (class class class)co 7413  Basecbs 17230  lecple 17281  joincjn 18328  meetcmee 18329  Latclat 18446  OLcol 39150  Atomscatm 39239  HLchlt 39326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-proset 18311  df-poset 18330  df-plt 18345  df-lub 18361  df-glb 18362  df-join 18363  df-meet 18364  df-p0 18440  df-lat 18447  df-clat 18514  df-oposet 39152  df-ol 39154  df-oml 39155  df-covers 39242  df-ats 39243  df-atl 39274  df-cvlat 39298  df-hlat 39327  df-psubsp 39480  df-pmap 39481  df-padd 39773

This theorem is referenced by:  dalawlem8  39855