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

Metamath Proof Explorer

Theorem dalawlem11

Description: Lemma for dalaw . First part of dalawlem13 . (Contributed by NM, 17-Sep-2012)

Ref Expression
Hypotheses dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion dalawlem11 ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
7 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
8 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
9 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
10 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
11 6 8 9 10 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
13 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ∈ 𝐴 )
14 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
15 6 12 13 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
16 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
17 7 11 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
18 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
19 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
20 6 9 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
21 5 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
22 7 11 15 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
23 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
24 5 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25 9 24 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
26 5 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
27 18 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
28 5 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → 𝑄 ≤ ( 𝑄 ∨ 𝑅 ) )
29 7 25 27 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑄 ≤ ( 𝑄 ∨ 𝑅 ) )
30 5 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31 8 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
33 7 31 25 20 32 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
34 23 29 33 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑄 ∨ 𝑅 ) )
35 5 1 7 17 11 20 22 34 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) )
36 5 4 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
37 13 36 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
38 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
39 7 11 37 38 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
40 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
41 7 39 15 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
42 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
43 6 18 8 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
44 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ∈ 𝐴 )
45 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
46 6 44 12 45 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
47 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
48 7 43 46 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
49 5 4 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
50 44 49 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
51 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
52 7 48 50 51 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
53 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
54 7 52 37 53 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
55 5 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
56 7 11 37 55 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
57 5 1 3 latmlem1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
58 7 11 39 15 57 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
59 56 58 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
60 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
61 7 11 37 60 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
62 5 1 2 3 4 atmod2i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ 𝑇 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
63 6 12 39 37 61 62 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ 𝑇 ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
64 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
65 6 9 13 64 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
66 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
67 6 8 12 66 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
68 5 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) )
69 7 65 67 68 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) )
70 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) )
71 69 70 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑅 ∨ 𝑈 ) )
72 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
73 7 65 67 72 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
74 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
75 6 18 44 74 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
76 5 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) ) )
77 7 73 75 31 76 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) ) )
78 71 77 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) )
79 5 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
80 12 79 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
81 5 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
82 7 31 80 81 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
83 5 1 2 3 4 atmod1i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) = ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) )
84 6 8 65 67 82 83 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) = ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) )
85 2 4 hlatjass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑈 ) = ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) )
86 6 8 18 44 85 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑈 ) = ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) )
87 2 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑃 ) )
88 6 8 18 87 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑃 ) )
89 88 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑈 ) = ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) )
90 86 89 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( 𝑅 ∨ 𝑈 ) ) = ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) )
91 78 84 90 3brtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) )
92 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑈 ∨ 𝑆 ) )
93 7 50 80 92 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ≤ ( 𝑈 ∨ 𝑆 ) )
94 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
95 7 31 65 94 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) )
96 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
97 7 95 67 96 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
98 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
99 7 43 50 98 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
100 5 1 3 latmlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ 𝑆 ≤ ( 𝑈 ∨ 𝑆 ) ) → ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
101 7 97 99 80 46 100 syl122anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ 𝑆 ≤ ( 𝑈 ∨ 𝑆 ) ) → ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
102 91 93 101 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ ( 𝑈 ∨ 𝑆 ) ) )
103 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
104 6 103 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝐾 ∈ OL )
105 5 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) = ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) ) )
106 104 95 67 80 105 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) = ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) ) )
107 2 4 hlatjass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) )
108 6 8 9 13 107 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) )
109 108 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
110 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
111 7 31 80 110 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
112 5 1 3 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) = 𝑆 ) )
113 7 80 67 112 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) = 𝑆 ) )
114 111 113 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) = 𝑆 )
115 109 114 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑆 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) )
116 106 115 eqtr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) = ( ( ( 𝑃 ∨ ( 𝑄 ∨ 𝑇 ) ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∧ 𝑆 ) )
117 5 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑈 ≤ ( 𝑈 ∨ 𝑆 ) )
118 7 50 80 117 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑈 ∨ 𝑆 ) )
119 5 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ ( 𝑈 ∨ 𝑆 ) ) → ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) = ( ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ ( 𝑈 ∨ 𝑆 ) ) )
120 6 44 43 46 118 119 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) = ( ( ( 𝑅 ∨ 𝑃 ) ∨ 𝑈 ) ∧ ( 𝑈 ∨ 𝑆 ) ) )
121 102 116 120 3brtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) )
122 5 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
123 7 39 80 122 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
124 5 1 2 latjlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ 𝑇 ) ≤ ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) ) )
125 7 123 52 37 124 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ≤ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ 𝑇 ) ≤ ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) ) )
126 121 125 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ 𝑇 ) ≤ ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) )
127 63 126 eqbrtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) )
128 5 1 7 17 41 54 59 127 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) )
129 5 2 latj31 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
130 7 48 50 37 129 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∨ 𝑈 ) ∨ 𝑇 ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
131 128 130 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
132 5 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
133 6 13 44 132 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
134 5 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ∈ ( Base ‘ 𝐾 ) )
135 7 133 48 134 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ∈ ( Base ‘ 𝐾 ) )
136 5 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) )
137 7 17 20 135 136 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) )
138 35 131 137 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
139 5 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ≤ ( 𝑅 ∨ 𝑃 ) )
140 7 43 46 139 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ≤ ( 𝑅 ∨ 𝑃 ) )
141 5 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → 𝑅 ≤ ( 𝑄 ∨ 𝑅 ) )
142 7 25 27 141 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → 𝑅 ≤ ( 𝑄 ∨ 𝑅 ) )
143 5 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑅 ∨ 𝑃 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
144 7 27 31 20 143 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑅 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ ( 𝑅 ∨ 𝑃 ) ≤ ( 𝑄 ∨ 𝑅 ) ) )
145 142 23 144 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑃 ) ≤ ( 𝑄 ∨ 𝑅 ) )
146 5 1 7 48 43 20 140 145 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ≤ ( 𝑄 ∨ 𝑅 ) )
147 5 1 2 3 4 llnmod2i2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) = ( ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
148 6 20 48 13 44 146 147 syl321anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) = ( ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
149 138 148 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )