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 38740
Description: Lemma for dalaw 38745. First part of dalawlem13 38742. (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 2732 . . . 4 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2 dalawlem.l . . . 4 ≀ = (leβ€˜πΎ)
3 simp11 1203 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ HL)
43hllatd 38222 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
5 simp21 1206 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
6 simp22 1207 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
7 dalawlem.j . . . . . . 7 ∨ = (joinβ€˜πΎ)
8 dalawlem.a . . . . . . 7 𝐴 = (Atomsβ€˜πΎ)
91, 7, 8hlatjcl 38225 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
103, 5, 6, 9syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
11 simp31 1209 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ∈ 𝐴)
12 simp32 1210 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ∈ 𝐴)
131, 7, 8hlatjcl 38225 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
143, 11, 12, 13syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
15 dalawlem.m . . . . . 6 ∧ = (meetβ€˜πΎ)
161, 15latmcl 18389 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
174, 10, 14, 16syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
18 simp23 1208 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ∈ 𝐴)
191, 7, 8hlatjcl 38225 . . . . 5 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
203, 6, 18, 19syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))
211, 2, 15latmle1 18413 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑃 ∨ 𝑄))
224, 10, 14, 21syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑃 ∨ 𝑄))
23 simp12 1204 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ≀ (𝑄 ∨ 𝑅))
241, 8atbase 38147 . . . . . . 7 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
256, 24syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
261, 8atbase 38147 . . . . . . 7 (𝑅 ∈ 𝐴 β†’ 𝑅 ∈ (Baseβ€˜πΎ))
2718, 26syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ∈ (Baseβ€˜πΎ))
281, 2, 7latlej1 18397 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑅 ∈ (Baseβ€˜πΎ)) β†’ 𝑄 ≀ (𝑄 ∨ 𝑅))
294, 25, 27, 28syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑄 ≀ (𝑄 ∨ 𝑅))
301, 8atbase 38147 . . . . . . 7 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
315, 30syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
321, 2, 7latjle12 18399 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑄 ∨ 𝑅) ∧ 𝑄 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅)))
334, 31, 25, 20, 32syl13anc 1372 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ≀ (𝑄 ∨ 𝑅) ∧ 𝑄 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅)))
3423, 29, 33mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ≀ (𝑄 ∨ 𝑅))
351, 2, 4, 17, 10, 20, 22, 34lattrd 18395 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅))
361, 8atbase 38147 . . . . . . . 8 (𝑇 ∈ 𝐴 β†’ 𝑇 ∈ (Baseβ€˜πΎ))
3712, 36syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ∈ (Baseβ€˜πΎ))
381, 7latjcl 18388 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
394, 10, 37, 38syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
401, 15latmcl 18389 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
414, 39, 14, 40syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
421, 7, 8hlatjcl 38225 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) β†’ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ))
433, 18, 5, 42syl3anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ))
44 simp33 1211 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ∈ 𝐴)
451, 7, 8hlatjcl 38225 . . . . . . . . 9 ((𝐾 ∈ HL ∧ π‘ˆ ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))
463, 44, 11, 45syl3anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))
471, 15latmcl 18389 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
484, 43, 46, 47syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
491, 8atbase 38147 . . . . . . . 8 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
5044, 49syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
511, 7latjcl 18388 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
524, 48, 50, 51syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
531, 7latjcl 18388 . . . . . 6 ((𝐾 ∈ Lat ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
544, 52, 37, 53syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) ∈ (Baseβ€˜πΎ))
551, 2, 7latlej1 18397 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
564, 10, 37, 55syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
571, 2, 15latmlem1 18418 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇))))
584, 10, 39, 14, 57syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇))))
5956, 58mpd 15 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
601, 2, 7latlej2 18398 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
614, 10, 37, 60syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇))
621, 2, 7, 15, 8atmod2i2 38721 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑇)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
633, 11, 39, 37, 61, 62syl131anc 1383 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)))
641, 7, 8hlatjcl 38225 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) β†’ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
653, 6, 12, 64syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
661, 7, 8hlatjcl 38225 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
673, 5, 11, 66syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ))
681, 15latmcom 18412 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
694, 65, 67, 68syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
70 simp13 1205 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ))
7169, 70eqbrtrd 5169 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ))
721, 15latmcl 18389 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
734, 65, 67, 72syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
741, 7, 8hlatjcl 38225 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
753, 18, 44, 74syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
761, 2, 7latjlej2 18403 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ (𝑅 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ))) β†’ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ))))
774, 73, 75, 31, 76syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≀ (𝑅 ∨ π‘ˆ) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ))))
7871, 77mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) ≀ (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
791, 8atbase 38147 . . . . . . . . . . . . 13 (𝑆 ∈ 𝐴 β†’ 𝑆 ∈ (Baseβ€˜πΎ))
8011, 79syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ∈ (Baseβ€˜πΎ))
811, 2, 7latlej1 18397 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑃 ≀ (𝑃 ∨ 𝑆))
824, 31, 80, 81syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑃 ≀ (𝑃 ∨ 𝑆))
831, 2, 7, 15, 8atmod1i1 38716 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) ∧ 𝑃 ≀ (𝑃 ∨ 𝑆)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
843, 5, 65, 67, 82, 83syl131anc 1383 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)))
857, 8hlatjass 38228 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
863, 5, 18, 44, 85syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = (𝑃 ∨ (𝑅 ∨ π‘ˆ)))
877, 8hlatjcom 38226 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
883, 5, 18, 87syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
8988oveq1d 7420 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∨ π‘ˆ) = ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
9086, 89eqtr3d 2774 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑅 ∨ π‘ˆ)) = ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
9178, 84, 903brtr3d 5178 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ))
921, 2, 7latlej2 18398 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑆 ≀ (π‘ˆ ∨ 𝑆))
934, 50, 80, 92syl3anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ≀ (π‘ˆ ∨ 𝑆))
941, 7latjcl 18388 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑇) ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
954, 31, 65, 94syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ))
961, 15latmcl 18389 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
974, 95, 67, 96syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ))
981, 7latjcl 18388 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
994, 43, 50, 98syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1001, 2, 15latmlem12 18420 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) ∧ (𝑆 ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ 𝑆 ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆))))
1014, 97, 99, 80, 46, 100syl122anc 1379 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ≀ ((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ 𝑆 ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆))))
10291, 93, 101mp2and 697 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
103 hlol 38219 . . . . . . . . . . 11 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
1043, 103syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝐾 ∈ OL)
1051, 15latmassOLD 38087 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ))) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)))
106104, 95, 67, 80, 105syl13anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆) = ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)))
1077, 8hlatjass 38228 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
1083, 5, 6, 12, 107syl13anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑇) = (𝑃 ∨ (𝑄 ∨ 𝑇)))
109108eqcomd 2738 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑃 ∨ (𝑄 ∨ 𝑇)) = ((𝑃 ∨ 𝑄) ∨ 𝑇))
1101, 2, 7latlej2 18398 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ 𝑆 ≀ (𝑃 ∨ 𝑆))
1114, 31, 80, 110syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑆 ≀ (𝑃 ∨ 𝑆))
1121, 2, 15latleeqm2 18417 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ (𝑆 ≀ (𝑃 ∨ 𝑆) ↔ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆))
1134, 80, 67, 112syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑆 ≀ (𝑃 ∨ 𝑆) ↔ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆))
114111, 113mpbid 231 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑆) ∧ 𝑆) = 𝑆)
115109, 114oveq12d 7423 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑆)) = (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆))
116106, 115eqtr2d 2773 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) = (((𝑃 ∨ (𝑄 ∨ 𝑇)) ∧ (𝑃 ∨ 𝑆)) ∧ 𝑆))
1171, 2, 7latlej1 18397 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ π‘ˆ ≀ (π‘ˆ ∨ 𝑆))
1184, 50, 80, 117syl3anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ π‘ˆ ≀ (π‘ˆ ∨ 𝑆))
1191, 2, 7, 15, 8atmod4i1 38725 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ (π‘ˆ ∨ 𝑆)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) = (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
1203, 44, 43, 46, 118, 119syl131anc 1383 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) = (((𝑅 ∨ 𝑃) ∨ π‘ˆ) ∧ (π‘ˆ ∨ 𝑆)))
121102, 116, 1203brtr4d 5179 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ))
1221, 15latmcl 18389 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ))
1234, 39, 80, 122syl3anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ))
1241, 2, 7latjlej1 18402 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∈ (Baseβ€˜πΎ) ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇)))
1254, 123, 52, 37, 124syl13anc 1372 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≀ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇)))
126121, 125mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ 𝑇) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
12763, 126eqbrtrrd 5171 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ (𝑆 ∨ 𝑇)) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
1281, 2, 4, 17, 41, 54, 59, 127lattrd 18395 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇))
1291, 7latj31 18436 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ))) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) = ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
1304, 48, 50, 37, 129syl13anc 1372 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∨ π‘ˆ) ∨ 𝑇) = ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
131128, 130breqtrd 5173 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
1321, 7, 8hlatjcl 38225 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1333, 12, 44, 132syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1341, 7latjcl 18388 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ)) β†’ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))
1354, 133, 48, 134syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))
1361, 2, 15latlem12 18415 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))) ↔ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))))
1374, 17, 20, 135, 136syl13anc 1372 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))) ↔ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))))
13835, 131, 137mpbi2and 710 . 2 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
1391, 2, 15latmle1 18413 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Baseβ€˜πΎ) ∧ (π‘ˆ ∨ 𝑆) ∈ (Baseβ€˜πΎ)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑅 ∨ 𝑃))
1404, 43, 46, 139syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑅 ∨ 𝑃))
1411, 2, 7latlej2 18398 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑅 ∈ (Baseβ€˜πΎ)) β†’ 𝑅 ≀ (𝑄 ∨ 𝑅))
1424, 25, 27, 141syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ 𝑅 ≀ (𝑄 ∨ 𝑅))
1431, 2, 7latjle12 18399 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑅 ≀ (𝑄 ∨ 𝑅) ∧ 𝑃 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅)))
1444, 27, 31, 20, 143syl13anc 1372 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ≀ (𝑄 ∨ 𝑅) ∧ 𝑃 ≀ (𝑄 ∨ 𝑅)) ↔ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅)))
145142, 23, 144mpbi2and 710 . . . 4 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (𝑅 ∨ 𝑃) ≀ (𝑄 ∨ 𝑅))
1461, 2, 4, 48, 43, 20, 140, 145lattrd 18395 . . 3 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑄 ∨ 𝑅))
1471, 2, 7, 15, 8llnmod2i2 38722 . . 3 (((𝐾 ∈ HL ∧ (𝑄 ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ∈ (Baseβ€˜πΎ)) ∧ (𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)) ≀ (𝑄 ∨ 𝑅)) β†’ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) = ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
1483, 20, 48, 12, 44, 146, 147syl321anc 1392 . 2 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))) = ((𝑄 ∨ 𝑅) ∧ ((𝑇 ∨ π‘ˆ) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆)))))
149138, 148breqtrrd 5175 1 (((𝐾 ∈ HL ∧ 𝑃 ≀ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≀ (𝑅 ∨ π‘ˆ)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≀ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ π‘ˆ)) ∨ ((𝑅 ∨ 𝑃) ∧ (π‘ˆ ∨ 𝑆))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   class class class wbr 5147  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  lecple 17200  joincjn 18260  meetcmee 18261  Latclat 18380  OLcol 38032  Atomscatm 38121  HLchlt 38208
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-proset 18244  df-poset 18262  df-plt 18279  df-lub 18295  df-glb 18296  df-join 18297  df-meet 18298  df-p0 18374  df-lat 18381  df-clat 18448  df-oposet 38034  df-ol 38036  df-oml 38037  df-covers 38124  df-ats 38125  df-atl 38156  df-cvlat 38180  df-hlat 38209  df-psubsp 38362  df-pmap 38363  df-padd 38655
This theorem is referenced by:  dalawlem13  38742
  Copyright terms: Public domain W3C validator