Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme22e Structured version   Visualization version   GIF version
Theorem cdleme22e 39203
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. 𝐹, 𝑁, 𝑂 represent f(z), fz(s), fz(t) respectively. When t ∨ v = p ∨ q, fz(s) ≀ fz(t) ∨ v. (Contributed by NM, 6-Dec-2012.)
Hypotheses
Ref Expression
cdleme22.l ≀ = (leβ€˜πΎ)
cdleme22.j ∨ = (joinβ€˜πΎ)
cdleme22.m ∧ = (meetβ€˜πΎ)
cdleme22.a 𝐴 = (Atomsβ€˜πΎ)
cdleme22.h 𝐻 = (LHypβ€˜πΎ)
cdleme22e.u π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
cdleme22e.f 𝐹 = ((𝑧 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
cdleme22e.n 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š)))
cdleme22e.o 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
Assertion
Ref Expression
cdleme22e (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑁 ≀ (𝑂 ∨ 𝑉))
Proof of Theorem cdleme22e
StepHypRef Expression
1 cdleme22e.n . . 3 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š)))
2 simp1l 1197 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝐾 ∈ HL)
32hllatd 38222 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝐾 ∈ Lat)
4 simp21l 1290 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑃 ∈ 𝐴)
5 simp22l 1292 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑄 ∈ 𝐴)
6 eqid 2732 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
7 cdleme22.j . . . . . 6 ∨ = (joinβ€˜πΎ)
8 cdleme22.a . . . . . 6 𝐴 = (Atomsβ€˜πΎ)
96, 7, 8hlatjcl 38225 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
102, 4, 5, 9syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
11 simp1r 1198 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘Š ∈ 𝐻)
12 simp33l 1300 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑧 ∈ 𝐴)
13 cdleme22.l . . . . . . 7 ≀ = (leβ€˜πΎ)
14 cdleme22.m . . . . . . 7 ∧ = (meetβ€˜πΎ)
15 cdleme22.h . . . . . . 7 𝐻 = (LHypβ€˜πΎ)
16 cdleme22e.u . . . . . . 7 π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
17 cdleme22e.f . . . . . . 7 𝐹 = ((𝑧 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
1813, 7, 14, 8, 15, 16, 17, 6cdleme1b 39085 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) β†’ 𝐹 ∈ (Baseβ€˜πΎ))
192, 11, 4, 5, 12, 18syl23anc 1377 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝐹 ∈ (Baseβ€˜πΎ))
20 simp23l 1294 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑆 ∈ 𝐴)
216, 7, 8hlatjcl 38225 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) β†’ (𝑆 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
222, 20, 12, 21syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑆 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
236, 15lhpbase 38857 . . . . . . 7 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
2411, 23syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘Š ∈ (Baseβ€˜πΎ))
256, 14latmcl 18389 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑧) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((𝑆 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
263, 22, 24, 25syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑆 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
276, 7latjcl 18388 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Baseβ€˜πΎ) ∧ ((𝑆 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
283, 19, 26, 27syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
296, 13, 14latmle1 18413 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š))) ≀ (𝑃 ∨ 𝑄))
303, 10, 28, 29syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑆 ∨ 𝑧) ∧ π‘Š))) ≀ (𝑃 ∨ 𝑄))
311, 30eqbrtrid 5182 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑁 ≀ (𝑃 ∨ 𝑄))
32 simp1 1136 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
33 simp21 1206 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
34 simp23r 1295 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑇 ∈ 𝐴)
35 simp31 1209 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š))
36 simp32l 1298 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑃 β‰  𝑄)
37 simp32r 1299 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄))
3813, 7, 14, 8, 15, 16cdleme22a 39199 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ 𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄))) β†’ 𝑉 = π‘ˆ)
3932, 33, 5, 34, 35, 36, 37, 38syl133anc 1393 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑉 = π‘ˆ)
4039oveq2d 7421 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑂 ∨ 𝑉) = (𝑂 ∨ π‘ˆ))
41 cdleme22e.o . . . . . 6 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
4241oveq1i 7415 . . . . 5 (𝑂 ∨ π‘ˆ) = (((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ)
43 simp21r 1291 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ Β¬ 𝑃 ≀ π‘Š)
4413, 7, 14, 8, 15, 16cdleme0a 39070 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 β‰  𝑄)) β†’ π‘ˆ ∈ 𝐴)
452, 11, 4, 43, 5, 36, 44syl222anc 1386 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘ˆ ∈ 𝐴)
466, 7, 8hlatjcl 38225 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) β†’ (𝑇 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
472, 34, 12, 46syl3anc 1371 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
486, 14latmcl 18389 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑇 ∨ 𝑧) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((𝑇 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
493, 47, 24, 48syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
506, 7latjcl 18388 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Baseβ€˜πΎ) ∧ ((𝑇 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
513, 19, 49, 50syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
5213, 7, 14, 8, 15, 16cdlemeulpq 39079 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ π‘ˆ ≀ (𝑃 ∨ 𝑄))
532, 11, 4, 5, 52syl22anc 837 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘ˆ ≀ (𝑃 ∨ 𝑄))
546, 13, 7, 14, 8atmod2i1 38720 . . . . . 6 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ (𝑃 ∨ 𝑄)) β†’ (((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
552, 45, 10, 51, 53, 54syl131anc 1383 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
5642, 55eqtr2id 2785 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)) = (𝑂 ∨ π‘ˆ))
5740, 56eqtr4d 2775 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑂 ∨ 𝑉) = ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
5839oveq2d 7421 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ 𝑉) = (𝑇 ∨ π‘ˆ))
5937, 58eqtr3d 2774 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑄) = (𝑇 ∨ π‘ˆ))
606, 7, 8hlatjcl 38225 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
612, 34, 45, 60syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
626, 8atbase 38147 . . . . . . . 8 (𝑧 ∈ 𝐴 β†’ 𝑧 ∈ (Baseβ€˜πΎ))
6312, 62syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑧 ∈ (Baseβ€˜πΎ))
646, 13, 7latlej1 18397 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑇 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ 𝑧 ∈ (Baseβ€˜πΎ)) β†’ (𝑇 ∨ π‘ˆ) ≀ ((𝑇 ∨ π‘ˆ) ∨ 𝑧))
653, 61, 63, 64syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ π‘ˆ) ≀ ((𝑇 ∨ π‘ˆ) ∨ 𝑧))
667, 8hlatj32 38230 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑇 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑇 ∨ π‘ˆ) ∨ 𝑧) = ((𝑇 ∨ 𝑧) ∨ π‘ˆ))
672, 34, 45, 12, 66syl13anc 1372 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ π‘ˆ) ∨ 𝑧) = ((𝑇 ∨ 𝑧) ∨ π‘ˆ))
686, 8atbase 38147 . . . . . . . . . 10 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
6945, 68syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
706, 7latj32 18434 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑇 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))) β†’ ((𝑧 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
713, 63, 69, 49, 70syl13anc 1372 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑧 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
726, 7latj32 18434 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Baseβ€˜πΎ) ∧ ((𝑇 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ))) β†’ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) = ((𝐹 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
733, 19, 49, 69, 72syl13anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) = ((𝐹 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
746, 7, 8hlatjcl 38225 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) β†’ (𝑃 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
752, 4, 12, 74syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑧) ∈ (Baseβ€˜πΎ))
7613, 7, 8hlatlej1 38233 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) β†’ 𝑃 ≀ (𝑃 ∨ 𝑧))
772, 4, 12, 76syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑃 ≀ (𝑃 ∨ 𝑧))
786, 13, 7, 14, 8atmod3i1 38723 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑧) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ 𝑃 ≀ (𝑃 ∨ 𝑧)) β†’ (𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑃 ∨ 𝑧) ∧ (𝑃 ∨ π‘Š)))
792, 4, 75, 24, 77, 78syl131anc 1383 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑃 ∨ 𝑧) ∧ (𝑃 ∨ π‘Š)))
80 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (1.β€˜πΎ) = (1.β€˜πΎ)
8113, 7, 80, 8, 15lhpjat2 38880 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (𝑃 ∨ π‘Š) = (1.β€˜πΎ))
822, 11, 33, 81syl21anc 836 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ π‘Š) = (1.β€˜πΎ))
8382oveq2d 7421 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑧) ∧ (𝑃 ∨ π‘Š)) = ((𝑃 ∨ 𝑧) ∧ (1.β€˜πΎ)))
84 hlol 38219 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
852, 84syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝐾 ∈ OL)
866, 14, 80olm11 38085 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ OL ∧ (𝑃 ∨ 𝑧) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑧) ∧ (1.β€˜πΎ)) = (𝑃 ∨ 𝑧))
8785, 75, 86syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑧) ∧ (1.β€˜πΎ)) = (𝑃 ∨ 𝑧))
8879, 83, 873eqtrd 2776 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = (𝑃 ∨ 𝑧))
8988oveq1d 7420 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ 𝑄) = ((𝑃 ∨ 𝑧) ∨ 𝑄))
9016oveq2i 7416 . . . . . . . . . . . . . . . . . . 19 (𝑄 ∨ π‘ˆ) = (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ π‘Š))
9113, 7, 8hlatlej2 38234 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ 𝑄 ≀ (𝑃 ∨ 𝑄))
922, 4, 5, 91syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑄 ≀ (𝑃 ∨ 𝑄))
936, 13, 7, 14, 8atmod3i1 38723 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ 𝑄 ≀ (𝑃 ∨ 𝑄)) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ π‘Š)) = ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ π‘Š)))
942, 5, 10, 24, 92, 93syl131anc 1383 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ π‘Š)) = ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ π‘Š)))
9590, 94eqtrid 2784 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∨ π‘ˆ) = ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ π‘Š)))
96 simp22 1207 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š))
9713, 7, 80, 8, 15lhpjat2 38880 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) β†’ (𝑄 ∨ π‘Š) = (1.β€˜πΎ))
982, 11, 96, 97syl21anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∨ π‘Š) = (1.β€˜πΎ))
9998oveq2d 7421 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ π‘Š)) = ((𝑃 ∨ 𝑄) ∧ (1.β€˜πΎ)))
1006, 14, 80olm11 38085 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ OL ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∧ (1.β€˜πΎ)) = (𝑃 ∨ 𝑄))
10185, 10, 100syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∧ (1.β€˜πΎ)) = (𝑃 ∨ 𝑄))
10295, 99, 1013eqtrd 2776 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∨ π‘ˆ) = (𝑃 ∨ 𝑄))
103102oveq1d 7420 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑄 ∨ π‘ˆ) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑃 ∨ 𝑄) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
1046, 8atbase 38147 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
1054, 104syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
1066, 14latmcl 18389 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑧) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
1073, 75, 24, 106syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))
1086, 8atbase 38147 . . . . . . . . . . . . . . . . . 18 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
1095, 108syl 17 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
1106, 7latj32 18434 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ 𝑄) = ((𝑃 ∨ 𝑄) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
1113, 105, 107, 109, 110syl13anc 1372 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ 𝑄) = ((𝑃 ∨ 𝑄) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
112103, 111eqtr4d 2775 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑄 ∨ π‘ˆ) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑃 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ 𝑄))
1137, 8hlatj32 38230 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) = ((𝑃 ∨ 𝑧) ∨ 𝑄))
1142, 4, 5, 12, 113syl13anc 1372 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) = ((𝑃 ∨ 𝑧) ∨ 𝑄))
11589, 112, 1143eqtr4rd 2783 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) = ((𝑄 ∨ π‘ˆ) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)))
1166, 7latj32 18434 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ))) β†’ ((𝑄 ∨ π‘ˆ) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
1173, 109, 69, 107, 116syl13anc 1372 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑄 ∨ π‘ˆ) ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) = ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
118115, 117eqtrd 2772 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) = ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
119118oveq2d 7421 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑧 ∨ π‘ˆ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
1206, 7latjcl 18388 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑧 ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) ∈ (Baseβ€˜πΎ))
1213, 10, 63, 120syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∨ 𝑧) ∈ (Baseβ€˜πΎ))
1226, 13, 7latlej2 18398 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑧 ∈ (Baseβ€˜πΎ)) β†’ 𝑧 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧))
1233, 10, 63, 122syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑧 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧))
1246, 13, 7, 14, 8atmod1i1 38716 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑧 ∈ 𝐴 ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧) ∈ (Baseβ€˜πΎ)) ∧ 𝑧 ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧)) β†’ (𝑧 ∨ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧))) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)))
1252, 12, 69, 121, 123, 124syl131anc 1383 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧))) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)))
12617oveq1i 7415 . . . . . . . . . . . . 13 (𝐹 ∨ π‘ˆ) = (((𝑧 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ)
1276, 7, 8hlatjcl 38225 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑧 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1282, 12, 45, 127syl3anc 1371 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1296, 7latjcl 18388 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑧) ∧ π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
1303, 109, 107, 129syl3anc 1371 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ))
13113, 7, 8hlatlej2 38234 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑧 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ π‘ˆ ≀ (𝑧 ∨ π‘ˆ))
1322, 12, 45, 131syl3anc 1371 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘ˆ ≀ (𝑧 ∨ π‘ˆ))
1336, 13, 7, 14, 8atmod2i1 38720 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑧 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ (𝑧 ∨ π‘ˆ)) β†’ (((𝑧 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
1342, 45, 128, 130, 132, 133syl131anc 1383 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (((𝑧 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š))) ∨ π‘ˆ) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
135126, 134eqtrid 2784 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐹 ∨ π‘ˆ) = ((𝑧 ∨ π‘ˆ) ∧ ((𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)))
136119, 125, 1353eqtr4rd 2783 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐹 ∨ π‘ˆ) = (𝑧 ∨ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧))))
1376, 13, 7latlej1 18397 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑧 ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧))
1383, 10, 63, 137syl3anc 1371 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑄) ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧))
1396, 13, 3, 69, 10, 121, 53, 138lattrd 18395 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧))
1406, 13, 14latleeqm1 18416 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ π‘ˆ ∈ (Baseβ€˜πΎ) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧) ∈ (Baseβ€˜πΎ)) β†’ (π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧) ↔ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)) = π‘ˆ))
1413, 69, 121, 140syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (π‘ˆ ≀ ((𝑃 ∨ 𝑄) ∨ 𝑧) ↔ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)) = π‘ˆ))
142139, 141mpbid 231 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧)) = π‘ˆ)
143142oveq2d 7421 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ (π‘ˆ ∧ ((𝑃 ∨ 𝑄) ∨ 𝑧))) = (𝑧 ∨ π‘ˆ))
144136, 143eqtrd 2772 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝐹 ∨ π‘ˆ) = (𝑧 ∨ π‘ˆ))
145144oveq1d 7420 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝐹 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑧 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
14673, 145eqtrd 2772 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) = ((𝑧 ∨ π‘ˆ) ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
14713, 7, 8hlatlej2 38234 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ≀ (𝑇 ∨ 𝑧))
1482, 34, 12, 147syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ 𝑧 ≀ (𝑇 ∨ 𝑧))
1496, 13, 7, 14, 8atmod3i1 38723 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑧 ∈ 𝐴 ∧ (𝑇 ∨ 𝑧) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ 𝑧 ≀ (𝑇 ∨ 𝑧)) β†’ (𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑇 ∨ 𝑧) ∧ (𝑧 ∨ π‘Š)))
1502, 12, 47, 24, 148, 149syl131anc 1383 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑇 ∨ 𝑧) ∧ (𝑧 ∨ π‘Š)))
151 simp33 1211 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))
15213, 7, 80, 8, 15lhpjat2 38880 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š)) β†’ (𝑧 ∨ π‘Š) = (1.β€˜πΎ))
1532, 11, 151, 152syl21anc 836 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ π‘Š) = (1.β€˜πΎ))
154153oveq2d 7421 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ 𝑧) ∧ (𝑧 ∨ π‘Š)) = ((𝑇 ∨ 𝑧) ∧ (1.β€˜πΎ)))
155150, 154eqtrd 2772 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) = ((𝑇 ∨ 𝑧) ∧ (1.β€˜πΎ)))
1566, 14, 80olm11 38085 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑇 ∨ 𝑧) ∈ (Baseβ€˜πΎ)) β†’ ((𝑇 ∨ 𝑧) ∧ (1.β€˜πΎ)) = (𝑇 ∨ 𝑧))
15785, 47, 156syl2anc 584 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ 𝑧) ∧ (1.β€˜πΎ)) = (𝑇 ∨ 𝑧))
158155, 157eqtr2d 2773 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ 𝑧) = (𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)))
159158oveq1d 7420 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ 𝑧) ∨ π‘ˆ) = ((𝑧 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
16071, 146, 1593eqtr4rd 2783 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ 𝑧) ∨ π‘ˆ) = ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
16167, 160eqtrd 2772 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑇 ∨ π‘ˆ) ∨ 𝑧) = ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
16265, 161breqtrd 5173 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑇 ∨ π‘ˆ) ≀ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
16359, 162eqbrtrd 5169 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑄) ≀ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ))
1646, 7latjcl 18388 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1653, 51, 69, 164syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
1666, 13, 14latleeqm1 18416 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) ↔ ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)) = (𝑃 ∨ 𝑄)))
1673, 10, 165, 166syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ≀ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ) ↔ ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)) = (𝑃 ∨ 𝑄)))
168163, 167mpbid 231 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑄) ∧ ((𝐹 ∨ ((𝑇 ∨ 𝑧) ∧ π‘Š)) ∨ π‘ˆ)) = (𝑃 ∨ 𝑄))
16957, 168eqtr2d 2773 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š) ∧ (𝑃 β‰  𝑄 ∧ (𝑇 ∨ 𝑉) = (𝑃 ∨ 𝑄)) ∧ (𝑧 ∈ 𝐴 ∧ Β¬ 𝑧 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑄) = (𝑂 ∨ 𝑉))
17031, 169breqtrd 5173 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 5147  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  lecple 17200  joincjn 18260  meetcmee 18261  1.cp1 18373  Latclat 18380  OLcol 38032  Atomscatm 38121  HLchlt 38208  LHypclh 38843
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-p1 18375  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  df-lhyp 38847
This theorem is referenced by:  cdleme26e  39218
  Copyright terms: Public domain W3C validator