Metamath Proof Explorer

Theorem cdleme22b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. t <_ p \/ q. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdleme22b ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐾 ∈ HL )
7 simp1r1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ∈ 𝐴 )
8 simp1r2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑇 ∈ 𝐴 )
9 simp1r3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ≠ 𝑇 )
10 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
11 2 4 10 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ 𝑆 ≠ 𝑇 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
12 6 7 8 9 11 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
13 4 10 llnneat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 )
14 6 12 13 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 )
15 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
16 15 10 llnn0 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) )
17 6 12 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) )
18 14 17 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) ) )
19 df-ne ⊢ ( ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) ↔ ¬ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) )
20 19 anbi2i ⊢ ( ( ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) ) ↔ ( ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∧ ¬ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
21 pm4.56 ⊢ ( ( ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∧ ¬ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) ↔ ¬ ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
22 20 21 bitri ⊢ ( ( ¬ ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≠ ( 0. ‘ 𝐾 ) ) ↔ ¬ ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
23 18 22 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
24 simp3r2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )
25 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑉 ∈ 𝐴 )
26 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) )
27 6 8 25 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) )
28 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐾 ∈ Lat )
29 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
30 29 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
31 7 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
32 29 4 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
33 8 32 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
34 29 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
35 6 8 25 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
36 29 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ) )
37 28 31 33 35 36 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑇 ≤ ( 𝑇 ∨ 𝑉 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ) )
38 24 27 37 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) )
39 38 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) )
40 simp3r3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
41 40 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
42 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
43 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑃 ∈ 𝐴 )
44 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑄 ∈ 𝐴 )
45 29 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
46 6 43 44 45 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
47 29 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
48 28 31 33 46 47 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
49 48 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
50 41 42 49 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) )
51 29 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
52 6 7 8 51 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
53 29 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
54 28 52 35 46 53 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
55 54 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
56 39 50 55 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
57 56 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) )
58 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
59 6 58 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐾 ∈ OP )
60 59 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝐾 ∈ OP )
61 52 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
62 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
63 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) )
64 29 1 15 4 leat3 ⊢ ( ( ( 𝐾 ∈ OP ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
65 60 61 62 63 64 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
66 65 exp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) ) ) )
67 breq2 ⊢ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ ( 0. ‘ 𝐾 ) ) )
68 67 biimpa ⊢ ( ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ∨ 𝑇 ) ≤ ( 0. ‘ 𝐾 ) )
69 29 1 15 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
70 59 52 69 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
71 68 70 imbitrid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
72 71 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) )
73 72 olcd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ∧ ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) )
74 73 exp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) ) ) )
75 simp3r1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) )
76 2 3 15 4 2atmat0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∨ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
77 6 8 25 43 44 75 76 syl33anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∨ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) = ( 0. ‘ 𝐾 ) ) )
78 66 74 77 mpjaod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ≤ ( ( 𝑇 ∨ 𝑉 ) ∧ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) ) )
79 57 78 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ( 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) → ( ( 𝑆 ∨ 𝑇 ) ∈ 𝐴 ∨ ( 𝑆 ∨ 𝑇 ) = ( 0. ‘ 𝐾 ) ) ) )
80 23 79 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ ( ( 𝑇 ∨ 𝑉 ) ≠ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )