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

Theorem cvrat4 38617
Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 31917 analog.) (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
cvrat4.b 𝐡 = (Baseβ€˜πΎ)
cvrat4.l ≀ = (leβ€˜πΎ)
cvrat4.j ∨ = (joinβ€˜πΎ)
cvrat4.z 0 = (0.β€˜πΎ)
cvrat4.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
cvrat4 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
Distinct variable groups:   𝐴,π‘Ÿ   𝐡,π‘Ÿ   ∨ ,π‘Ÿ   𝐾,π‘Ÿ   ≀ ,π‘Ÿ   𝑃,π‘Ÿ   𝑄,π‘Ÿ   𝑋,π‘Ÿ
Allowed substitution hint:   0 (π‘Ÿ)

Proof of Theorem cvrat4
StepHypRef Expression
1 hlatl 38533 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ AtLat)
21adantr 479 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ AtLat)
3 simpr1 1192 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑋 ∈ 𝐡)
4 cvrat4.b . . . . . . . . . . 11 𝐡 = (Baseβ€˜πΎ)
5 cvrat4.l . . . . . . . . . . 11 ≀ = (leβ€˜πΎ)
6 cvrat4.z . . . . . . . . . . 11 0 = (0.β€˜πΎ)
7 cvrat4.a . . . . . . . . . . 11 𝐴 = (Atomsβ€˜πΎ)
84, 5, 6, 7atlex 38489 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐡 ∧ 𝑋 β‰  0 ) β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋)
983exp 1117 . . . . . . . . 9 (𝐾 ∈ AtLat β†’ (𝑋 ∈ 𝐡 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋)))
102, 3, 9sylc 65 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋))
1110adantr 479 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋))
12 simpll 763 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝐾 ∈ HL)
13 simplr3 1215 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ∈ 𝐴)
14 simpr 483 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐴)
15 cvrat4.j . . . . . . . . . . . . . . 15 ∨ = (joinβ€˜πΎ)
165, 15, 7hlatlej1 38548 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ≀ (𝑄 ∨ π‘Ÿ))
1712, 13, 14, 16syl3anc 1369 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ≀ (𝑄 ∨ π‘Ÿ))
18 breq1 5150 . . . . . . . . . . . . 13 (𝑃 = 𝑄 β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑄 ≀ (𝑄 ∨ π‘Ÿ)))
1917, 18imbitrrid 245 . . . . . . . . . . . 12 (𝑃 = 𝑄 β†’ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
2019expd 414 . . . . . . . . . . 11 (𝑃 = 𝑄 β†’ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (π‘Ÿ ∈ 𝐴 β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2120impcom 406 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (π‘Ÿ ∈ 𝐴 β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
2221anim2d 610 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ ((π‘Ÿ ≀ 𝑋 ∧ π‘Ÿ ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2322expcomd 415 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (π‘Ÿ ∈ 𝐴 β†’ (π‘Ÿ ≀ 𝑋 β†’ (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
2423reximdvai 3163 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2511, 24syld 47 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2625ex 411 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
2726a1i 11 . . . 4 (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))))
2827com4l 92 . . 3 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))))
2928imp4a 421 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
30 hllat 38536 . . . . . . . . . . . . . 14 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
3130adantr 479 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
32 simpr3 1194 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
334, 7atbase 38462 . . . . . . . . . . . . . 14 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ 𝐡)
3432, 33syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐡)
354, 5, 15latleeqj2 18409 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ (𝑄 ≀ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
3631, 34, 3, 35syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄 ≀ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
3736biimpa 475 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) β†’ (𝑋 ∨ 𝑄) = 𝑋)
3837breq2d 5159 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) ↔ 𝑃 ≀ 𝑋))
3938biimpa 475 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ 𝑋)
4039expl 456 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ 𝑋))
41 simpl 481 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ HL)
42 simpr2 1193 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
435, 15, 7hlatlej2 38549 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) β†’ 𝑃 ≀ (𝑄 ∨ 𝑃))
4441, 32, 42, 43syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ≀ (𝑄 ∨ 𝑃))
4540, 44jctird 525 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
4645, 42jctild 524 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃)))))
4746impl 454 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
48 breq1 5150 . . . . . . 7 (π‘Ÿ = 𝑃 β†’ (π‘Ÿ ≀ 𝑋 ↔ 𝑃 ≀ 𝑋))
49 oveq2 7419 . . . . . . . 8 (π‘Ÿ = 𝑃 β†’ (𝑄 ∨ π‘Ÿ) = (𝑄 ∨ 𝑃))
5049breq2d 5159 . . . . . . 7 (π‘Ÿ = 𝑃 β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑃 ≀ (𝑄 ∨ 𝑃)))
5148, 50anbi12d 629 . . . . . 6 (π‘Ÿ = 𝑃 β†’ ((π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)) ↔ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
5251rspcev 3611 . . . . 5 ((𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5347, 52syl 17 . . . 4 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5453adantrl 712 . . 3 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ (𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5554exp31 418 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄 ≀ 𝑋 β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
56 simpr 483 . . 3 ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ (𝑋 ∨ 𝑄))
57 ioran 980 . . . . 5 (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) ↔ (Β¬ 𝑃 = 𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
58 df-ne 2939 . . . . . 6 (𝑃 β‰  𝑄 ↔ Β¬ 𝑃 = 𝑄)
5958anbi1i 622 . . . . 5 ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ↔ (Β¬ 𝑃 = 𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
6057, 59bitr4i 277 . . . 4 (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) ↔ (𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
61 eqid 2730 . . . . . . . . . 10 (meetβ€˜πΎ) = (meetβ€˜πΎ)
624, 5, 15, 61, 7cvrat3 38616 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))
63623expd 1351 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 β‰  𝑄 β†’ (Β¬ 𝑄 ≀ 𝑋 β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))))
6463imp4c 422 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))
654, 7atbase 38462 . . . . . . . . . . . . 13 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)
6642, 65syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐡)
674, 15latjcl 18396 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 ∨ 𝑄) ∈ 𝐡)
6831, 66, 34, 67syl3anc 1369 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ∈ 𝐡)
694, 5, 61latmle1 18421 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
7031, 3, 68, 69syl3anc 1369 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
7170adantr 479 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
72 simpll 763 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝐾 ∈ HL)
7363imp44 427 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴)
74 simplr2 1214 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝑃 ∈ 𝐴)
7534adantr 479 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝑄 ∈ 𝐡)
7673, 74, 753jca 1126 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡))
7772, 76jca 510 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)))
784, 5, 61, 6, 7atnle 38490 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐡) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑄(meetβ€˜πΎ)𝑋) = 0 ))
792, 32, 3, 78syl3anc 1369 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑄(meetβ€˜πΎ)𝑋) = 0 ))
804, 61latmcom 18420 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)𝑋) = (𝑋(meetβ€˜πΎ)𝑄))
8131, 34, 3, 80syl3anc 1369 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)𝑋) = (𝑋(meetβ€˜πΎ)𝑄))
8281eqeq1d 2732 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄(meetβ€˜πΎ)𝑋) = 0 ↔ (𝑋(meetβ€˜πΎ)𝑄) = 0 ))
8379, 82bitrd 278 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑋(meetβ€˜πΎ)𝑄) = 0 ))
844, 61latmcl 18397 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
8531, 3, 68, 84syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
8685, 3, 343jca 1126 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡))
8731, 86jca 510 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝐾 ∈ Lat ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡)))
884, 5, 61latmlem2 18427 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑄(meetβ€˜πΎ)𝑋)))
8987, 70, 88sylc 65 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑄(meetβ€˜πΎ)𝑋))
9089, 81breqtrd 5173 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑋(meetβ€˜πΎ)𝑄))
91 breq2 5151 . . . . . . . . . . . . . . . 16 ((𝑋(meetβ€˜πΎ)𝑄) = 0 β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑋(meetβ€˜πΎ)𝑄) ↔ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ))
9290, 91syl5ibcom 244 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋(meetβ€˜πΎ)𝑄) = 0 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ))
93 hlop 38535 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
9493adantr 479 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ OP)
954, 61latmcl 18397 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡)
9631, 34, 85, 95syl3anc 1369 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡)
974, 5, 6ople0 38360 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ↔ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ))
9894, 96, 97syl2anc 582 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ↔ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ))
9992, 98sylibd 238 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋(meetβ€˜πΎ)𝑄) = 0 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ))
10083, 99sylbid 239 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ 𝑄 ≀ 𝑋 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ))
101100imp 405 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ Β¬ 𝑄 ≀ 𝑋) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
102101adantrl 712 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
103102adantrr 713 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
1044, 5, 61latmle2 18422 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑃 ∨ 𝑄))
10531, 3, 68, 104syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑃 ∨ 𝑄))
1064, 15latjcom 18404 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
10731, 66, 34, 106syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
108105, 107breqtrd 5173 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃))
109108adantr 479 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃))
11030adantr 479 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
111 simpr3 1194 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ 𝑄 ∈ 𝐡)
112 simpr1 1192 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴)
1134, 7atbase 38462 . . . . . . . . . . . . . 14 ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
114112, 113syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
1154, 61latmcom 18420 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄))
116110, 111, 114, 115syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄))
117116eqeq1d 2732 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ↔ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄) = 0 ))
1184, 5, 15, 61, 6, 7hlexch3 38565 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡) ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄) = 0 ) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃) β†’ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
1191183expia 1119 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄) = 0 β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃) β†’ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
120117, 119sylbid 239 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃) β†’ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
12177, 103, 109, 120syl3c 66 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))
12271, 121jca 510 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
123122ex 411 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
12464, 123jcad 511 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))))
125 breq1 5150 . . . . . . . 8 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (π‘Ÿ ≀ 𝑋 ↔ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋))
126 oveq2 7419 . . . . . . . . 9 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (𝑄 ∨ π‘Ÿ) = (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))
127126breq2d 5159 . . . . . . . 8 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
128125, 127anbi12d 629 . . . . . . 7 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ ((π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)) ↔ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
129128rspcev 3611 . . . . . 6 (((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
130124, 129syl6 35 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
131130expd 414 . . . 4 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13260, 131biimtrid 241 . . 3 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13356, 132syl7 74 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13429, 55, 133ecase3d 1030 1 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  lecple 17208  joincjn 18268  meetcmee 18269  0.cp0 18380  Latclat 18388  OPcops 38345  Atomscatm 38436  AtLatcal 38437  HLchlt 38523
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-proset 18252  df-poset 18270  df-plt 18287  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-p0 18382  df-lat 18389  df-clat 18456  df-oposet 38349  df-ol 38351  df-oml 38352  df-covers 38439  df-ats 38440  df-atl 38471  df-cvlat 38495  df-hlat 38524
This theorem is referenced by:  cvrat42  38618  ps-2  38652
  Copyright terms: Public domain W3C validator