Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2lplnja Structured version   Visualization version   GIF version
Theorem 2lplnja 38793
Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 38794 in terms of atoms). (Contributed by NM, 12-Jul-2012.)
Hypotheses
Ref Expression
2lplnja.l ≀ = (leβ€˜πΎ)
2lplnja.j ∨ = (joinβ€˜πΎ)
2lplnja.a 𝐴 = (Atomsβ€˜πΎ)
2lplnja.v 𝑉 = (LVolsβ€˜πΎ)
Assertion
Ref Expression
2lplnja ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) = π‘Š)
Proof of Theorem 2lplnja
StepHypRef Expression
1 eqid 2732 . 2 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2 2lplnja.l . 2 ≀ = (leβ€˜πΎ)
3 simp11l 1284 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝐾 ∈ HL)
43hllatd 38537 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝐾 ∈ Lat)
5 simp121 1305 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑃 ∈ 𝐴)
6 simp122 1306 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑄 ∈ 𝐴)
7 2lplnja.j . . . . . 6 ∨ = (joinβ€˜πΎ)
8 2lplnja.a . . . . . 6 𝐴 = (Atomsβ€˜πΎ)
91, 7, 8hlatjcl 38540 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
103, 5, 6, 9syl3anc 1371 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
11 simp123 1307 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑅 ∈ 𝐴)
121, 8atbase 38462 . . . . 5 (𝑅 ∈ 𝐴 β†’ 𝑅 ∈ (Baseβ€˜πΎ))
1311, 12syl 17 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑅 ∈ (Baseβ€˜πΎ))
141, 7latjcl 18396 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑅 ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))
154, 10, 13, 14syl3anc 1371 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))
16 simp2l1 1272 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 ∈ 𝐴)
17 simp2l2 1273 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑇 ∈ 𝐴)
181, 7, 8hlatjcl 38540 . . . . 5 ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
193, 16, 17, 18syl3anc 1371 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ))
20 simp2l3 1274 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘ˆ ∈ 𝐴)
211, 8atbase 38462 . . . . 5 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
2220, 21syl 17 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
231, 7latjcl 18396 . . . 4 ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
244, 19, 22, 23syl3anc 1371 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
251, 7latjcl 18396 . . 3 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) ∈ (Baseβ€˜πΎ))
264, 15, 24, 25syl3anc 1371 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) ∈ (Baseβ€˜πΎ))
27 simp11r 1285 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘Š ∈ 𝑉)
28 2lplnja.v . . . 4 𝑉 = (LVolsβ€˜πΎ)
291, 28lvolbase 38752 . . 3 (π‘Š ∈ 𝑉 β†’ π‘Š ∈ (Baseβ€˜πΎ))
3027, 29syl 17 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘Š ∈ (Baseβ€˜πΎ))
31 simp31 1209 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š)
32 simp32 1210 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š)
331, 2, 7latjle12 18407 . . . 4 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) ≀ π‘Š))
344, 15, 24, 30, 33syl13anc 1372 . . 3 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) ≀ π‘Š))
3531, 32, 34mpbi2and 710 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) ≀ π‘Š)
361, 2, 7latlej2 18406 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ π‘ˆ ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
374, 19, 22, 36syl3anc 1371 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘ˆ ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
381, 2, 4, 22, 24, 30, 37, 32lattrd 18403 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘ˆ ≀ π‘Š)
391, 2, 7latjle12 18407 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ π‘ˆ ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š))
404, 15, 22, 30, 39syl13anc 1372 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ π‘ˆ ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š))
4131, 38, 40mpbi2and 710 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š)
4241ad2antrr 724 . . . . . 6 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š)
433ad2antrr 724 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝐾 ∈ HL)
443, 5, 63jca 1128 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
4544ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
4611, 20jca 512 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴))
4746ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴))
48 simp13l 1288 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑃 β‰  𝑄)
4948ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝑃 β‰  𝑄)
50 simp13r 1289 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))
5150ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))
52 simp33 1211 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
5352ad2antrr 724 . . . . . . . . 9 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
54 simplr 767 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55 simpr 485 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
561, 8atbase 38462 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ 𝐴 β†’ 𝑆 ∈ (Baseβ€˜πΎ))
5716, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 ∈ (Baseβ€˜πΎ))
581, 8atbase 38462 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ 𝐴 β†’ 𝑇 ∈ (Baseβ€˜πΎ))
5917, 58syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑇 ∈ (Baseβ€˜πΎ))
601, 2, 7latjle12 18407 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ ((𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
614, 57, 59, 15, 60syl13anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
6261ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
6354, 55, 62mpbi2and 710 . . . . . . . . . . . . . . 15 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
6463adantr 481 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
65 simpr 485 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
661, 2, 7latjle12 18407 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Lat ∧ ((𝑆 ∨ 𝑇) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ (((𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
674, 19, 22, 15, 66syl13anc 1372 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
6867ad3antrrr 728 . . . . . . . . . . . . . 14 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑆 ∨ 𝑇) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
6964, 65, 68mpbi2and 710 . . . . . . . . . . . . 13 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
70 simp2l 1199 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴))
71 simp12 1204 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
72 simp2rr 1243 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))
73 simp2rl 1242 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 β‰  𝑇)
742, 7, 83at 38664 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇) ∧ 𝑆 β‰  𝑇)) β†’ (((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
753, 70, 71, 72, 73, 74syl32anc 1378 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
7675ad3antrrr 728 . . . . . . . . . . . . 13 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
7769, 76mpbid 231 . . . . . . . . . . . 12 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∨ 𝑅))
7877eqcomd 2738 . . . . . . . . . . 11 (((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
7978ex 413 . . . . . . . . . 10 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
8079necon3ad 2953 . . . . . . . . 9 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ Β¬ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
8153, 80mpd 15 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
822, 7, 8, 28lvoli2 38755 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ∈ 𝑉)
8345, 47, 49, 51, 81, 82syl113anc 1382 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ∈ 𝑉)
8427ad2antrr 724 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ∈ 𝑉)
852, 28lvolcmp 38791 . . . . . . 7 ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ∈ 𝑉 ∧ π‘Š ∈ 𝑉) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) = π‘Š))
8643, 83, 84, 85syl3anc 1371 . . . . . 6 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) = π‘Š))
8742, 86mpbid 231 . . . . 5 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) = π‘Š)
881, 2, 7latjlej2 18411 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ (π‘ˆ ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
894, 22, 24, 15, 88syl13anc 1372 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (π‘ˆ ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
9037, 89mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
9190ad2antrr 724 . . . . 5 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ π‘ˆ) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
9287, 91eqbrtrrd 5172 . . . 4 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
931, 7, 8hlatjcl 38540 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑆 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
943, 16, 20, 93syl3anc 1371 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑆 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
951, 2, 7latlej2 18406 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑆 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ)) β†’ 𝑇 ≀ ((𝑆 ∨ π‘ˆ) ∨ 𝑇))
964, 94, 59, 95syl3anc 1371 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑇 ≀ ((𝑆 ∨ π‘ˆ) ∨ 𝑇))
977, 8hlatj32 38545 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴)) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑆 ∨ π‘ˆ) ∨ 𝑇))
983, 16, 17, 20, 97syl13anc 1372 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = ((𝑆 ∨ π‘ˆ) ∨ 𝑇))
9996, 98breqtrrd 5176 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑇 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
1001, 2, 4, 59, 24, 30, 99, 32lattrd 18403 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑇 ≀ π‘Š)
1011, 2, 7latjle12 18407 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ 𝑇 ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š))
1024, 15, 59, 30, 101syl13anc 1372 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ 𝑇 ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š))
10331, 100, 102mpbi2and 710 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š)
104103ad2antrr 724 . . . . . 6 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š)
1053ad2antrr 724 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝐾 ∈ HL)
10644ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
10711, 17jca 512 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
108107ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
10948ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝑃 β‰  𝑄)
11050ad2antrr 724 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))
111 simpr 485 . . . . . . . 8 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
1122, 7, 8, 28lvoli2 38755 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
113106, 108, 109, 110, 111, 112syl113anc 1382 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
11427ad2antrr 724 . . . . . . 7 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ∈ 𝑉)
1152, 28lvolcmp 38791 . . . . . . 7 ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉 ∧ π‘Š ∈ 𝑉) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = π‘Š))
116105, 113, 114, 115syl3anc 1371 . . . . . 6 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = π‘Š))
117104, 116mpbid 231 . . . . 5 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = π‘Š)
1181, 2, 7latjlej2 18411 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ (𝑇 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
1194, 59, 24, 15, 118syl13anc 1372 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑇 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
12099, 119mpd 15 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
121120ad2antrr 724 . . . . 5 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
122117, 121eqbrtrrd 5172 . . . 4 ((((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ Β¬ 𝑇 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
12392, 122pm2.61dan 811 . . 3 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
1241, 7, 8hlatjcl 38540 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1253, 17, 20, 124syl3anc 1371 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1261, 2, 7latlej1 18405 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Baseβ€˜πΎ) ∧ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) β†’ 𝑆 ≀ (𝑆 ∨ (𝑇 ∨ π‘ˆ)))
1274, 57, 125, 126syl3anc 1371 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 ≀ (𝑆 ∨ (𝑇 ∨ π‘ˆ)))
1281, 7latjass 18440 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Baseβ€˜πΎ) ∧ 𝑇 ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ))) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = (𝑆 ∨ (𝑇 ∨ π‘ˆ)))
1294, 57, 59, 22, 128syl13anc 1372 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) = (𝑆 ∨ (𝑇 ∨ π‘ˆ)))
130127, 129breqtrrd 5176 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))
1311, 2, 4, 57, 24, 30, 130, 32lattrd 18403 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ 𝑆 ≀ π‘Š)
1321, 2, 7latjle12 18407 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ) ∧ 𝑆 ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ 𝑆 ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š))
1334, 15, 57, 30, 132syl13anc 1372 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ 𝑆 ≀ π‘Š) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š))
13431, 131, 133mpbi2and 710 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š)
135134adantr 481 . . . . 5 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š)
1363adantr 481 . . . . . 6 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝐾 ∈ HL)
13744adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
13811, 16jca 512 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
139138adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
14048adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ 𝑃 β‰  𝑄)
14150adantr 481 . . . . . . 7 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))
142 simpr 485 . . . . . . 7 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))
1432, 7, 8, 28lvoli2 38755 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
144137, 139, 140, 141, 142, 143syl113anc 1382 . . . . . 6 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
14527adantr 481 . . . . . 6 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ∈ 𝑉)
1462, 28lvolcmp 38791 . . . . . 6 ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ∧ π‘Š ∈ 𝑉) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = π‘Š))
147136, 144, 145, 146syl3anc 1371 . . . . 5 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ π‘Š ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = π‘Š))
148135, 147mpbid 231 . . . 4 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = π‘Š)
1491, 2, 7latjlej2 18411 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Baseβ€˜πΎ))) β†’ (𝑆 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
1504, 57, 24, 15, 149syl13anc 1372 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (𝑆 ≀ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ))))
151130, 150mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
152151adantr 481 . . . 4 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
153148, 152eqbrtrrd 5172 . . 3 (((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) ∧ Β¬ 𝑆 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑅)) β†’ π‘Š ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
154123, 153pm2.61dan 811 . 2 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ π‘Š ≀ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)))
1551, 2, 4, 26, 30, 35, 154latasymd 18402 1 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑅 ≀ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (𝑆 β‰  𝑇 ∧ Β¬ π‘ˆ ≀ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≀ π‘Š ∧ ((𝑆 ∨ 𝑇) ∨ π‘ˆ) ≀ π‘Š ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) β‰  ((𝑆 ∨ 𝑇) ∨ π‘ˆ))) β†’ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ π‘ˆ)) = π‘Š)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7411  Basecbs 17148  lecple 17208  joincjn 18268  Latclat 18388  Atomscatm 38436  HLchlt 38523  LVolsclvol 38667
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-proset 18252  df-poset 18270  df-plt 18287  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-p0 18382  df-lat 18389  df-clat 18456  df-oposet 38349  df-ol 38351  df-oml 38352  df-covers 38439  df-ats 38440  df-atl 38471  df-cvlat 38495  df-hlat 38524  df-llines 38672  df-lplanes 38673  df-lvols 38674
This theorem is referenced by:  2lplnj  38794
  Copyright terms: Public domain W3C validator