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

Theorem lhp2lt 38350
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.
StepHypRef Expression
1 simp2r 1201 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑃 ≀ π‘Š)
2 simp3r 1203 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑄 ≀ π‘Š)
3 simp1l 1198 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝐾 ∈ HL)
43hllatd 37712 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝐾 ∈ Lat)
5 simp2l 1200 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑃 ∈ 𝐴)
6 eqid 2738 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
7 lhp2lt.a . . . . . 6 𝐴 = (Atomsβ€˜πΎ)
86, 7atbase 37637 . . . . 5 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
95, 8syl 17 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
10 simp3l 1202 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑄 ∈ 𝐴)
116, 7atbase 37637 . . . . 5 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
1210, 11syl 17 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
13 simp1r 1199 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ π‘Š ∈ 𝐻)
14 lhp2lt.h . . . . . 6 𝐻 = (LHypβ€˜πΎ)
156, 14lhpbase 38347 . . . . 5 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
1613, 15syl 17 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ π‘Š ∈ (Baseβ€˜πΎ))
17 lhp2lt.l . . . . 5 ≀ = (leβ€˜πΎ)
18 lhp2lt.j . . . . 5 ∨ = (joinβ€˜πΎ)
196, 17, 18latjle12 18274 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ π‘Š ∧ 𝑄 ≀ π‘Š) ↔ (𝑃 ∨ 𝑄) ≀ π‘Š))
204, 9, 12, 16, 19syl13anc 1373 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ ((𝑃 ≀ π‘Š ∧ 𝑄 ≀ π‘Š) ↔ (𝑃 ∨ 𝑄) ≀ π‘Š))
211, 2, 20mpbi2and 711 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ (𝑃 ∨ 𝑄) ≀ π‘Š)
2218, 17, 73dim2 37817 . . . 4 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ 𝐴 (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)))
233, 5, 10, 22syl3anc 1372 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ 𝐴 (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)))
24 simp11l 1285 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝐾 ∈ HL)
25 hlop 37710 . . . . . . . 8 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
2624, 25syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝐾 ∈ OP)
2724hllatd 37712 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝐾 ∈ Lat)
28 simp12l 1287 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝑃 ∈ 𝐴)
29 simp13l 1289 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝑄 ∈ 𝐴)
306, 18, 7hlatjcl 37715 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
3124, 28, 29, 30syl3anc 1372 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
32 simp2l 1200 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ π‘Ÿ ∈ 𝐴)
336, 7atbase 37637 . . . . . . . . . 10 (π‘Ÿ ∈ 𝐴 β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
3432, 33syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
356, 18latjcl 18263 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ))
3627, 31, 34, 35syl3anc 1372 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ))
37 simp2r 1201 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝑠 ∈ 𝐴)
386, 7atbase 37637 . . . . . . . . 9 (𝑠 ∈ 𝐴 β†’ 𝑠 ∈ (Baseβ€˜πΎ))
3937, 38syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ 𝑠 ∈ (Baseβ€˜πΎ))
406, 18latjcl 18263 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ (Baseβ€˜πΎ)) β†’ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠) ∈ (Baseβ€˜πΎ))
4127, 36, 39, 40syl3anc 1372 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠) ∈ (Baseβ€˜πΎ))
42 eqid 2738 . . . . . . . 8 (1.β€˜πΎ) = (1.β€˜πΎ)
43 eqid 2738 . . . . . . . 8 ( β‹– β€˜πΎ) = ( β‹– β€˜πΎ)
446, 42, 43ncvr1 37620 . . . . . . 7 ((𝐾 ∈ OP ∧ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠) ∈ (Baseβ€˜πΎ)) β†’ Β¬ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠))
4526, 41, 44syl2anc 585 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ Β¬ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠))
46 eqid 2738 . . . . . . . . . . . 12 (lubβ€˜πΎ) = (lubβ€˜πΎ)
47 simpl1l 1225 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝐾 ∈ HL)
4847hllatd 37712 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝐾 ∈ Lat)
49 simpl2l 1227 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝑃 ∈ 𝐴)
50 simpl3l 1229 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝑄 ∈ 𝐴)
5147, 49, 50, 30syl3anc 1372 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
52 simpr1l 1231 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ π‘Ÿ ∈ 𝐴)
5352, 33syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
5448, 51, 53, 35syl3anc 1372 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ))
5547, 25syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝐾 ∈ OP)
56 eqid 2738 . . . . . . . . . . . . . . 15 (glbβ€˜πΎ) = (glbβ€˜πΎ)
576, 46, 56op01dm 37531 . . . . . . . . . . . . . 14 (𝐾 ∈ OP β†’ ((Baseβ€˜πΎ) ∈ dom (lubβ€˜πΎ) ∧ (Baseβ€˜πΎ) ∈ dom (glbβ€˜πΎ)))
5857simpld 496 . . . . . . . . . . . . 13 (𝐾 ∈ OP β†’ (Baseβ€˜πΎ) ∈ dom (lubβ€˜πΎ))
5955, 58syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (Baseβ€˜πΎ) ∈ dom (lubβ€˜πΎ))
606, 46, 17, 42, 47, 54, 59ple1 18254 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ≀ (1.β€˜πΎ))
61 hlpos 37714 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ 𝐾 ∈ Poset)
6247, 61syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝐾 ∈ Poset)
636, 42op1cl 37533 . . . . . . . . . . . . 13 (𝐾 ∈ OP β†’ (1.β€˜πΎ) ∈ (Baseβ€˜πΎ))
6455, 63syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (1.β€˜πΎ) ∈ (Baseβ€˜πΎ))
65 simpr2l 1233 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄))
666, 17, 18, 43, 7cvr1 37759 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ 𝐴) β†’ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( β‹– β€˜πΎ)((𝑃 ∨ 𝑄) ∨ π‘Ÿ)))
6747, 51, 52, 66syl3anc 1372 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄)( β‹– β€˜πΎ)((𝑃 ∨ 𝑄) ∨ π‘Ÿ)))
6865, 67mpbid 231 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (𝑃 ∨ 𝑄)( β‹– β€˜πΎ)((𝑃 ∨ 𝑄) ∨ π‘Ÿ))
69 simpr3 1197 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (𝑃 ∨ 𝑄) = π‘Š)
70 simpl1r 1226 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ π‘Š ∈ 𝐻)
7142, 43, 14lhp1cvr 38348 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ π‘Š( β‹– β€˜πΎ)(1.β€˜πΎ))
7247, 70, 71syl2anc 585 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ π‘Š( β‹– β€˜πΎ)(1.β€˜πΎ))
7369, 72eqbrtrd 5126 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (𝑃 ∨ 𝑄)( β‹– β€˜πΎ)(1.β€˜πΎ))
746, 17, 43cvrcmp 37631 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ) ∧ (1.β€˜πΎ) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ)) ∧ ((𝑃 ∨ 𝑄)( β‹– β€˜πΎ)((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∧ (𝑃 ∨ 𝑄)( β‹– β€˜πΎ)(1.β€˜πΎ))) β†’ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ≀ (1.β€˜πΎ) ↔ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) = (1.β€˜πΎ)))
7562, 54, 64, 51, 68, 73, 74syl132anc 1389 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ≀ (1.β€˜πΎ) ↔ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) = (1.β€˜πΎ)))
7660, 75mpbid 231 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) = (1.β€˜πΎ))
77 simpr2r 1234 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))
78 simpr1r 1232 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ 𝑠 ∈ 𝐴)
796, 17, 18, 43, 7cvr1 37759 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ 𝐴) β†’ (Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ↔ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠)))
8047, 54, 78, 79syl3anc 1372 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ↔ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠)))
8177, 80mpbid 231 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠))
8276, 81eqbrtrrd 5128 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) ∧ (𝑃 ∨ 𝑄) = π‘Š)) β†’ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠))
83823exp2 1355 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ ((Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) β†’ ((𝑃 ∨ 𝑄) = π‘Š β†’ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠)))))
84833imp 1112 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ ((𝑃 ∨ 𝑄) = π‘Š β†’ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠)))
8584necon3bd 2956 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ (Β¬ (1.β€˜πΎ)( β‹– β€˜πΎ)(((𝑃 ∨ 𝑄) ∨ π‘Ÿ) ∨ 𝑠) β†’ (𝑃 ∨ 𝑄) β‰  π‘Š))
8645, 85mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ))) β†’ (𝑃 ∨ 𝑄) β‰  π‘Š)
87863exp 1120 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ ((π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ ((Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) β†’ (𝑃 ∨ 𝑄) β‰  π‘Š)))
8887rexlimdvv 3203 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ (βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ 𝐴 (Β¬ π‘Ÿ ≀ (𝑃 ∨ 𝑄) ∧ Β¬ 𝑠 ≀ ((𝑃 ∨ 𝑄) ∨ π‘Ÿ)) β†’ (𝑃 ∨ 𝑄) β‰  π‘Š))
8923, 88mpd 15 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ (𝑃 ∨ 𝑄) β‰  π‘Š)
903, 5, 10, 30syl3anc 1372 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
91 lhp2lt.s . . . 4 < = (ltβ€˜πΎ)
9217, 91pltval 18156 . . 3 ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ 𝐻) β†’ ((𝑃 ∨ 𝑄) < π‘Š ↔ ((𝑃 ∨ 𝑄) ≀ π‘Š ∧ (𝑃 ∨ 𝑄) β‰  π‘Š)))
933, 90, 13, 92syl3anc 1372 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ ((𝑃 ∨ 𝑄) < π‘Š ↔ ((𝑃 ∨ 𝑄) ≀ π‘Š ∧ (𝑃 ∨ 𝑄) β‰  π‘Š)))
9421, 89, 93mpbir2and 712 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≀ π‘Š) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≀ π‘Š)) β†’ (𝑃 ∨ 𝑄) < π‘Š)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2942  βˆƒwrex 3072   class class class wbr 5104  dom cdm 5631  β€˜cfv 6492  (class class class)co 7350  Basecbs 17018  lecple 17075  Posetcpo 18131  ltcplt 18132  lubclub 18133  glbcglb 18134  joincjn 18135  1.cp1 18248  Latclat 18255  OPcops 37520   β‹– ccvr 37610  Atomscatm 37611  HLchlt 37698  LHypclh 38333
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 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  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 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-proset 18119  df-poset 18137  df-plt 18154  df-lub 18170  df-glb 18171  df-join 18172  df-meet 18173  df-p0 18249  df-p1 18250  df-lat 18256  df-clat 18323  df-oposet 37524  df-ol 37526  df-oml 37527  df-covers 37614  df-ats 37615  df-atl 37646  df-cvlat 37670  df-hlat 37699  df-lhyp 38337
This theorem is referenced by:  lhpexle3lem  38360
  Copyright terms: Public domain W3C validator