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

Metamath Proof Explorer

Theorem 2llnjaN

Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN in terms of atoms). (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnja.l ⊢ ≤ = ( le ‘ 𝐾 )
2llnja.j ⊢ ∨ = ( join ‘ 𝐾 )
2llnja.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2llnja.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
2llnja.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2llnjaN ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2llnja.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2llnja.j ⊢ ∨ = ( join ‘ 𝐾 )
3 2llnja.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 2llnja.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 2llnja.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝐾 ∈ Lat )
9 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑄 ∈ 𝐴 )
10 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑅 ∈ 𝐴 )
11 6 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
12 7 9 10 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
13 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ 𝐴 )
14 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ 𝐴 )
15 6 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
16 7 13 14 15 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
17 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
18 8 12 16 17 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
19 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ 𝑃 )
20 6 5 lplnbase ⊢ ( 𝑊 ∈ 𝑃 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 )
23 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 )
24 6 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ≤ 𝑊 ) )
25 8 12 16 21 24 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ≤ 𝑊 ) )
26 22 23 25 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ≤ 𝑊 )
27 6 3 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
28 14 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
29 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
30 8 12 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
31 6 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
32 13 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
33 6 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) )
34 8 32 28 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) )
35 6 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
36 8 28 16 12 35 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
37 34 36 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
38 6 1 8 30 18 21 37 26 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 )
39 38 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 )
40 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
41 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
42 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
43 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑇 ∈ 𝐴 )
44 simp123 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ≠ 𝑅 )
45 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) )
46 simpl3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
47 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) )
48 6 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
49 8 32 28 12 48 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
50 49 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
51 50 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
52 46 47 51 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) )
53 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) )
54 1 2 3 ps-1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 𝑄 ∨ 𝑅 ) ) )
55 7 53 9 10 54 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 𝑄 ∨ 𝑅 ) ) )
56 55 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 𝑄 ∨ 𝑅 ) ) )
57 56 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 𝑄 ∨ 𝑅 ) ) )
58 52 57 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑆 ∨ 𝑇 ) = ( 𝑄 ∨ 𝑅 ) )
59 58 eqcomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑆 ∨ 𝑇 ) )
60 59 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑆 ∨ 𝑇 ) ) )
61 60 necon3ad ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) → ¬ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) )
62 45 61 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) )
63 1 2 3 5 lplni2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑃 )
64 40 41 42 43 44 62 63 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑃 )
65 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑊 ∈ 𝑃 )
66 1 5 lplncmp ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃 ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 ) )
67 40 64 65 66 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ 𝑊 ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 ) )
68 39 67 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) = 𝑊 )
69 37 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑇 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
70 68 69 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑊 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
71 70 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) → 𝑊 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
72 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
73 8 12 32 72 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
74 6 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
75 8 32 28 74 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
76 6 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
77 8 32 16 12 76 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
78 75 77 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
79 6 1 8 73 18 21 78 26 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 )
80 79 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 )
81 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
82 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
83 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
84 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑆 ∈ 𝐴 )
85 simp123 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ≠ 𝑅 )
86 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
87 1 2 3 5 lplni2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
88 81 82 83 84 85 86 87 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
89 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑊 ∈ 𝑃 )
90 1 5 lplncmp ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃 ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 ) )
91 81 88 89 90 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ 𝑊 ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 ) )
92 80 91 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = 𝑊 )
93 78 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
94 92 93 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑊 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
95 94 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) → 𝑊 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ) )
96 71 95 pm2.61d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → 𝑊 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) )
97 6 1 8 18 21 26 96 latasymd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ( 𝑄 ∨ 𝑅 ) ≤ 𝑊 ∧ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ ( 𝑄 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = 𝑊 )