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

Metamath Proof Explorer

Theorem 3dimlem3OLDN

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dimlem3OLDN ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ≠ 𝑄 )
5 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
6 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝐾 ∈ HL )
7 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
8 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ∈ 𝐴 )
9 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑄 ∈ 𝐴 )
10 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑄 ≠ 𝑅 )
11 10 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑅 ≠ 𝑄 )
12 2 1 3 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑄 ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
13 6 7 8 9 11 12 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
14 1 3 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
15 6 9 7 14 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
16 15 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
17 13 16 sylibrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
18 5 17 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
19 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
20 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
21 6 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝐾 ∈ Lat )
22 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
23 22 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
24 9 23 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25 22 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
26 7 25 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
27 22 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
28 8 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
29 22 1 latjrot ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
30 21 24 26 28 29 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
31 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
32 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑆 ∈ 𝐴 )
33 22 1 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
34 6 9 7 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
35 22 2 1 3 hlexchb1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
36 6 8 32 34 5 35 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
37 31 36 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
38 30 37 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
39 38 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
40 19 39 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
41 4 18 40 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )