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 38314
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 31650 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 38230 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ AtLat)
21adantr 482 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ AtLat)
3 simpr1 1195 . . . . . . . . 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 38186 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐡 ∧ 𝑋 β‰  0 ) β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋)
983exp 1120 . . . . . . . . 9 (𝐾 ∈ AtLat β†’ (𝑋 ∈ 𝐡 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋)))
102, 3, 9sylc 65 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋))
1110adantr 482 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋))
12 simpll 766 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝐾 ∈ HL)
13 simplr3 1218 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ∈ 𝐴)
14 simpr 486 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ 𝐴)
15 cvrat4.j . . . . . . . . . . . . . . 15 ∨ = (joinβ€˜πΎ)
165, 15, 7hlatlej1 38245 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ≀ (𝑄 ∨ π‘Ÿ))
1712, 13, 14, 16syl3anc 1372 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑄 ≀ (𝑄 ∨ π‘Ÿ))
18 breq1 5152 . . . . . . . . . . . . 13 (𝑃 = 𝑄 β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑄 ≀ (𝑄 ∨ π‘Ÿ)))
1917, 18imbitrrid 245 . . . . . . . . . . . 12 (𝑃 = 𝑄 β†’ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
2019expd 417 . . . . . . . . . . 11 (𝑃 = 𝑄 β†’ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (π‘Ÿ ∈ 𝐴 β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2120impcom 409 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (π‘Ÿ ∈ 𝐴 β†’ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
2221anim2d 613 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ ((π‘Ÿ ≀ 𝑋 ∧ π‘Ÿ ∈ 𝐴) β†’ (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2322expcomd 418 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (π‘Ÿ ∈ 𝐴 β†’ (π‘Ÿ ≀ 𝑋 β†’ (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
2423reximdvai 3166 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (βˆƒπ‘Ÿ ∈ 𝐴 π‘Ÿ ≀ 𝑋 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2511, 24syld 47 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
2625ex 414 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
2726a1i 11 . . . 4 (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))))
2827com4l 92 . . 3 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ (𝑋 β‰  0 β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))))
2928imp4a 424 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 = 𝑄 β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
30 hllat 38233 . . . . . . . . . . . . . 14 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
3130adantr 482 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
32 simpr3 1197 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
334, 7atbase 38159 . . . . . . . . . . . . . 14 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ 𝐡)
3432, 33syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐡)
354, 5, 15latleeqj2 18405 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ (𝑄 ≀ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
3631, 34, 3, 35syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄 ≀ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
3736biimpa 478 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) β†’ (𝑋 ∨ 𝑄) = 𝑋)
3837breq2d 5161 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) ↔ 𝑃 ≀ 𝑋))
3938biimpa 478 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ 𝑋)
4039expl 459 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ 𝑋))
41 simpl 484 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ HL)
42 simpr2 1196 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
435, 15, 7hlatlej2 38246 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) β†’ 𝑃 ≀ (𝑄 ∨ 𝑃))
4441, 32, 42, 43syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ≀ (𝑄 ∨ 𝑃))
4540, 44jctird 528 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
4645, 42jctild 527 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃)))))
4746impl 457 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
48 breq1 5152 . . . . . . 7 (π‘Ÿ = 𝑃 β†’ (π‘Ÿ ≀ 𝑋 ↔ 𝑃 ≀ 𝑋))
49 oveq2 7417 . . . . . . . 8 (π‘Ÿ = 𝑃 β†’ (𝑄 ∨ π‘Ÿ) = (𝑄 ∨ 𝑃))
5049breq2d 5161 . . . . . . 7 (π‘Ÿ = 𝑃 β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑃 ≀ (𝑄 ∨ 𝑃)))
5148, 50anbi12d 632 . . . . . 6 (π‘Ÿ = 𝑃 β†’ ((π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)) ↔ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))))
5251rspcev 3613 . . . . 5 ((𝑃 ∈ 𝐴 ∧ (𝑃 ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ 𝑃))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5347, 52syl 17 . . . 4 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5453adantrl 715 . . 3 ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≀ 𝑋) ∧ (𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
5554exp31 421 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄 ≀ 𝑋 β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
56 simpr 486 . . 3 ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ 𝑃 ≀ (𝑋 ∨ 𝑄))
57 ioran 983 . . . . 5 (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) ↔ (Β¬ 𝑃 = 𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
58 df-ne 2942 . . . . . 6 (𝑃 β‰  𝑄 ↔ Β¬ 𝑃 = 𝑄)
5958anbi1i 625 . . . . 5 ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ↔ (Β¬ 𝑃 = 𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
6057, 59bitr4i 278 . . . 4 (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) ↔ (𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋))
61 eqid 2733 . . . . . . . . . 10 (meetβ€˜πΎ) = (meetβ€˜πΎ)
624, 5, 15, 61, 7cvrat3 38313 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))
63623expd 1354 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 β‰  𝑄 β†’ (Β¬ 𝑄 ≀ 𝑋 β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))))
6463imp4c 425 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴))
654, 7atbase 38159 . . . . . . . . . . . . 13 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)
6642, 65syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐡)
674, 15latjcl 18392 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 ∨ 𝑄) ∈ 𝐡)
6831, 66, 34, 67syl3anc 1372 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) ∈ 𝐡)
694, 5, 61latmle1 18417 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
7031, 3, 68, 69syl3anc 1372 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
7170adantr 482 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋)
72 simpll 766 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝐾 ∈ HL)
7363imp44 430 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴)
74 simplr2 1217 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝑃 ∈ 𝐴)
7534adantr 482 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ 𝑄 ∈ 𝐡)
7673, 74, 753jca 1129 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡))
7772, 76jca 513 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)))
784, 5, 61, 6, 7atnle 38187 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐡) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑄(meetβ€˜πΎ)𝑋) = 0 ))
792, 32, 3, 78syl3anc 1372 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑄(meetβ€˜πΎ)𝑋) = 0 ))
804, 61latmcom 18416 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)𝑋) = (𝑋(meetβ€˜πΎ)𝑄))
8131, 34, 3, 80syl3anc 1372 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)𝑋) = (𝑋(meetβ€˜πΎ)𝑄))
8281eqeq1d 2735 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑄(meetβ€˜πΎ)𝑋) = 0 ↔ (𝑋(meetβ€˜πΎ)𝑄) = 0 ))
8379, 82bitrd 279 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ 𝑄 ≀ 𝑋 ↔ (𝑋(meetβ€˜πΎ)𝑄) = 0 ))
844, 61latmcl 18393 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
8531, 3, 68, 84syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
8685, 3, 343jca 1129 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡))
8731, 86jca 513 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝐾 ∈ Lat ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡)))
884, 5, 61latmlem2 18423 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑄(meetβ€˜πΎ)𝑋)))
8987, 70, 88sylc 65 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑄(meetβ€˜πΎ)𝑋))
9089, 81breqtrd 5175 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑋(meetβ€˜πΎ)𝑄))
91 breq2 5153 . . . . . . . . . . . . . . . 16 ((𝑋(meetβ€˜πΎ)𝑄) = 0 β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ (𝑋(meetβ€˜πΎ)𝑄) ↔ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ))
9290, 91syl5ibcom 244 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋(meetβ€˜πΎ)𝑄) = 0 β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ))
93 hlop 38232 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
9493adantr 482 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ 𝐾 ∈ OP)
954, 61latmcl 18393 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡)
9631, 34, 85, 95syl3anc 1372 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡)
974, 5, 6ople0 38057 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ∈ 𝐡) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) ≀ 0 ↔ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ))
9894, 96, 97syl2anc 585 . . . . . . . . . . . . . . 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 408 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ Β¬ 𝑄 ≀ 𝑋) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
102101adantrl 715 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
103102adantrr 716 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 )
1044, 5, 61latmle2 18418 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (𝑃 ∨ 𝑄) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑃 ∨ 𝑄))
10531, 3, 68, 104syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑃 ∨ 𝑄))
1064, 15latjcom 18400 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐡 ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
10731, 66, 34, 106syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
108105, 107breqtrd 5175 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃))
109108adantr 482 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃))
11030adantr 482 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
111 simpr3 1197 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ 𝑄 ∈ 𝐡)
112 simpr1 1195 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴)
1134, 7atbase 38159 . . . . . . . . . . . . . 14 ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
114112, 113syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡)
1154, 61latmcom 18416 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐡) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄))
116110, 111, 114, 115syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ (𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄))
117116eqeq1d 2735 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡)) β†’ ((𝑄(meetβ€˜πΎ)(𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))) = 0 ↔ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄) = 0 ))
1184, 5, 15, 61, 6, 7hlexch3 38262 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐡) ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))(meetβ€˜πΎ)𝑄) = 0 ) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ (𝑄 ∨ 𝑃) β†’ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
1191183expia 1122 . . . . . . . . . . 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 513 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄))) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
123122ex 414 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
12464, 123jcad 514 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))))
125 breq1 5152 . . . . . . . 8 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (π‘Ÿ ≀ 𝑋 ↔ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋))
126 oveq2 7417 . . . . . . . . 9 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (𝑄 ∨ π‘Ÿ) = (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))
127126breq2d 5161 . . . . . . . 8 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ (𝑃 ≀ (𝑄 ∨ π‘Ÿ) ↔ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)))))
128125, 127anbi12d 632 . . . . . . 7 (π‘Ÿ = (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) β†’ ((π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)) ↔ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))))
129128rspcev 3613 . . . . . 6 (((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄)) ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ (𝑋(meetβ€˜πΎ)(𝑃 ∨ 𝑄))))) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))
130124, 129syl6 35 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
131130expd 417 . . . 4 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑃 β‰  𝑄 ∧ Β¬ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13260, 131biimtrid 241 . . 3 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) β†’ (𝑃 ≀ (𝑋 ∨ 𝑄) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13356, 132syl7 74 . 2 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ (Β¬ (𝑃 = 𝑄 ∨ 𝑄 ≀ 𝑋) β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ)))))
13429, 55, 133ecase3d 1033 1 ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐡 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑋 β‰  0 ∧ 𝑃 ≀ (𝑋 ∨ 𝑄)) β†’ βˆƒπ‘Ÿ ∈ 𝐴 (π‘Ÿ ≀ 𝑋 ∧ 𝑃 ≀ (𝑄 ∨ π‘Ÿ))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆƒwrex 3071   class class class wbr 5149  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  lecple 17204  joincjn 18264  meetcmee 18265  0.cp0 18376  Latclat 18384  OPcops 38042  Atomscatm 38133  AtLatcal 38134  HLchlt 38220
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 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-proset 18248  df-poset 18266  df-plt 18283  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-p0 18378  df-lat 18385  df-clat 18452  df-oposet 38046  df-ol 38048  df-oml 38049  df-covers 38136  df-ats 38137  df-atl 38168  df-cvlat 38192  df-hlat 38221
This theorem is referenced by:  cvrat42  38315  ps-2  38349
  Copyright terms: Public domain W3C validator