This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lplnexllnN

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.)

Ref Expression
Hypotheses lplnexat.l ⊢ ≤ = ( le ‘ 𝐾 )
lplnexat.j ⊢ ∨ = ( join ‘ 𝐾 )
lplnexat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lplnexat.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
lplnexat.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnexllnN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 lplnexat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplnexat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lplnexat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lplnexat.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 lplnexat.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ 𝑃 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → 𝐾 ∈ HL )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 5 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
10 6 9 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
11 8 1 2 3 4 5 islpln3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑧 ∈ 𝑁 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) )
12 7 10 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑧 ∈ 𝑁 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) )
13 6 12 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ∃ 𝑧 ∈ 𝑁 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) )
14 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ HL )
15 simpr2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ∈ 𝑁 )
16 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑄 ∈ 𝐴 )
17 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑄 ≤ 𝑧 )
18 1 2 3 4 llnexatN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝑁 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑧 ) → ∃ 𝑠 ∈ 𝐴 ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) )
19 14 15 16 17 18 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) )
20 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝐾 ∈ HL )
21 simp22r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑟 ∈ 𝐴 )
22 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑠 ∈ 𝐴 )
23 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑄 ∈ 𝐴 )
24 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ¬ 𝑟 ≤ 𝑧 )
25 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑧 = ( 𝑄 ∨ 𝑠 ) )
26 25 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ( 𝑟 ≤ 𝑧 ↔ 𝑟 ≤ ( 𝑄 ∨ 𝑠 ) ) )
27 24 26 mtbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ¬ 𝑟 ≤ ( 𝑄 ∨ 𝑠 ) )
28 1 2 3 atnlej2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ¬ 𝑟 ≤ ( 𝑄 ∨ 𝑠 ) ) → 𝑟 ≠ 𝑠 )
29 20 21 23 22 27 28 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑟 ≠ 𝑠 )
30 2 3 4 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑠 ) → ( 𝑟 ∨ 𝑠 ) ∈ 𝑁 )
31 20 21 22 29 30 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ( 𝑟 ∨ 𝑠 ) ∈ 𝑁 )
32 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑄 ≠ 𝑠 )
33 1 2 3 hlatcon2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑠 ∧ ¬ 𝑟 ≤ ( 𝑄 ∨ 𝑠 ) ) ) → ¬ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) )
34 20 23 22 21 32 27 33 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ¬ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) )
35 simp23r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑋 = ( 𝑧 ∨ 𝑟 ) )
36 25 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ( 𝑧 ∨ 𝑟 ) = ( ( 𝑄 ∨ 𝑠 ) ∨ 𝑟 ) )
37 20 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝐾 ∈ Lat )
38 8 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
39 23 38 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
40 8 3 atbase ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ( Base ‘ 𝐾 ) )
41 22 40 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑠 ∈ ( Base ‘ 𝐾 ) )
42 8 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
43 21 42 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
44 8 2 latj31 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ∨ 𝑠 ) ∨ 𝑟 ) = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) )
45 37 39 41 43 44 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ( ( 𝑄 ∨ 𝑠 ) ∨ 𝑟 ) = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) )
46 35 36 45 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → 𝑋 = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) )
47 breq2 ⊢ ( 𝑦 = ( 𝑟 ∨ 𝑠 ) → ( 𝑄 ≤ 𝑦 ↔ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) ) )
48 47 notbid ⊢ ( 𝑦 = ( 𝑟 ∨ 𝑠 ) → ( ¬ 𝑄 ≤ 𝑦 ↔ ¬ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) ) )
49 oveq1 ⊢ ( 𝑦 = ( 𝑟 ∨ 𝑠 ) → ( 𝑦 ∨ 𝑄 ) = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) )
50 49 eqeq2d ⊢ ( 𝑦 = ( 𝑟 ∨ 𝑠 ) → ( 𝑋 = ( 𝑦 ∨ 𝑄 ) ↔ 𝑋 = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) ) )
51 48 50 anbi12d ⊢ ( 𝑦 = ( 𝑟 ∨ 𝑠 ) → ( ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ↔ ( ¬ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) ) ) )
52 51 rspcev ⊢ ( ( ( 𝑟 ∨ 𝑠 ) ∈ 𝑁 ∧ ( ¬ 𝑄 ≤ ( 𝑟 ∨ 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ∨ 𝑠 ) ∨ 𝑄 ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )
53 31 34 46 52 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )
54 53 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( ( 𝑠 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) )
55 54 expd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( 𝑠 ∈ 𝐴 → ( ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) ) )
56 55 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( ∃ 𝑠 ∈ 𝐴 ( 𝑄 ≠ 𝑠 ∧ 𝑧 = ( 𝑄 ∨ 𝑠 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) )
57 19 56 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )
58 57 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ( 𝑄 ≤ 𝑧 → ( ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) ) ) )
59 simpr2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ∈ 𝑁 )
60 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ¬ 𝑄 ≤ 𝑧 )
61 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ HL )
62 61 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ Lat )
63 8 4 llnbase ⊢ ( 𝑧 ∈ 𝑁 → 𝑧 ∈ ( Base ‘ 𝐾 ) )
64 59 63 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
65 simpr2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ 𝐴 )
66 65 42 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
67 8 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ≤ ( 𝑧 ∨ 𝑟 ) )
68 62 64 66 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ≤ ( 𝑧 ∨ 𝑟 ) )
69 simpr3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑋 = ( 𝑧 ∨ 𝑟 ) )
70 68 69 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ≤ 𝑋 )
71 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑄 ≤ 𝑋 )
72 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑄 ∈ 𝐴 )
73 72 38 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
74 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑋 ∈ 𝑃 )
75 74 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
76 8 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑧 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ↔ ( 𝑧 ∨ 𝑄 ) ≤ 𝑋 ) )
77 62 64 73 75 76 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( ( 𝑧 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋 ) ↔ ( 𝑧 ∨ 𝑄 ) ≤ 𝑋 ) )
78 70 71 77 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( 𝑧 ∨ 𝑄 ) ≤ 𝑋 )
79 8 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
80 62 64 73 79 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( 𝑧 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
81 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
82 8 1 2 81 3 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑄 ≤ 𝑧 ↔ 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ∨ 𝑄 ) ) )
83 61 64 72 82 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( ¬ 𝑄 ≤ 𝑧 ↔ 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ∨ 𝑄 ) ) )
84 60 83 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ∨ 𝑄 ) )
85 8 81 4 5 lplni ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑧 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ∨ 𝑄 ) ) → ( 𝑧 ∨ 𝑄 ) ∈ 𝑃 )
86 61 80 59 84 85 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( 𝑧 ∨ 𝑄 ) ∈ 𝑃 )
87 1 5 lplncmp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑧 ∨ 𝑄 ) ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑧 ∨ 𝑄 ) ≤ 𝑋 ↔ ( 𝑧 ∨ 𝑄 ) = 𝑋 ) )
88 61 86 74 87 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( ( 𝑧 ∨ 𝑄 ) ≤ 𝑋 ↔ ( 𝑧 ∨ 𝑄 ) = 𝑋 ) )
89 78 88 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ( 𝑧 ∨ 𝑄 ) = 𝑋 )
90 89 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → 𝑋 = ( 𝑧 ∨ 𝑄 ) )
91 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑄 ≤ 𝑦 ↔ 𝑄 ≤ 𝑧 ) )
92 91 notbid ⊢ ( 𝑦 = 𝑧 → ( ¬ 𝑄 ≤ 𝑦 ↔ ¬ 𝑄 ≤ 𝑧 ) )
93 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∨ 𝑄 ) = ( 𝑧 ∨ 𝑄 ) )
94 93 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑋 = ( 𝑦 ∨ 𝑄 ) ↔ 𝑋 = ( 𝑧 ∨ 𝑄 ) ) )
95 92 94 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ↔ ( ¬ 𝑄 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑄 ) ) ) )
96 95 rspcev ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑄 ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )
97 59 60 90 96 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( ¬ 𝑄 ≤ 𝑧 ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )
98 97 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ( ¬ 𝑄 ≤ 𝑧 → ( ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) ) ) )
99 58 98 pm2.61d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ( ( 𝑧 ∈ 𝑁 ∧ 𝑟 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) ) )
100 99 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ( ∃ 𝑧 ∈ 𝑁 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑧 ∧ 𝑋 = ( 𝑧 ∨ 𝑟 ) ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) ) )
101 13 100 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑁 ( ¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑄 ) ) )