Theorem lhp2lt 41195

Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.)

Hypotheses

Ref	Expression
lhp2lt.l	⊢ ≤ = (le‘𝐾)
lhp2lt.s	⊢ < = (lt‘𝐾)
lhp2lt.j	⊢ ∨ = (join‘𝐾)
lhp2lt.a	⊢ 𝐴 = (Atoms‘𝐾)
lhp2lt.h	⊢ 𝐻 = (LHyp‘𝐾)

Assertion

Ref	Expression
lhp2lt	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊)

Proof of Theorem lhp2lt

Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2r 1219	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ≤ 𝑊)
2		simp3r 1221	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ≤ 𝑊)
3		simp1l 1216	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝐾 ∈ HL)
4	3	hllatd 40558	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝐾 ∈ Lat)
5		simp2l 1218	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
6		eqid 2760	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		lhp2lt.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	6, 7	atbase 40483	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
9	5, 8	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
10		simp3l 1220	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ∈ 𝐴)
11	6, 7	atbase 40483	. . . . 5 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
12	10, 11	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ∈ (Base‘𝐾))
13		simp1r 1217	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
14		lhp2lt.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
15	6, 14	lhpbase 41192	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
16	13, 15	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
17		lhp2lt.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
18		lhp2lt.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
19	6, 17, 18	latjle12 18633	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊))
20	4, 9, 12, 16, 19	syl13anc 1399	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊))
21	1, 2, 20	mpbi2and 725	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ≤ 𝑊)
22	18, 17, 7	3dim2 40662	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)))
23	3, 5, 10, 22	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)))
24		simp11l 1303	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ HL)
25		hlop 40556	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
26	24, 25	syl 18	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ OP)
27	24	hllatd 40558	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ Lat)
28		simp12l 1305	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑃 ∈ 𝐴)
29		simp13l 1307	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑄 ∈ 𝐴)
30	6, 18, 7	hlatjcl 40561	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
31	24, 28, 29, 30	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
32		simp2l 1218	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑟 ∈ 𝐴)
33	6, 7	atbase 40483	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
34	32, 33	syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑟 ∈ (Base‘𝐾))
35	6, 18	latjcl 18622	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
36	27, 31, 34, 35	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
37		simp2r 1219	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑠 ∈ 𝐴)
38	6, 7	atbase 40483	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝐴 → 𝑠 ∈ (Base‘𝐾))
39	37, 38	syl 18	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑠 ∈ (Base‘𝐾))
40	6, 18	latjcl 18622	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾))
41	27, 36, 39, 40	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾))
42		eqid 2760	. . . . . . . 8 ⊢ (1.‘𝐾) = (1.‘𝐾)
43		eqid 2760	. . . . . . . 8 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
44	6, 42, 43	ncvr1 40466	. . . . . . 7 ⊢ ((𝐾 ∈ OP ∧ (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾)) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
45	26, 41, 44	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
46		eqid 2760	. . . . . . . . . . . 12 ⊢ (lub‘𝐾) = (lub‘𝐾)
47		simpl1l 1243	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ HL)
48	47	hllatd 40558	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ Lat)
49		simpl2l 1245	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑃 ∈ 𝐴)
50		simpl3l 1247	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑄 ∈ 𝐴)
51	47, 49, 50, 30	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
52		simpr1l 1249	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑟 ∈ 𝐴)
53	52, 33	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑟 ∈ (Base‘𝐾))
54	48, 51, 53, 35	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
55	47, 25	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ OP)
56		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (glb‘𝐾) = (glb‘𝐾)
57	6, 46, 56	op01dm 40377	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ OP → ((Base‘𝐾) ∈ dom (lub‘𝐾) ∧ (Base‘𝐾) ∈ dom (glb‘𝐾)))
58	57	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ OP → (Base‘𝐾) ∈ dom (lub‘𝐾))
59	55, 58	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (Base‘𝐾) ∈ dom (lub‘𝐾))
60	6, 46, 17, 42, 47, 54, 59	ple1 18611	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾))
61		hlpos 40560	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
62	47, 61	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ Poset)
63	6, 42	op1cl 40379	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
64	55, 63	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (1.‘𝐾) ∈ (Base‘𝐾))
65		simpr2l 1251	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))
66	6, 17, 18, 43, 7	cvr1 40604	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟)))
67	47, 51, 52, 66	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟)))
68	65, 67	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟))
69		simpr3 1215	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄) = 𝑊)
70		simpl1r 1244	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑊 ∈ 𝐻)
71	42, 43, 14	lhp1cvr 41193	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
72	47, 70, 71	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
73	69, 72	eqbrtrd 5126	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))
74	6, 17, 43	cvrcmp 40477	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟) ∧ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾)))
75	62, 54, 64, 51, 68, 73, 74	syl132anc 1415	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾)))
76	60, 75	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾))
77		simpr2r 1252	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))
78		simpr1r 1250	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑠 ∈ 𝐴)
79	6, 17, 18, 43, 7	cvr1 40604	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑠 ∈ 𝐴) → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
80	47, 54, 78, 79	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
81	77, 80	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
82	76, 81	eqbrtrrd 5128	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
83	82	3exp2 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) → ((¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → ((𝑃 ∨ 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))))
84	83	3imp 1128	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ((𝑃 ∨ 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
85	84	necon3bd 2969	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) → (𝑃 ∨ 𝑄) ≠ 𝑊))
86	45, 85	mpd 16	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (𝑃 ∨ 𝑄) ≠ 𝑊)
87	86	3exp 1137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) → ((¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → (𝑃 ∨ 𝑄) ≠ 𝑊)))
88	87	rexlimdvv 3218	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → (𝑃 ∨ 𝑄) ≠ 𝑊))
89	23, 88	mpd 16	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ≠ 𝑊)
90	3, 5, 10, 30	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
91		lhp2lt.s	. . . 4 ⊢ < = (lt‘𝐾)
92	17, 91	pltval 18513	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ 𝐻) → ((𝑃 ∨ 𝑄) < 𝑊 ↔ ((𝑃 ∨ 𝑄) ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) ≠ 𝑊)))
93	3, 90, 13, 92	syl3anc 1398	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑃 ∨ 𝑄) < 𝑊 ↔ ((𝑃 ∨ 𝑄) ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) ≠ 𝑊)))
94	21, 89, 93	mpbir2and 726	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086   class class class wbr 5102  dom cdm 5651  ‘cfv 6543  (class class class)co 7424  Basecbs 17396  lecple 17444  Posetcpo 18490  ltcplt 18491  lubclub 18492  glbcglb 18493  joincjn 18494  1.cp1 18605  Latclat 18614  OPcops 40366   ⋖ ccvr 40456  Atomscatm 40457  HLchlt 40544  LHypclh 41178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-proset 18477  df-poset 18496  df-plt 18511  df-lub 18527  df-glb 18528  df-join 18529  df-meet 18530  df-p0 18606  df-p1 18607  df-lat 18615  df-clat 18682  df-oposet 40370  df-ol 40372  df-oml 40373  df-covers 40460  df-ats 40461  df-atl 40492  df-cvlat 40516  df-hlat 40545  df-lhyp 41182

This theorem is used by:  lhpexle3lem  41205