2lplnja - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2lplnja		Structured version Visualization version GIF version

Theorem 2lplnja 36915

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 36916 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**
Step	Hyp	Ref	Expression
1		eqid 2798	. 2 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		2lplnja.l	. 2 ⊢ ≤ = (le‘𝐾)
3		simp11l 1281	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝐾 ∈ HL)
4	3	hllatd 36660	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝐾 ∈ Lat)
5		simp121 1302	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑃 ∈ 𝐴)
6		simp122 1303	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑄 ∈ 𝐴)
7		2lplnja.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
8		2lplnja.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9	1, 7, 8	hlatjcl 36663	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
10	3, 5, 6, 9	syl3anc 1368	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
11		simp123 1304	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑅 ∈ 𝐴)
12	1, 8	atbase 36585	. . . . 5 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
13	11, 12	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑅 ∈ (Base‘𝐾))
14	1, 7	latjcl 17653	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
15	4, 10, 13, 14	syl3anc 1368	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
16		simp2l1 1269	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ∈ 𝐴)
17		simp2l2 1270	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ∈ 𝐴)
18	1, 7, 8	hlatjcl 36663	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
19	3, 16, 17, 18	syl3anc 1368	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
20		simp2l3 1271	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ∈ 𝐴)
21	1, 8	atbase 36585	. . . . 5 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
22	20, 21	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ∈ (Base‘𝐾))
23	1, 7	latjcl 17653	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾))
24	4, 19, 22, 23	syl3anc 1368	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾))
25	1, 7	latjcl 17653	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ∈ (Base‘𝐾))
26	4, 15, 24, 25	syl3anc 1368	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ∈ (Base‘𝐾))
27		simp11r 1282	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ∈ 𝑉)
28		2lplnja.v	. . . 4 ⊢ 𝑉 = (LVols‘𝐾)
29	1, 28	lvolbase 36874	. . 3 ⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ (Base‘𝐾))
30	27, 29	syl 17	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ∈ (Base‘𝐾))
31		simp31 1206	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊)
32		simp32 1207	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊)
33	1, 2, 7	latjle12 17664	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊))
34	4, 15, 24, 30, 33	syl13anc 1369	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊))
35	31, 32, 34	mpbi2and 711	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊)
36	1, 2, 7	latlej2 17663	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
37	4, 19, 22, 36	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
38	1, 2, 4, 22, 24, 30, 37, 32	lattrd 17660	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ≤ 𝑊)
39	1, 2, 7	latjle12 17664	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊))
40	4, 15, 22, 30, 39	syl13anc 1369	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊))
41	31, 38, 40	mpbi2and 711	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊)
42	41	ad2antrr 725	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊)
43	3	ad2antrr 725	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
44	3, 5, 6	3jca 1125	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
45	44	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
46	11, 20	jca 515	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
47	46	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
48		simp13l 1285	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑃 ≠ 𝑄)
49	48	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
50		simp13r 1286	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
51	50	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
52		simp33 1208	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))
53	52	ad2antrr 725	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))
54		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56	1, 8	atbase 36585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
57	16, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ∈ (Base‘𝐾))
58	1, 8	atbase 36585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾))
59	17, 58	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ∈ (Base‘𝐾))
60	1, 2, 7	latjle12 17664	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
61	4, 57, 59, 15, 60	syl13anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
62	61	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
63	54, 55, 62	mpbi2and 711	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
64	63	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
65		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
66	1, 2, 7	latjle12 17664	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	4, 19, 22, 15, 66	syl13anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	67	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	64, 65, 68	mpbi2and 711	. . . . . . . . . . . . 13 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
70		simp2l 1196	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
71		simp12 1201	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
72		simp2rr 1240	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))
73		simp2rl 1239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≠ 𝑇)
74	2, 7, 8	3at 36786	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (¬ 𝑈 ≤ (𝑆 ∨ 𝑇) ∧ 𝑆 ≠ 𝑇)) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
75	3, 70, 71, 72, 73, 74	syl32anc 1375	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
76	75	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
77	69, 76	mpbid 235	. . . . . . . . . . . 12 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅))
78	77	eqcomd 2804	. . . . . . . . . . 11 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈))
79	78	ex 416	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)))
80	79	necon3ad 3000	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈) → ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
81	53, 80	mpd 15	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
82	2, 7, 8, 28	lvoli2 36877	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉)
83	45, 47, 49, 51, 81, 82	syl113anc 1379	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉)
84	27	ad2antrr 725	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
85	2, 28	lvolcmp 36913	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊))
86	43, 83, 84, 85	syl3anc 1368	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊))
87	42, 86	mpbid 235	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊)
88	1, 2, 7	latjlej2 17668	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
89	4, 22, 24, 15, 88	syl13anc 1369	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
90	37, 89	mpd 15	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
91	90	ad2antrr 725	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
92	87, 91	eqbrtrrd 5054	. . . 4 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
93	1, 7, 8	hlatjcl 36663	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
94	3, 16, 20, 93	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
95	1, 2, 7	latlej2 17663	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ≤ ((𝑆 ∨ 𝑈) ∨ 𝑇))
96	4, 94, 59, 95	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ ((𝑆 ∨ 𝑈) ∨ 𝑇))
97	7, 8	hlatj32 36668	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑆 ∨ 𝑈) ∨ 𝑇))
98	3, 16, 17, 20, 97	syl13anc 1369	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑆 ∨ 𝑈) ∨ 𝑇))
99	96, 98	breqtrrd 5058	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
100	1, 2, 4, 59, 24, 30, 99, 32	lattrd 17660	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ 𝑊)
101	1, 2, 7	latjle12 17664	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊))
102	4, 15, 59, 30, 101	syl13anc 1369	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊))
103	31, 100, 102	mpbi2and 711	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
104	103	ad2antrr 725	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
105	3	ad2antrr 725	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
106	44	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
107	11, 17	jca 515	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
108	107	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
109	48	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
110	50	ad2antrr 725	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
111		simpr 488	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
112	2, 7, 8, 28	lvoli2 36877	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
113	106, 108, 109, 110, 111, 112	syl113anc 1379	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
114	27	ad2antrr 725	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
115	2, 28	lvolcmp 36913	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊))
116	105, 113, 114, 115	syl3anc 1368	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊))
117	104, 116	mpbid 235	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊)
118	1, 2, 7	latjlej2 17668	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
119	4, 59, 24, 15, 118	syl13anc 1369	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
120	99, 119	mpd 15	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
121	120	ad2antrr 725	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
122	117, 121	eqbrtrrd 5054	. . . 4 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
123	92, 122	pm2.61dan 812	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
124	1, 7, 8	hlatjcl 36663	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
125	3, 17, 20, 124	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
126	1, 2, 7	latlej1 17662	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑆 ∨ (𝑇 ∨ 𝑈)))
127	4, 57, 125, 126	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ (𝑆 ∨ (𝑇 ∨ 𝑈)))
128	1, 7	latjass 17697	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = (𝑆 ∨ (𝑇 ∨ 𝑈)))
129	4, 57, 59, 22, 128	syl13anc 1369	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = (𝑆 ∨ (𝑇 ∨ 𝑈)))
130	127, 129	breqtrrd 5058	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
131	1, 2, 4, 57, 24, 30, 130, 32	lattrd 17660	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ 𝑊)
132	1, 2, 7	latjle12 17664	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊))
133	4, 15, 57, 30, 132	syl13anc 1369	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊))
134	31, 131, 133	mpbi2and 711	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
135	134	adantr 484	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
136	3	adantr 484	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
137	44	adantr 484	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
138	11, 16	jca 515	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
139	138	adantr 484	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
140	48	adantr 484	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
141	50	adantr 484	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
142		simpr 488	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
143	2, 7, 8, 28	lvoli2 36877	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
144	137, 139, 140, 141, 142, 143	syl113anc 1379	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
145	27	adantr 484	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
146	2, 28	lvolcmp 36913	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊))
147	136, 144, 145, 146	syl3anc 1368	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊))
148	135, 147	mpbid 235	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊)
149	1, 2, 7	latjlej2 17668	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
150	4, 57, 24, 15, 149	syl13anc 1369	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
151	130, 150	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
152	151	adantr 484	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
153	148, 152	eqbrtrrd 5054	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
154	123, 153	pm2.61dan 812	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
155	1, 2, 4, 26, 30, 35, 154	latasymd 17659	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 class class class wbr 5030 ‘cfv 6324 (class class class)co 7135 Basecbs 16475 lecple 16564 joincjn 17546 Latclat 17647 Atomscatm 36559 HLchlt 36646 LVolsclvol 36789

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-proset 17530 df-poset 17548 df-plt 17560 df-lub 17576 df-glb 17577 df-join 17578 df-meet 17579 df-p0 17641 df-lat 17648 df-clat 17710 df-oposet 36472 df-ol 36474 df-oml 36475 df-covers 36562 df-ats 36563 df-atl 36594 df-cvlat 36618 df-hlat 36647 df-llines 36794 df-lplanes 36795 df-lvols 36796

This theorem is referenced by: 2lplnj 36916

W3C validator