Theorem 4atlem11 37630

Description: Lemma for 4at 37634. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.)

Hypotheses

Ref	Expression
4at.l	⊢ ≤ = (le‘𝐾)
4at.j	⊢ ∨ = (join‘𝐾)
4at.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
4atlem11	⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))

Proof of Theorem 4atlem11

Step	Hyp	Ref	Expression
1		3anass 1094	. . . 4 ⊢ ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
2		simpl11 1247	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ HL)
3	2	hllatd 37385	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝐾 ∈ Lat)
4		simpl2l 1225	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ 𝐴)
5		eqid 2739	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		4at.a	. . . . . . . 8 ⊢ 𝐴 = (Atoms‘𝐾)
7	5, 6	atbase 37310	. . . . . . 7 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
8	4, 7	syl 17	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑅 ∈ (Base‘𝐾))
9		simpl2r 1226	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ 𝐴)
10	5, 6	atbase 37310	. . . . . . 7 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
11	9, 10	syl 17	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑆 ∈ (Base‘𝐾))
12		simpl12 1248	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑃 ∈ 𝐴)
13		simpl31 1253	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑈 ∈ 𝐴)
14		4at.j	. . . . . . . . 9 ⊢ ∨ = (join‘𝐾)
15	5, 14, 6	hlatjcl 37388	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
16	2, 12, 13, 15	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
17		simpl32 1254	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑉 ∈ 𝐴)
18		simpl33 1255	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑊 ∈ 𝐴)
19	5, 14, 6	hlatjcl 37388	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) → (𝑉 ∨ 𝑊) ∈ (Base‘𝐾))
20	2, 17, 18, 19	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑉 ∨ 𝑊) ∈ (Base‘𝐾))
21	5, 14	latjcl 18166	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑉 ∨ 𝑊) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))
22	3, 16, 20, 21	syl3anc 1370	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))
23		4at.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
24	5, 23, 14	latjle12 18177	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))) → ((𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
25	3, 8, 11, 22, 24	syl13anc 1371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
26	25	anbi2d 629	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) ↔ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
27	1, 26	syl5bb 283	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
28		simpl13 1249	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑄 ∈ 𝐴)
29	5, 6	atbase 37310	. . . . 5 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑄 ∈ (Base‘𝐾))
31	5, 14, 6	hlatjcl 37388	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
32	2, 4, 9, 31	syl3anc 1370	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
33	5, 23, 14	latjle12 18177	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∈ (Base‘𝐾))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
34	3, 30, 32, 22, 33	syl13anc 1371	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ (𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
35	27, 34	bitrd 278	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ↔ (𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
36		simpl1 1190	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴))
37		simpl2 1191	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
38	17, 18	jca 512	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴))
39		simpr 485	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
40	23, 14, 6	4atlem3a 37618	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)))
41	36, 37, 38, 39, 40	syl31anc 1372	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)))
42		simp1l 1196	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
43		simp1r 1197	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
44		simp2 1136	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊))
45		simp3 1137	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
46	23, 14, 6	4atlem11b 37629	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
47	42, 43, 44, 45, 46	syl121anc 1374	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
48	47	3exp 1118	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
49	2	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝐾 ∈ HL)
50	12	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑃 ∈ 𝐴)
51	28	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑄 ∈ 𝐴)
52	4	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑅 ∈ 𝐴)
53	9	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑆 ∈ 𝐴)
54	14, 6	hlatj4 37395	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)))
55	49, 50, 51, 52, 53, 54	syl122anc 1378	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)))
56	49, 50, 52	3jca 1127	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
57	51, 53	jca 512	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
58		simp1l3 1267	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴))
59		simp1r2 1269	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))
60	23, 14, 6	4atlem0be 37616	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑅)
61	49, 50, 51, 52, 59, 60	syl131anc 1382	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑃 ≠ 𝑅)
62		simp1r1 1268	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑃 ≠ 𝑄)
63	23, 14, 6	4atlem0ae 37615	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑄 ≤ (𝑃 ∨ 𝑅))
64	49, 50, 51, 52, 62, 59, 63	syl132anc 1387	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑄 ≤ (𝑃 ∨ 𝑅))
65		simp1r3 1270	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
66	14, 6	hlatj32 37393	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑃 ∨ 𝑅) ∨ 𝑄))
67	49, 50, 51, 52, 66	syl13anc 1371	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑃 ∨ 𝑅) ∨ 𝑄))
68	67	breq2d 5087	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑆 ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)))
69	65, 68	mtbid 324	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄))
70	61, 64, 69	3jca 1127	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑃 ≠ 𝑅 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑅) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)))
71		simp2 1136	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊))
72		simp32 1209	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
73		simp31 1208	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
74		simp33 1210	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
75	23, 14, 6	4atlem11b 37629	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑅 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑅) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) ∧ (𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
76	56, 57, 58, 70, 71, 72, 73, 74, 75	syl323anc 1399	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
77	55, 76	eqtrd 2779	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
78	77	3exp 1118	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
79	5, 6	atbase 37310	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
80	12, 79	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → 𝑃 ∈ (Base‘𝐾))
81	5, 14	latj4rot 18217	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)))
82	3, 80, 30, 8, 11, 81	syl122anc 1378	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)))
83	14, 6	hlatjcom 37389	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑆 ∨ 𝑃) = (𝑃 ∨ 𝑆))
84	2, 9, 12, 83	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ∨ 𝑃) = (𝑃 ∨ 𝑆))
85	84	oveq1d 7299	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑆 ∨ 𝑃) ∨ (𝑄 ∨ 𝑅)) = ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑅)))
86	82, 85	eqtrd 2779	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑅)))
87	86	3ad2ant1 1132	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑅)))
88	2, 12, 9	3jca 1127	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴))
89	28, 4	jca 512	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
90		simpl3 1192	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴))
91	88, 89, 90	3jca 1127	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
92	91	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)))
93	23, 14, 6	4noncolr1 37476	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)))
94	36, 37, 39, 93	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)))
95		necom 2998	. . . . . . . . . . 11 ⊢ (𝑆 ≠ 𝑃 ↔ 𝑃 ≠ 𝑆)
96	95	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ↔ 𝑃 ≠ 𝑆))
97	84	breq2d 5087	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ≤ (𝑆 ∨ 𝑃) ↔ 𝑄 ≤ (𝑃 ∨ 𝑆)))
98	97	notbid 318	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ↔ ¬ 𝑄 ≤ (𝑃 ∨ 𝑆)))
99	84	oveq1d 7299	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑆 ∨ 𝑃) ∨ 𝑄) = ((𝑃 ∨ 𝑆) ∨ 𝑄))
100	99	breq2d 5087	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄) ↔ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄)))
101	100	notbid 318	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄) ↔ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄)))
102	96, 98, 101	3anbi123d 1435	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄)) ↔ (𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑆) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄))))
103	94, 102	mpbid 231	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑆) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄)))
104	103	3ad2ant1 1132	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑆) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄)))
105		simp2 1136	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊))
106		simpr3 1195	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
107		simpr1 1193	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
108		simpr2 1194	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
109	106, 107, 108	3jca 1127	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
110	109	3adant2 1130	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → (𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
111	23, 14, 6	4atlem11b 37629	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑆) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑆) ∨ 𝑄)) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) ∧ (𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑅)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
112	92, 104, 105, 110, 111	syl121anc 1374	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑅)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
113	87, 112	eqtrd 2779	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))
114	113	3exp 1118	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
115	48, 78, 114	3jaod 1427	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊) ∨ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))))
116	41, 115	mpd 15	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))
117	35, 116	sylbird 259	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2944   class class class wbr 5075  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  lecple 16978  joincjn 18038  Latclat 18158  Atomscatm 37284  HLchlt 37371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-proset 18022  df-poset 18040  df-plt 18057  df-lub 18073  df-glb 18074  df-join 18075  df-meet 18076  df-p0 18152  df-lat 18159  df-clat 18226  df-oposet 37197  df-ol 37199  df-oml 37200  df-covers 37287  df-ats 37288  df-atl 37319  df-cvlat 37343  df-hlat 37372  df-llines 37519  df-lplanes 37520  df-lvols 37521

This theorem is referenced by:  4atlem12b  37632