Theorem lhp2lt 39966

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 1201	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ≤ 𝑊)
2		simp3r 1203	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ≤ 𝑊)
3		simp1l 1198	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝐾 ∈ HL)
4	3	hllatd 39328	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝐾 ∈ Lat)
5		simp2l 1200	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
6		eqid 2735	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		lhp2lt.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	6, 7	atbase 39253	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
9	5, 8	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
10		simp3l 1202	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ∈ 𝐴)
11	6, 7	atbase 39253	. . . . 5 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
12	10, 11	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑄 ∈ (Base‘𝐾))
13		simp1r 1199	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
14		lhp2lt.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
15	6, 14	lhpbase 39963	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
16	13, 15	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
17		lhp2lt.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
18		lhp2lt.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
19	6, 17, 18	latjle12 18458	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊))
20	4, 9, 12, 16, 19	syl13anc 1374	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊))
21	1, 2, 20	mpbi2and 712	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ≤ 𝑊)
22	18, 17, 7	3dim2 39433	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)))
23	3, 5, 10, 22	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)))
24		simp11l 1285	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ HL)
25		hlop 39326	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
26	24, 25	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ OP)
27	24	hllatd 39328	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝐾 ∈ Lat)
28		simp12l 1287	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑃 ∈ 𝐴)
29		simp13l 1289	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑄 ∈ 𝐴)
30	6, 18, 7	hlatjcl 39331	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
31	24, 28, 29, 30	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
32		simp2l 1200	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑟 ∈ 𝐴)
33	6, 7	atbase 39253	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
34	32, 33	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑟 ∈ (Base‘𝐾))
35	6, 18	latjcl 18447	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
36	27, 31, 34, 35	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
37		simp2r 1201	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑠 ∈ 𝐴)
38	6, 7	atbase 39253	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝐴 → 𝑠 ∈ (Base‘𝐾))
39	37, 38	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → 𝑠 ∈ (Base‘𝐾))
40	6, 18	latjcl 18447	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾)) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾))
41	27, 36, 39, 40	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾))
42		eqid 2735	. . . . . . . 8 ⊢ (1.‘𝐾) = (1.‘𝐾)
43		eqid 2735	. . . . . . . 8 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
44	6, 42, 43	ncvr1 39236	. . . . . . 7 ⊢ ((𝐾 ∈ OP ∧ (((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) ∈ (Base‘𝐾)) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
45	26, 41, 44	syl2anc 584	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
46		eqid 2735	. . . . . . . . . . . 12 ⊢ (lub‘𝐾) = (lub‘𝐾)
47		simpl1l 1225	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ HL)
48	47	hllatd 39328	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ Lat)
49		simpl2l 1227	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑃 ∈ 𝐴)
50		simpl3l 1229	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑄 ∈ 𝐴)
51	47, 49, 50, 30	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
52		simpr1l 1231	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑟 ∈ 𝐴)
53	52, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑟 ∈ (Base‘𝐾))
54	48, 51, 53, 35	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾))
55	47, 25	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ OP)
56		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ (glb‘𝐾) = (glb‘𝐾)
57	6, 46, 56	op01dm 39147	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ OP → ((Base‘𝐾) ∈ dom (lub‘𝐾) ∧ (Base‘𝐾) ∈ dom (glb‘𝐾)))
58	57	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ OP → (Base‘𝐾) ∈ dom (lub‘𝐾))
59	55, 58	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (Base‘𝐾) ∈ dom (lub‘𝐾))
60	6, 46, 17, 42, 47, 54, 59	ple1 18438	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾))
61		hlpos 39330	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
62	47, 61	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝐾 ∈ Poset)
63	6, 42	op1cl 39149	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
64	55, 63	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (1.‘𝐾) ∈ (Base‘𝐾))
65		simpr2l 1233	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))
66	6, 17, 18, 43, 7	cvr1 39375	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟)))
67	47, 51, 52, 66	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟)))
68	65, 67	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟))
69		simpr3 1197	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄) = 𝑊)
70		simpl1r 1226	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑊 ∈ 𝐻)
71	42, 43, 14	lhp1cvr 39964	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
72	47, 70, 71	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑊( ⋖ ‘𝐾)(1.‘𝐾))
73	69, 72	eqbrtrd 5141	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))
74	6, 17, 43	cvrcmp 39247	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) ∧ ((𝑃 ∨ 𝑄)( ⋖ ‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑟) ∧ (𝑃 ∨ 𝑄)( ⋖ ‘𝐾)(1.‘𝐾))) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾)))
75	62, 54, 64, 51, 68, 73, 74	syl132anc 1390	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (((𝑃 ∨ 𝑄) ∨ 𝑟) ≤ (1.‘𝐾) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾)))
76	60, 75	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟) = (1.‘𝐾))
77		simpr2r 1234	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))
78		simpr1r 1232	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → 𝑠 ∈ 𝐴)
79	6, 17, 18, 43, 7	cvr1 39375	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑄) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑠 ∈ 𝐴) → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
80	47, 54, 78, 79	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
81	77, 80	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → ((𝑃 ∨ 𝑄) ∨ 𝑟)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
82	76, 81	eqbrtrrd 5143	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) ∧ (𝑃 ∨ 𝑄) = 𝑊)) → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠))
83	82	3exp2 1355	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) → ((¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → ((𝑃 ∨ 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))))
84	83	3imp 1110	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → ((𝑃 ∨ 𝑄) = 𝑊 → (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠)))
85	84	necon3bd 2946	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (¬ (1.‘𝐾)( ⋖ ‘𝐾)(((𝑃 ∨ 𝑄) ∨ 𝑟) ∨ 𝑠) → (𝑃 ∨ 𝑄) ≠ 𝑊))
86	45, 85	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) → (𝑃 ∨ 𝑄) ≠ 𝑊)
87	86	3exp 1119	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) → ((¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → (𝑃 ∨ 𝑄) ≠ 𝑊)))
88	87	rexlimdvv 3197	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟)) → (𝑃 ∨ 𝑄) ≠ 𝑊))
89	23, 88	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ≠ 𝑊)
90	3, 5, 10, 30	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
91		lhp2lt.s	. . . 4 ⊢ < = (lt‘𝐾)
92	17, 91	pltval 18340	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ 𝐻) → ((𝑃 ∨ 𝑄) < 𝑊 ↔ ((𝑃 ∨ 𝑄) ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) ≠ 𝑊)))
93	3, 90, 13, 92	syl3anc 1373	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → ((𝑃 ∨ 𝑄) < 𝑊 ↔ ((𝑃 ∨ 𝑄) ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) ≠ 𝑊)))
94	21, 89, 93	mpbir2and 713	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∃wrex 3060   class class class wbr 5119  dom cdm 5654  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  lecple 17276  Posetcpo 18317  ltcplt 18318  lubclub 18319  glbcglb 18320  joincjn 18321  1.cp1 18432  Latclat 18439  OPcops 39136   ⋖ ccvr 39226  Atomscatm 39227  HLchlt 39314  LHypclh 39949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-proset 18304  df-poset 18323  df-plt 18338  df-lub 18354  df-glb 18355  df-join 18356  df-meet 18357  df-p0 18433  df-p1 18434  df-lat 18440  df-clat 18507  df-oposet 39140  df-ol 39142  df-oml 39143  df-covers 39230  df-ats 39231  df-atl 39262  df-cvlat 39286  df-hlat 39315  df-lhyp 39953

This theorem is referenced by:  lhpexle3lem  39976