Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalawlem11 Structured version   Visualization version   GIF version
Theorem dalawlem11 39409
Description: Lemma for dalaw 39414. First part of dalawlem13 39411. (Contributed by NM, 17-Sep-2012.)
Hypotheses
Ref Expression
dalawlem.l ≀ = (leβ€˜πΎ)
dalawlem.j ∨ = (joinβ€˜πΎ)
dalawlem.m ∧ = (meetβ€˜πΎ)
dalawlem.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
dalawlem11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
Proof of Theorem dalawlem11
StepHypRef Expression
1 eqid 2725 . . . 4 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2 dalawlem.l . . . 4 ≀ = (leβ€˜πΎ)
3 simp11 1200 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ HL)
43hllatd 38891 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
5 simp21 1203 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
6 simp22 1204 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
7 dalawlem.j . . . . . . 7 ∨ = (joinβ€˜πΎ)
8 dalawlem.a . . . . . . 7 𝐴 = (Atomsβ€˜πΎ)
91, 7, 8hlatjcl 38894 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
103, 5, 6, 9syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
11 simp31 1206 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ∈ 𝐴)
12 simp32 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ∈ 𝐴)
131, 7, 8hlatjcl 38894 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
143, 11, 12, 13syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
15 dalawlem.m . . . . . 6 ∧ = (meetβ€˜πΎ)
161, 15latmcl 18429 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
174, 10, 14, 16syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
18 simp23 1205 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ∈ 𝐴)
191, 7, 8hlatjcl 38894 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
203, 6, 18, 19syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
211, 2, 15latmle1 18453 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑃 ∨ 𝑄))
224, 10, 14, 21syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑃 ∨ 𝑄))
23 simp12 1201 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ≀ (𝑄 ∨ 𝑅))
241, 8atbase 38816 . . . . . . 7 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
256, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
261, 8atbase 38816 . . . . . . 7 (𝑅 ∈ 𝐴 β†’ 𝑅 ∈ (Baseβ€˜πΎ))
2718, 26syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ∈ (Baseβ€˜πΎ))
281, 2, 7latlej1 18437 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑅 ∈ (Baseβ€˜πΎ)) β†’ 𝑄 ≀ (𝑄 ∨ 𝑅))
294, 25, 27, 28syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ≀ (𝑄 ∨ 𝑅))
301, 8atbase 38816 . . . . . . 7 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
315, 30syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
321, 2, 7latjle12 18439 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑄 ∨ 𝑅) ∧ 𝑄 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅)))
334, 31, 25, 20, 32syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑄 ∨ 𝑅) ∧ 𝑄 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅)))
3423, 29, 33mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅))
351, 2, 4, 17, 10, 20, 22, 34lattrd 18435 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅))
361, 8atbase 38816 . . . . . . . 8 (𝑇 ∈ 𝐴 β†’ 𝑇 ∈ (Baseβ€˜πΎ))
3712, 36syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ∈ (Baseβ€˜πΎ))
381, 7latjcl 18428 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
394, 10, 37, 38syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
401, 15latmcl 18429 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
414, 39, 14, 40syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
421, 7, 8hlatjcl 38894 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) β†’ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ))
433, 18, 5, 42syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ))
44 simp33 1208 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ∈ 𝐴)
451, 7, 8hlatjcl 38894 . . . . . . . . 9 ((𝐾 ∈ HL ∧ π‘ˆ ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))
463, 44, 11, 45syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))
471, 15latmcl 18429 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
484, 43, 46, 47syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
491, 8atbase 38816 . . . . . . . 8 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
5044, 49syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
511, 7latjcl 18428 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
524, 48, 50, 51syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
531, 7latjcl 18428 . . . . . 6 ((𝐾 ∈ Lat ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
544, 52, 37, 53syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
551, 2, 7latlej1 18437 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
564, 10, 37, 55syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
571, 2, 15latmlem1 18458 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇))))
584, 10, 39, 14, 57syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇))))
5956, 58mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
601, 2, 7latlej2 18438 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
614, 10, 37, 60syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
621, 2, 7, 15, 8atmod2i2 39390 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
633, 11, 39, 37, 61, 62syl131anc 1380 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
641, 7, 8hlatjcl 38894 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) β†’ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
653, 6, 12, 64syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
661, 7, 8hlatjcl 38894 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
673, 5, 11, 66syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
681, 15latmcom 18452 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
694, 65, 67, 68syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
70 simp13 1202 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ))
7169, 70eqbrtrd 5165 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ))
721, 15latmcl 18429 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
734, 65, 67, 72syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
741, 7, 8hlatjcl 38894 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
753, 18, 44, 74syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
761, 2, 7latjlej2 18443 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ))) β†’ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ))))
774, 73, 75, 31, 76syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ))))
7871, 77mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
791, 8atbase 38816 . . . . . . . . . . . . 13 (𝑆 ∈ 𝐴 β†’ 𝑆 ∈ (Baseβ€˜πΎ))
8011, 79syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ∈ (Baseβ€˜πΎ))
811, 2, 7latlej1 18437 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑃 ≀ (𝑃 ∨ 𝑆))
824, 31, 80, 81syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ≀ (𝑃 ∨ 𝑆))
831, 2, 7, 15, 8atmod1i1 39385 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) ∧ 𝑃 ≀ (𝑃 ∨ 𝑆)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
843, 5, 65, 67, 82, 83syl131anc 1380 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
857, 8hlatjass 38897 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
863, 5, 18, 44, 85syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
877, 8hlatjcom 38895 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
883, 5, 18, 87syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
8988oveq1d 7430 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
9086, 89eqtr3d 2767 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑅 ∨ π‘ˆ)) = ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
9178, 84, 903brtr3d 5174 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
921, 2, 7latlej2 18438 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑆 ≀ (π‘ˆ ∨ 𝑆))
934, 50, 80, 92syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ≀ (π‘ˆ ∨ 𝑆))
941, 7latjcl 18428 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
954, 31, 65, 94syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
961, 15latmcl 18429 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
974, 95, 67, 96syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
981, 7latjcl 18428 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
994, 43, 50, 98syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1001, 2, 15latmlem12 18460 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) ∧ (𝑆 ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ 𝑆 ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆))))
1014, 97, 99, 80, 46, 100syl122anc 1376 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ 𝑆 ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆))))
10291, 93, 101mp2and 697 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
103 hlol 38888 . . . . . . . . . . 11 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
1043, 103syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ OL)
1051, 15latmassOLD 38756 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ))) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)))
106104, 95, 67, 80, 105syl13anc 1369 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)))
1077, 8hlatjass 38897 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
1083, 5, 6, 12, 107syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
109108eqcomd 2731 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) = ((𝑃 ∨ 𝑄) ∨ 𝑇))
1101, 2, 7latlej2 18438 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑆 ≀ (𝑃 ∨ 𝑆))
1114, 31, 80, 110syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ≀ (𝑃 ∨ 𝑆))
1121, 2, 15latleeqm2 18457 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ (𝑆 ≀ (𝑃 ∨ 𝑆) ↔ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆))
1134, 80, 67, 112syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑆 ≀ (𝑃 ∨ 𝑆) ↔ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆))
114111, 113mpbid 231 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆)
115109, 114oveq12d 7433 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆))
116106, 115eqtr2d 2766 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) = (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆))
1171, 2, 7latlej1 18437 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ π‘ˆ ≀ (π‘ˆ ∨ 𝑆))
1184, 50, 80, 117syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ≀ (π‘ˆ ∨ 𝑆))
1191, 2, 7, 15, 8atmod4i1 39394 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) = (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
1203, 44, 43, 46, 118, 119syl131anc 1380 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) = (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
121102, 116, 1203brtr4d 5175 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ))
1221, 15latmcl 18429 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ))
1234, 39, 80, 122syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ))
1241, 2, 7latjlej1 18442 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ) ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇)))
1254, 123, 52, 37, 124syl13anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇)))
126121, 125mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
12763, 126eqbrtrrd 5167 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
1281, 2, 4, 17, 41, 54, 59, 127lattrd 18435 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
1291, 7latj31 18476 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ))) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) = ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
1304, 48, 50, 37, 129syl13anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) = ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
131128, 130breqtrd 5169 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
1321, 7, 8hlatjcl 38894 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1333, 12, 44, 132syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1341, 7latjcl 18428 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ)) β†’ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))
1354, 133, 48, 134syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))
1361, 2, 15latlem12 18455 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))) ↔ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))))
1374, 17, 20, 135, 136syl13anc 1369 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))) ↔ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))))
13835, 131, 137mpbi2and 710 . 2 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
1391, 2, 15latmle1 18453 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑅 ∨ 𝑃))
1404, 43, 46, 139syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑅 ∨ 𝑃))
1411, 2, 7latlej2 18438 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑅 ∈ (Baseβ€˜πΎ)) β†’ 𝑅 ≀ (𝑄 ∨ 𝑅))
1424, 25, 27, 141syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ≀ (𝑄 ∨ 𝑅))
1431, 2, 7latjle12 18439 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑅 ≀ (𝑄 ∨ 𝑅) ∧ 𝑃 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅)))
1444, 27, 31, 20, 143syl13anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ≀ (𝑄 ∨ 𝑅) ∧ 𝑃 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅)))
145142, 23, 144mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅))
1461, 2, 4, 48, 43, 20, 140, 145lattrd 18435 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑄 ∨ 𝑅))
1471, 2, 7, 15, 8llnmod2i2 39391 . . 3 (((𝐾 ∈ HL ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ)) ∧ (𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑄 ∨ 𝑅)) β†’ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) = ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
1483, 20, 48, 12, 44, 146, 147syl321anc 1389 . 2 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) = ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
149138, 148breqtrrd 5171 1 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   class class class wbr 5143  β€˜cfv 6542  (class class class)co 7415  Basecbs 17177  lecple 17237  joincjn 18300  meetcmee 18301  Latclat 18420  OLcol 38701  Atomscatm 38790  HLchlt 38877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-1st 7989  df-2nd 7990  df-proset 18284  df-poset 18302  df-plt 18319  df-lub 18335  df-glb 18336  df-join 18337  df-meet 18338  df-p0 18414  df-lat 18421  df-clat 18488  df-oposet 38703  df-ol 38705  df-oml 38706  df-covers 38793  df-ats 38794  df-atl 38825  df-cvlat 38849  df-hlat 38878  df-psubsp 39031  df-pmap 39032  df-padd 39324
This theorem is referenced by:  dalawlem13  39411
  Copyright terms: Public domain W3C validator