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

Metamath Proof Explorer

Theorem cdleme23c

Description: Part of proof of Lemma E in Crawley p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012)

Ref Expression
Hypotheses cdleme23.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdleme23.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme23.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme23.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme23.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme23.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme23.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) )
Assertion cdleme23c ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdleme23.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdleme23.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdleme23.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdleme23.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdleme23.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme23.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme23.v ⊢ 𝑉 = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) )
8 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
10 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ∈ 𝐴 )
11 1 5 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵 )
12 10 11 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ∈ 𝐵 )
13 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ∈ 𝐴 )
14 1 5 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ 𝐵 )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ∈ 𝐵 )
16 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
17 9 12 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) )
18 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
19 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
20 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
21 19 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
22 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
23 9 18 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
24 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → 𝑆 ≤ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) )
25 9 12 23 24 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) )
26 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
27 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
28 26 27 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) )
29 25 28 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) )
30 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
31 8 10 13 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 )
32 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑇 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
33 9 15 23 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
34 1 2 4 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) ) → ( ( 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ↔ 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
35 9 12 31 33 34 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑆 ≤ ( 𝑆 ∨ 𝑇 ) ∧ 𝑆 ≤ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ↔ 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
36 17 29 35 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
37 7 oveq2i ⊢ ( 𝑇 ∨ 𝑉 ) = ( 𝑇 ∨ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) )
38 1 2 3 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) )
39 9 12 15 38 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) )
40 1 2 3 4 5 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑇 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑇 ) ) → ( 𝑇 ∨ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
41 8 13 31 23 39 40 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑇 ∨ ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑋 ∧ 𝑊 ) ) ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
42 37 41 eqtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑇 ∨ 𝑉 ) = ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
43 36 42 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑆 ≠ 𝑇 ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑇 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑆 ≤ ( 𝑇 ∨ 𝑉 ) )