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 40065

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 40066 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 2736	. 2 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		2lplnja.l	. 2 ⊢ ≤ = (le‘𝐾)
3		simp11l 1286	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝐾 ∈ HL)
4	3	hllatd 39810	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝐾 ∈ Lat)
5		simp121 1307	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑃 ∈ 𝐴)
6		simp122 1308	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑄 ∈ 𝐴)
7		2lplnja.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
8		2lplnja.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9	1, 7, 8	hlatjcl 39813	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
10	3, 5, 6, 9	syl3anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
11		simp123 1309	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑅 ∈ 𝐴)
12	1, 8	atbase 39735	. . . . 5 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
13	11, 12	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑅 ∈ (Base‘𝐾))
14	1, 7	latjcl 18405	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
15	4, 10, 13, 14	syl3anc 1374	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
16		simp2l1 1274	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ∈ 𝐴)
17		simp2l2 1275	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ∈ 𝐴)
18	1, 7, 8	hlatjcl 39813	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
19	3, 16, 17, 18	syl3anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
20		simp2l3 1276	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ∈ 𝐴)
21	1, 8	atbase 39735	. . . . 5 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
22	20, 21	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ∈ (Base‘𝐾))
23	1, 7	latjcl 18405	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾))
24	4, 19, 22, 23	syl3anc 1374	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾))
25	1, 7	latjcl 18405	. . 3 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ∈ (Base‘𝐾))
26	4, 15, 24, 25	syl3anc 1374	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ∈ (Base‘𝐾))
27		simp11r 1287	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ∈ 𝑉)
28		2lplnja.v	. . . 4 ⊢ 𝑉 = (LVols‘𝐾)
29	1, 28	lvolbase 40024	. . 3 ⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ (Base‘𝐾))
30	27, 29	syl 17	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ∈ (Base‘𝐾))
31		simp31 1211	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊)
32		simp32 1212	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊)
33	1, 2, 7	latjle12 18416	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊))
34	4, 15, 24, 30, 33	syl13anc 1375	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊))
35	31, 32, 34	mpbi2and 713	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) ≤ 𝑊)
36	1, 2, 7	latlej2 18415	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
37	4, 19, 22, 36	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
38	1, 2, 4, 22, 24, 30, 37, 32	lattrd 18412	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑈 ≤ 𝑊)
39	1, 2, 7	latjle12 18416	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊))
40	4, 15, 22, 30, 39	syl13anc 1375	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊))
41	31, 38, 40	mpbi2and 713	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊)
42	41	ad2antrr 727	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊)
43	3	ad2antrr 727	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
44	3, 5, 6	3jca 1129	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
45	44	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
46	11, 20	jca 511	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
47	46	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
48		simp13l 1290	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑃 ≠ 𝑄)
49	48	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
50		simp13r 1291	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
51	50	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
52		simp33 1213	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))
53	52	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))
54		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56	1, 8	atbase 39735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
57	16, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ∈ (Base‘𝐾))
58	1, 8	atbase 39735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾))
59	17, 58	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ∈ (Base‘𝐾))
60	1, 2, 7	latjle12 18416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
61	4, 57, 59, 15, 60	syl13anc 1375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
62	61	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
63	54, 55, 62	mpbi2and 713	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
64	63	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
65		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
66	1, 2, 7	latjle12 18416	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	4, 19, 22, 15, 66	syl13anc 1375	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	67	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑆 ∨ 𝑇) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	64, 65, 68	mpbi2and 713	. . . . . . . . . . . . 13 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
70		simp2l 1201	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
71		simp12 1206	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
72		simp2rr 1245	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))
73		simp2rl 1244	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≠ 𝑇)
74	2, 7, 8	3at 39936	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (¬ 𝑈 ≤ (𝑆 ∨ 𝑇) ∧ 𝑆 ≠ 𝑇)) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
75	3, 70, 71, 72, 73, 74	syl32anc 1381	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
76	75	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅)))
77	69, 76	mpbid 232	. . . . . . . . . . . 12 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑃 ∨ 𝑄) ∨ 𝑅))
78	77	eqcomd 2742	. . . . . . . . . . 11 ⊢ (((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈))
79	78	ex 412	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)))
80	79	necon3ad 2945	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈) → ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
81	53, 80	mpd 15	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
82	2, 7, 8, 28	lvoli2 40027	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑈 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉)
83	45, 47, 49, 51, 81, 82	syl113anc 1385	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉)
84	27	ad2antrr 727	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
85	2, 28	lvolcmp 40063	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊))
86	43, 83, 84, 85	syl3anc 1374	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊))
87	42, 86	mpbid 232	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) = 𝑊)
88	1, 2, 7	latjlej2 18420	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
89	4, 22, 24, 15, 88	syl13anc 1375	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
90	37, 89	mpd 15	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
91	90	ad2antrr 727	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑈) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
92	87, 91	eqbrtrrd 5109	. . . 4 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
93	1, 7, 8	hlatjcl 39813	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
94	3, 16, 20, 93	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
95	1, 2, 7	latlej2 18415	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ≤ ((𝑆 ∨ 𝑈) ∨ 𝑇))
96	4, 94, 59, 95	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ ((𝑆 ∨ 𝑈) ∨ 𝑇))
97	7, 8	hlatj32 39818	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑆 ∨ 𝑈) ∨ 𝑇))
98	3, 16, 17, 20, 97	syl13anc 1375	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = ((𝑆 ∨ 𝑈) ∨ 𝑇))
99	96, 98	breqtrrd 5113	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
100	1, 2, 4, 59, 24, 30, 99, 32	lattrd 18412	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑇 ≤ 𝑊)
101	1, 2, 7	latjle12 18416	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊))
102	4, 15, 59, 30, 101	syl13anc 1375	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊))
103	31, 100, 102	mpbi2and 713	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
104	103	ad2antrr 727	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
105	3	ad2antrr 727	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
106	44	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
107	11, 17	jca 511	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
108	107	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴))
109	48	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
110	50	ad2antrr 727	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
111		simpr 484	. . . . . . . 8 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
112	2, 7, 8, 28	lvoli2 40027	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
113	106, 108, 109, 110, 111, 112	syl113anc 1385	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉)
114	27	ad2antrr 727	. . . . . . 7 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
115	2, 28	lvolcmp 40063	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊))
116	105, 113, 114, 115	syl3anc 1374	. . . . . 6 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊))
117	104, 116	mpbid 232	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) = 𝑊)
118	1, 2, 7	latjlej2 18420	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
119	4, 59, 24, 15, 118	syl13anc 1375	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑇 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
120	99, 119	mpd 15	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
121	120	ad2antrr 727	. . . . 5 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑇) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
122	117, 121	eqbrtrrd 5109	. . . 4 ⊢ ((((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
123	92, 122	pm2.61dan 813	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
124	1, 7, 8	hlatjcl 39813	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
125	3, 17, 20, 124	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
126	1, 2, 7	latlej1 18414	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑆 ∨ (𝑇 ∨ 𝑈)))
127	4, 57, 125, 126	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ (𝑆 ∨ (𝑇 ∨ 𝑈)))
128	1, 7	latjass 18449	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = (𝑆 ∨ (𝑇 ∨ 𝑈)))
129	4, 57, 59, 22, 128	syl13anc 1375	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((𝑆 ∨ 𝑇) ∨ 𝑈) = (𝑆 ∨ (𝑇 ∨ 𝑈)))
130	127, 129	breqtrrd 5113	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈))
131	1, 2, 4, 57, 24, 30, 130, 32	lattrd 18412	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑆 ≤ 𝑊)
132	1, 2, 7	latjle12 18416	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊))
133	4, 15, 57, 30, 132	syl13anc 1375	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ 𝑆 ≤ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊))
134	31, 131, 133	mpbi2and 713	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
135	134	adantr 480	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
136	3	adantr 480	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝐾 ∈ HL)
137	44	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
138	11, 16	jca 511	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
139	138	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
140	48	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑃 ≠ 𝑄)
141	50	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
142		simpr 484	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
143	2, 7, 8, 28	lvoli2 40027	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
144	137, 139, 140, 141, 142, 143	syl113anc 1385	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉)
145	27	adantr 480	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ∈ 𝑉)
146	2, 28	lvolcmp 40063	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊))
147	136, 144, 145, 146	syl3anc 1374	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊))
148	135, 147	mpbid 232	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = 𝑊)
149	1, 2, 7	latjlej2 18420	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
150	4, 57, 24, 15, 149	syl13anc 1375	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (𝑆 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈))))
151	130, 150	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
152	151	adantr 480	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
153	148, 152	eqbrtrrd 5109	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
154	123, 153	pm2.61dan 813	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → 𝑊 ≤ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)))
155	1, 2, 4, 26, 30, 35, 154	latasymd 18411	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 Basecbs 17179 lecple 17227 joincjn 18277 Latclat 18397 Atomscatm 39709 HLchlt 39796 LVolsclvol 39939

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-proset 18260 df-poset 18279 df-plt 18294 df-lub 18310 df-glb 18311 df-join 18312 df-meet 18313 df-p0 18389 df-lat 18398 df-clat 18465 df-oposet 39622 df-ol 39624 df-oml 39625 df-covers 39712 df-ats 39713 df-atl 39744 df-cvlat 39768 df-hlat 39797 df-llines 39944 df-lplanes 39945 df-lvols 39946

This theorem is referenced by: 2lplnj 40066

W3C validator