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

Theorem lplnexllnN 38948
Description: Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
lplnexat.l ≀ = (leβ€˜πΎ)
lplnexat.j ∨ = (joinβ€˜πΎ)
lplnexat.a 𝐴 = (Atomsβ€˜πΎ)
lplnexat.n 𝑁 = (LLinesβ€˜πΎ)
lplnexat.p 𝑃 = (LPlanesβ€˜πΎ)
Assertion
Ref Expression
lplnexllnN (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
Distinct variable groups:   𝑦, ∨   𝑦, ≀   𝑦,𝑁   𝑦,𝑄   𝑦,𝑋
Allowed substitution hints:   𝐴(𝑦)   𝑃(𝑦)   𝐾(𝑦)

Proof of Theorem lplnexllnN
Dummy variables 𝑠 π‘Ÿ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1189 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ 𝑋 ∈ 𝑃)
2 simpl1 1188 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ 𝐾 ∈ HL)
3 eqid 2726 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
4 lplnexat.p . . . . . 6 𝑃 = (LPlanesβ€˜πΎ)
53, 4lplnbase 38918 . . . . 5 (𝑋 ∈ 𝑃 β†’ 𝑋 ∈ (Baseβ€˜πΎ))
61, 5syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
7 lplnexat.l . . . . 5 ≀ = (leβ€˜πΎ)
8 lplnexat.j . . . . 5 ∨ = (joinβ€˜πΎ)
9 lplnexat.a . . . . 5 𝐴 = (Atomsβ€˜πΎ)
10 lplnexat.n . . . . 5 𝑁 = (LLinesβ€˜πΎ)
113, 7, 8, 9, 10, 4islpln3 38917 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ (Baseβ€˜πΎ)) β†’ (𝑋 ∈ 𝑃 ↔ βˆƒπ‘§ ∈ 𝑁 βˆƒπ‘Ÿ ∈ 𝐴 (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))))
122, 6, 11syl2anc 583 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ (𝑋 ∈ 𝑃 ↔ βˆƒπ‘§ ∈ 𝑁 βˆƒπ‘Ÿ ∈ 𝐴 (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))))
131, 12mpbid 231 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ βˆƒπ‘§ ∈ 𝑁 βˆƒπ‘Ÿ ∈ 𝐴 (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))
14 simpll1 1209 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝐾 ∈ HL)
15 simpr2l 1229 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧 ∈ 𝑁)
16 simpll3 1211 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑄 ∈ 𝐴)
17 simpr1 1191 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑄 ≀ 𝑧)
187, 8, 9, 10llnexatN 38905 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑧 ∈ 𝑁 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑧) β†’ βˆƒπ‘  ∈ 𝐴 (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))
1914, 15, 16, 17, 18syl31anc 1370 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ βˆƒπ‘  ∈ 𝐴 (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))
20 simp1l1 1263 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝐾 ∈ HL)
21 simp22r 1290 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ π‘Ÿ ∈ 𝐴)
22 simp3l 1198 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑠 ∈ 𝐴)
23 simp1l3 1265 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑄 ∈ 𝐴)
24 simp23l 1291 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ Β¬ π‘Ÿ ≀ 𝑧)
25 simp3rr 1244 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑧 = (𝑄 ∨ 𝑠))
2625breq2d 5153 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ (π‘Ÿ ≀ 𝑧 ↔ π‘Ÿ ≀ (𝑄 ∨ 𝑠)))
2724, 26mtbid 324 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ Β¬ π‘Ÿ ≀ (𝑄 ∨ 𝑠))
287, 8, 9atnlej2 38764 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (π‘Ÿ ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ Β¬ π‘Ÿ ≀ (𝑄 ∨ 𝑠)) β†’ π‘Ÿ β‰  𝑠)
2920, 21, 23, 22, 27, 28syl131anc 1380 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ π‘Ÿ β‰  𝑠)
308, 9, 10llni2 38896 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Ÿ ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ π‘Ÿ β‰  𝑠) β†’ (π‘Ÿ ∨ 𝑠) ∈ 𝑁)
3120, 21, 22, 29, 30syl31anc 1370 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ (π‘Ÿ ∨ 𝑠) ∈ 𝑁)
32 simp3rl 1243 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑄 β‰  𝑠)
337, 8, 9hlatcon2 38836 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ∧ π‘Ÿ ∈ 𝐴) ∧ (𝑄 β‰  𝑠 ∧ Β¬ π‘Ÿ ≀ (𝑄 ∨ 𝑠))) β†’ Β¬ 𝑄 ≀ (π‘Ÿ ∨ 𝑠))
3420, 23, 22, 21, 32, 27, 33syl132anc 1385 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ Β¬ 𝑄 ≀ (π‘Ÿ ∨ 𝑠))
35 simp23r 1292 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑋 = (𝑧 ∨ π‘Ÿ))
3625oveq1d 7420 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ (𝑧 ∨ π‘Ÿ) = ((𝑄 ∨ 𝑠) ∨ π‘Ÿ))
3720hllatd 38747 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝐾 ∈ Lat)
383, 9atbase 38672 . . . . . . . . . . . . 13 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
3923, 38syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
403, 9atbase 38672 . . . . . . . . . . . . 13 (𝑠 ∈ 𝐴 β†’ 𝑠 ∈ (Baseβ€˜πΎ))
4122, 40syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑠 ∈ (Baseβ€˜πΎ))
423, 9atbase 38672 . . . . . . . . . . . . 13 (π‘Ÿ ∈ 𝐴 β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
4321, 42syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
443, 8latj31 18452 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Baseβ€˜πΎ))) β†’ ((𝑄 ∨ 𝑠) ∨ π‘Ÿ) = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))
4537, 39, 41, 43, 44syl13anc 1369 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ ((𝑄 ∨ 𝑠) ∨ π‘Ÿ) = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))
4635, 36, 453eqtrd 2770 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ 𝑋 = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))
47 breq2 5145 . . . . . . . . . . . . 13 (𝑦 = (π‘Ÿ ∨ 𝑠) β†’ (𝑄 ≀ 𝑦 ↔ 𝑄 ≀ (π‘Ÿ ∨ 𝑠)))
4847notbid 318 . . . . . . . . . . . 12 (𝑦 = (π‘Ÿ ∨ 𝑠) β†’ (Β¬ 𝑄 ≀ 𝑦 ↔ Β¬ 𝑄 ≀ (π‘Ÿ ∨ 𝑠)))
49 oveq1 7412 . . . . . . . . . . . . 13 (𝑦 = (π‘Ÿ ∨ 𝑠) β†’ (𝑦 ∨ 𝑄) = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))
5049eqeq2d 2737 . . . . . . . . . . . 12 (𝑦 = (π‘Ÿ ∨ 𝑠) β†’ (𝑋 = (𝑦 ∨ 𝑄) ↔ 𝑋 = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄)))
5148, 50anbi12d 630 . . . . . . . . . . 11 (𝑦 = (π‘Ÿ ∨ 𝑠) β†’ ((Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)) ↔ (Β¬ 𝑄 ≀ (π‘Ÿ ∨ 𝑠) ∧ 𝑋 = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))))
5251rspcev 3606 . . . . . . . . . 10 (((π‘Ÿ ∨ 𝑠) ∈ 𝑁 ∧ (Β¬ 𝑄 ≀ (π‘Ÿ ∨ 𝑠) ∧ 𝑋 = ((π‘Ÿ ∨ 𝑠) ∨ 𝑄))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
5331, 34, 46, 52syl12anc 834 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ))) ∧ (𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
54533expia 1118 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ ((𝑠 ∈ 𝐴 ∧ (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))))
5554expd 415 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (𝑠 ∈ 𝐴 β†’ ((𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))))
5655rexlimdv 3147 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (βˆƒπ‘  ∈ 𝐴 (𝑄 β‰  𝑠 ∧ 𝑧 = (𝑄 ∨ 𝑠)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))))
5719, 56mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
58573exp2 1351 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ (𝑄 ≀ 𝑧 β†’ ((𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))))))
59 simpr2l 1229 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧 ∈ 𝑁)
60 simpr1 1191 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ Β¬ 𝑄 ≀ 𝑧)
61 simpll1 1209 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝐾 ∈ HL)
6261hllatd 38747 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝐾 ∈ Lat)
633, 10llnbase 38893 . . . . . . . . . . . 12 (𝑧 ∈ 𝑁 β†’ 𝑧 ∈ (Baseβ€˜πΎ))
6459, 63syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧 ∈ (Baseβ€˜πΎ))
65 simpr2r 1230 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ π‘Ÿ ∈ 𝐴)
6665, 42syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
673, 7, 8latlej1 18413 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑧 ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Baseβ€˜πΎ)) β†’ 𝑧 ≀ (𝑧 ∨ π‘Ÿ))
6862, 64, 66, 67syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧 ≀ (𝑧 ∨ π‘Ÿ))
69 simpr3r 1232 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑋 = (𝑧 ∨ π‘Ÿ))
7068, 69breqtrrd 5169 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧 ≀ 𝑋)
71 simplr 766 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑄 ≀ 𝑋)
72 simpll3 1211 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑄 ∈ 𝐴)
7372, 38syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
74 simpll2 1210 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑋 ∈ 𝑃)
7574, 5syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
763, 7, 8latjle12 18415 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ 𝑋 ∈ (Baseβ€˜πΎ))) β†’ ((𝑧 ≀ 𝑋 ∧ 𝑄 ≀ 𝑋) ↔ (𝑧 ∨ 𝑄) ≀ 𝑋))
7762, 64, 73, 75, 76syl13anc 1369 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ ((𝑧 ≀ 𝑋 ∧ 𝑄 ≀ 𝑋) ↔ (𝑧 ∨ 𝑄) ≀ 𝑋))
7870, 71, 77mpbi2and 709 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (𝑧 ∨ 𝑄) ≀ 𝑋)
793, 8latjcl 18404 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑧 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ)) β†’ (𝑧 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
8062, 64, 73, 79syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (𝑧 ∨ 𝑄) ∈ (Baseβ€˜πΎ))
81 eqid 2726 . . . . . . . . . . . . 13 ( β‹– β€˜πΎ) = ( β‹– β€˜πΎ)
823, 7, 8, 81, 9cvr1 38794 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑧 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ 𝐴) β†’ (Β¬ 𝑄 ≀ 𝑧 ↔ 𝑧( β‹– β€˜πΎ)(𝑧 ∨ 𝑄)))
8361, 64, 72, 82syl3anc 1368 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (Β¬ 𝑄 ≀ 𝑧 ↔ 𝑧( β‹– β€˜πΎ)(𝑧 ∨ 𝑄)))
8460, 83mpbid 231 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑧( β‹– β€˜πΎ)(𝑧 ∨ 𝑄))
853, 81, 10, 4lplni 38916 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑧 ∨ 𝑄) ∈ (Baseβ€˜πΎ) ∧ 𝑧 ∈ 𝑁) ∧ 𝑧( β‹– β€˜πΎ)(𝑧 ∨ 𝑄)) β†’ (𝑧 ∨ 𝑄) ∈ 𝑃)
8661, 80, 59, 84, 85syl31anc 1370 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (𝑧 ∨ 𝑄) ∈ 𝑃)
877, 4lplncmp 38946 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑧 ∨ 𝑄) ∈ 𝑃 ∧ 𝑋 ∈ 𝑃) β†’ ((𝑧 ∨ 𝑄) ≀ 𝑋 ↔ (𝑧 ∨ 𝑄) = 𝑋))
8861, 86, 74, 87syl3anc 1368 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ ((𝑧 ∨ 𝑄) ≀ 𝑋 ↔ (𝑧 ∨ 𝑄) = 𝑋))
8978, 88mpbid 231 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ (𝑧 ∨ 𝑄) = 𝑋)
9089eqcomd 2732 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ 𝑋 = (𝑧 ∨ 𝑄))
91 breq2 5145 . . . . . . . . 9 (𝑦 = 𝑧 β†’ (𝑄 ≀ 𝑦 ↔ 𝑄 ≀ 𝑧))
9291notbid 318 . . . . . . . 8 (𝑦 = 𝑧 β†’ (Β¬ 𝑄 ≀ 𝑦 ↔ Β¬ 𝑄 ≀ 𝑧))
93 oveq1 7412 . . . . . . . . 9 (𝑦 = 𝑧 β†’ (𝑦 ∨ 𝑄) = (𝑧 ∨ 𝑄))
9493eqeq2d 2737 . . . . . . . 8 (𝑦 = 𝑧 β†’ (𝑋 = (𝑦 ∨ 𝑄) ↔ 𝑋 = (𝑧 ∨ 𝑄)))
9592, 94anbi12d 630 . . . . . . 7 (𝑦 = 𝑧 β†’ ((Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)) ↔ (Β¬ 𝑄 ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ 𝑄))))
9695rspcev 3606 . . . . . 6 ((𝑧 ∈ 𝑁 ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ 𝑄))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
9759, 60, 90, 96syl12anc 834 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) ∧ (Β¬ 𝑄 ≀ 𝑧 ∧ (𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) ∧ (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)))) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
98973exp2 1351 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ (Β¬ 𝑄 ≀ 𝑧 β†’ ((𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))))))
9958, 98pm2.61d 179 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ ((𝑧 ∈ 𝑁 ∧ π‘Ÿ ∈ 𝐴) β†’ ((Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))))
10099rexlimdvv 3204 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ (βˆƒπ‘§ ∈ 𝑁 βˆƒπ‘Ÿ ∈ 𝐴 (Β¬ π‘Ÿ ≀ 𝑧 ∧ 𝑋 = (𝑧 ∨ π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))))
10113, 100mpd 15 1 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≀ 𝑋) β†’ βˆƒπ‘¦ ∈ 𝑁 (Β¬ 𝑄 ≀ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064   class class class wbr 5141  β€˜cfv 6537  (class class class)co 7405  Basecbs 17153  lecple 17213  joincjn 18276  Latclat 18396   β‹– ccvr 38645  Atomscatm 38646  HLchlt 38733  LLinesclln 38875  LPlanesclpl 38876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-proset 18260  df-poset 18278  df-plt 18295  df-lub 18311  df-glb 18312  df-join 18313  df-meet 18314  df-p0 18390  df-lat 18397  df-clat 18464  df-oposet 38559  df-ol 38561  df-oml 38562  df-covers 38649  df-ats 38650  df-atl 38681  df-cvlat 38705  df-hlat 38734  df-llines 38882  df-lplanes 38883
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator