Theorem dalawlem3 40365

Description: Lemma for dalaw 40378. First piece of dalawlem5 40367. (Contributed by NM, 4-Oct-2012.)

Hypotheses

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

Assertion

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

Proof of Theorem dalawlem3

Step	Hyp	Ref	Expression
1		eqid 2739	. 2 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		dalawlem.l	. 2 ⊢ ≤ = (le‘𝐾)
3		simp11 1210	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ HL)
4	3	hllatd 39856	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ Lat)
5		simp22 1214	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
6		simp32 1217	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑇 ∈ 𝐴)
7		dalawlem.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
8		dalawlem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9	1, 7, 8	hlatjcl 39859	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
10	3, 5, 6, 9	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
11		simp21 1213	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
12	1, 8	atbase 39781	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
13	11, 12	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ∈ (Base‘𝐾))
14	1, 7	latjcl 18396	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾))
15	4, 10, 13, 14	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾))
16		simp31 1216	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ∈ 𝐴)
17	1, 8	atbase 39781	. . . 4 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
18	16, 17	syl 17	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ∈ (Base‘𝐾))
19		dalawlem.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
20	1, 19	latmcl 18397	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ∈ (Base‘𝐾))
21	4, 15, 18, 20	syl3anc 1379	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ∈ (Base‘𝐾))
22		simp23 1215	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ∈ 𝐴)
23	1, 7, 8	hlatjcl 39859	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
24	3, 5, 22, 23	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
25		simp33 1218	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ 𝐴)
26	1, 8	atbase 39781	. . . . 5 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ (Base‘𝐾))
28	1, 19	latmcl 18397	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))
29	4, 24, 27, 28	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))
30	1, 7, 8	hlatjcl 39859	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
31	3, 22, 11, 30	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
32	1, 7, 8	hlatjcl 39859	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
33	3, 25, 16, 32	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
34	1, 19	latmcl 18397	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))
35	4, 31, 33, 34	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))
36	1, 7	latjcl 18396	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
37	4, 29, 35, 36	syl3anc 1379	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
38	1, 7, 8	hlatjcl 39859	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
39	3, 6, 25, 38	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
40	1, 19	latmcl 18397	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾))
41	4, 24, 39, 40	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾))
42	1, 7	latjcl 18396	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
43	4, 41, 35, 42	syl3anc 1379	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ∈ (Base‘𝐾))
44	1, 8	atbase 39781	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
45	5, 44	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ∈ (Base‘𝐾))
46	1, 19	latmcl 18397	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝑄 ∧ 𝑈) ∈ (Base‘𝐾))
47	4, 45, 27, 46	syl3anc 1379	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∧ 𝑈) ∈ (Base‘𝐾))
48	1, 7, 8	hlatjcl 39859	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
49	3, 11, 16, 48	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
50	1, 19	latmcl 18397	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾))
51	4, 49, 45, 50	syl3anc 1379	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾))
52	1, 7	latjcl 18396	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∧ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾))
53	4, 47, 51, 52	syl3anc 1379	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾))
54	1, 7	latjcl 18396	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ∈ (Base‘𝐾))
55	4, 13, 53, 54	syl3anc 1379	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ∈ (Base‘𝐾))
56	1, 8	atbase 39781	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
57	22, 56	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ∈ (Base‘𝐾))
58	1, 7	latjcl 18396	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾))
59	4, 57, 29, 58	syl3anc 1379	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾))
60	1, 7	latjcl 18396	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) ∈ (Base‘𝐾))
61	4, 13, 59, 60	syl3anc 1379	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) ∈ (Base‘𝐾))
62	1, 7	latjcl 18396	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∧ 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → ((𝑄 ∧ 𝑈) ∨ 𝑃) ∈ (Base‘𝐾))
63	4, 47, 13, 62	syl3anc 1379	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ 𝑃) ∈ (Base‘𝐾))
64	1, 2, 7, 19	latmlej22 18438	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾) ∧ ((𝑄 ∧ 𝑈) ∨ 𝑃) ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∧ 𝑈) ∨ 𝑃) ∨ 𝑆))
65	4, 18, 15, 63, 64	syl13anc 1380	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∧ 𝑈) ∨ 𝑃) ∨ 𝑆))
66	1, 7	latjass 18440	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∧ 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (((𝑄 ∧ 𝑈) ∨ 𝑃) ∨ 𝑆) = ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)))
67	4, 47, 13, 18, 66	syl13anc 1380	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∧ 𝑈) ∨ 𝑃) ∨ 𝑆) = ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)))
68	65, 67	breqtrd 5098	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)))
69	1, 19	latmcl 18397	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
70	4, 10, 49, 69	syl3anc 1379	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
71	1, 7	latjcl 18396	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) ∈ (Base‘𝐾))
72	4, 70, 13, 71	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) ∈ (Base‘𝐾))
73	1, 7, 8	hlatjcl 39859	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
74	3, 11, 5, 73	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
75	2, 7, 8	hlatlej2 39868	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → 𝑆 ≤ (𝑃 ∨ 𝑆))
76	3, 11, 16, 75	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ≤ (𝑃 ∨ 𝑆))
77	1, 2, 19	latmlem2 18427	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾))) → (𝑆 ≤ (𝑃 ∨ 𝑆) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ (𝑃 ∨ 𝑆))))
78	4, 18, 49, 15, 77	syl13anc 1380	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑆 ≤ (𝑃 ∨ 𝑆) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ (𝑃 ∨ 𝑆))))
79	76, 78	mpd 15	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ (𝑃 ∨ 𝑆)))
80	2, 7, 8	hlatlej1 39867	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑆))
81	3, 11, 16, 80	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ≤ (𝑃 ∨ 𝑆))
82	1, 2, 7, 19, 8	atmod4i1 40358	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑆)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) = (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ (𝑃 ∨ 𝑆)))
83	3, 11, 10, 49, 81, 82	syl131anc 1391	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) = (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ (𝑃 ∨ 𝑆)))
84	79, 83	breqtrrd 5100	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃))
85	1, 19	latmcom 18420	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
86	4, 10, 49, 85	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
87		simp12 1211	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄))
88	86, 87	eqbrtrd 5094	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑄))
89	2, 7, 8	hlatlej1 39867	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))
90	3, 11, 5, 89	syl3anc 1379	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ≤ (𝑃 ∨ 𝑄))
91	1, 2, 7	latjle12 18407	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄)) ↔ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) ≤ (𝑃 ∨ 𝑄)))
92	4, 70, 13, 74, 91	syl13anc 1380	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄)) ↔ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) ≤ (𝑃 ∨ 𝑄)))
93	88, 90, 92	mpbi2and 718	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∨ 𝑃) ≤ (𝑃 ∨ 𝑄))
94	1, 2, 4, 21, 72, 74, 84, 93	lattrd 18403	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑃 ∨ 𝑄))
95	1, 7	latjcl 18396	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∧ 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
96	4, 47, 49, 95	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
97	1, 2, 19	latlem12 18423	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → (((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑃 ∨ 𝑄)) ↔ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄))))
98	4, 21, 96, 74, 97	syl13anc 1380	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑃 ∨ 𝑄)) ↔ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄))))
99	68, 94, 98	mpbi2and 718	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄)))
100	1, 2, 7, 19, 8	atmod3i1 40356	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑆)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑄)))
101	3, 11, 49, 45, 81, 100	syl131anc 1391	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑄)))
102	101	oveq2d 7372	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) = ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑄))))
103	1, 7	latj12 18441	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∧ 𝑈) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾))) → ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) = (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
104	4, 47, 13, 51, 103	syl13anc 1380	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) = (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
105	1, 2, 7, 19	latmlej12 18436	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (𝑄 ∧ 𝑈) ≤ (𝑃 ∨ 𝑄))
106	4, 45, 27, 13, 105	syl13anc 1380	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∧ 𝑈) ≤ (𝑃 ∨ 𝑄))
107	1, 2, 7, 19, 8	atmod1i1m 40350	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) ∧ (𝑄 ∧ 𝑈) ≤ (𝑃 ∨ 𝑄)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑄))) = (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄)))
108	3, 25, 45, 49, 74, 106, 107	syl231anc 1398	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑄))) = (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄)))
109	102, 104, 108	3eqtr3rd 2783	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∧ 𝑈) ∨ (𝑃 ∨ 𝑆)) ∧ (𝑃 ∨ 𝑄)) = (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
110	99, 109	breqtrd 5098	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
111	2, 7, 8	hlatlej1 39867	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑅))
112	3, 5, 22, 111	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ≤ (𝑄 ∨ 𝑅))
113	2, 7, 8	hlatlej2 39868	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → 𝑈 ≤ (𝑅 ∨ 𝑈))
114	3, 22, 25, 113	syl3anc 1379	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ≤ (𝑅 ∨ 𝑈))
115	1, 19	latmcl 18397	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
116	4, 49, 10, 115	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))
117	1, 7, 8	hlatjcl 39859	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))
118	3, 22, 25, 117	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))
119	2, 7, 8	hlatlej1 39867	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑇))
120	3, 5, 6, 119	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ≤ (𝑄 ∨ 𝑇))
121	1, 2, 19	latmlem2 18427	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))) → (𝑄 ≤ (𝑄 ∨ 𝑇) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))))
122	4, 45, 10, 49, 121	syl13anc 1380	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ≤ (𝑄 ∨ 𝑇) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇))))
123	120, 122	mpd 15	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
124		simp13 1212	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈))
125	1, 2, 4, 51, 116, 118, 123, 124	lattrd 18403	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ (𝑅 ∨ 𝑈))
126	1, 2, 7	latjle12 18407	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))) → ((𝑈 ≤ (𝑅 ∨ 𝑈) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ (𝑅 ∨ 𝑈)) ↔ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ 𝑈)))
127	4, 27, 51, 118, 126	syl13anc 1380	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑈 ≤ (𝑅 ∨ 𝑈) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ (𝑅 ∨ 𝑈)) ↔ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ 𝑈)))
128	114, 125, 127	mpbi2and 718	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ 𝑈))
129	1, 7	latjcl 18396	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾)) → (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾))
130	4, 27, 51, 129	syl3anc 1379	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾))
131	1, 2, 19	latmlem12 18428	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) ∧ ((𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾))) → ((𝑄 ≤ (𝑄 ∨ 𝑅) ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ 𝑈)) → (𝑄 ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈))))
132	4, 45, 24, 130, 118, 131	syl122anc 1387	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ≤ (𝑄 ∨ 𝑅) ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ 𝑈)) → (𝑄 ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈))))
133	112, 128, 132	mp2and 705	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
134	1, 2, 19	latmle2 18422	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ 𝑄)
135	4, 49, 45, 134	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ 𝑄)
136	1, 2, 7, 19, 8	atmod2i2 40354	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑈 ∈ 𝐴 ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑄) ≤ 𝑄) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) = (𝑄 ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
137	3, 25, 45, 51, 135, 136	syl131anc 1391	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) = (𝑄 ∧ (𝑈 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))))
138	2, 7, 8	hlatlej2 39868	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → 𝑅 ≤ (𝑄 ∨ 𝑅))
139	3, 5, 22, 138	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ≤ (𝑄 ∨ 𝑅))
140	1, 2, 7, 19, 8	atmod3i2 40357	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑈 ∈ 𝐴 ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑅)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) = ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
141	3, 25, 57, 24, 139, 140	syl131anc 1391	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) = ((𝑄 ∨ 𝑅) ∧ (𝑅 ∨ 𝑈)))
142	133, 137, 141	3brtr4d 5104	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))
143	1, 2, 7	latjlej2 18411	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ∈ (Base‘𝐾) ∧ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → (((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) → (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))))
144	4, 53, 59, 13, 143	syl13anc 1380	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄)) ≤ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)) → (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈)))))
145	142, 144	mpd 15	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ ((𝑄 ∧ 𝑈) ∨ ((𝑃 ∨ 𝑆) ∧ 𝑄))) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))))
146	1, 2, 4, 21, 55, 61, 110, 145	lattrd 18403	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))))
147	1, 7	latj13 18443	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾))) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) = (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
148	4, 13, 57, 29, 147	syl13anc 1380	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ (𝑅 ∨ ((𝑄 ∨ 𝑅) ∧ 𝑈))) = (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
149	146, 148	breqtrd 5098	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)))
150	1, 2, 7, 19	latmlej22 18438	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑇) ∨ 𝑃) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆))
151	4, 18, 15, 27, 150	syl13anc 1380	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆))
152	1, 7	latjcl 18396	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾))
153	4, 29, 31, 152	syl3anc 1379	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾))
154	1, 2, 19	latlem12 18423	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ ((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ∈ (Base‘𝐾) ∧ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))) → (((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆)) ↔ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆))))
155	4, 21, 153, 33, 154	syl13anc 1380	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (𝑈 ∨ 𝑆)) ↔ (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆))))
156	149, 151, 155	mpbi2and 718	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
157	1, 2, 7, 19	latmlej21 18437	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆))
158	4, 27, 24, 18, 157	syl13anc 1380	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆))
159	1, 2, 7, 19, 8	atmod1i1m 40350	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) ∧ ((𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾)) ∧ ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ (𝑈 ∨ 𝑆)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) = ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
160	3, 25, 24, 31, 33, 158, 159	syl231anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) = ((((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ (𝑅 ∨ 𝑃)) ∧ (𝑈 ∨ 𝑆)))
161	156, 160	breqtrrd 5100	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
162	2, 7, 8	hlatlej2 39868	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → 𝑈 ≤ (𝑇 ∨ 𝑈))
163	3, 6, 25, 162	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ≤ (𝑇 ∨ 𝑈))
164	1, 2, 19	latmlem2 18427	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑈 ≤ (𝑇 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))))
165	4, 27, 39, 24, 164	syl13anc 1380	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ≤ (𝑇 ∨ 𝑈) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))))
166	163, 165	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)))
167	1, 2, 7	latjlej1 18410	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑅) ∧ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∈ (Base‘𝐾) ∧ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))))
168	4, 29, 41, 35, 167	syl13anc 1380	. . 3 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ≤ ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))))
169	166, 168	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ 𝑈) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
170	1, 2, 4, 21, 37, 43, 161, 169	lattrd 18403	1 ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   class class class wbr 5072  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  lecple 17218  joincjn 18268  meetcmee 18269  Latclat 18388  Atomscatm 39755  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-proset 18251  df-poset 18270  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-lat 18389  df-clat 18456  df-oposet 39668  df-ol 39670  df-oml 39671  df-covers 39758  df-ats 39759  df-atl 39790  df-cvlat 39814  df-hlat 39843  df-psubsp 39995  df-pmap 39996  df-padd 40288

This theorem is referenced by:  dalawlem4  40366  dalawlem5  40367