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

Metamath Proof Explorer

Theorem 4atlem12

Description: Lemma for 4at . Combine all four possible cases. (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
4at.j ⊢ ∨ = ( join ‘ 𝐾 )
4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4atlem12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
5 4 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
6 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9 6 8 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
11 7 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑇 ∈ 𝐴 )
14 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑈 ∈ 𝐴 )
15 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
16 4 13 14 15 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
17 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑉 ∈ 𝐴 )
18 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑊 ∈ 𝐴 )
19 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
20 4 17 18 19 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
21 7 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
22 5 16 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
23 7 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
24 5 9 12 22 23 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
25 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
26 7 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
27 25 26 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
28 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
29 7 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
31 7 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
32 5 27 30 22 31 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
33 24 32 anbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
34 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
35 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
37 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
38 4 25 28 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
39 7 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
40 5 36 38 22 39 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
41 33 40 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
42 simp1l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
43 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
44 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) )
45 simp3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
46 1 2 3 4atlem12b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
47 42 43 44 45 46 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
48 47 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
49 7 2 latj4rot ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑃 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
50 5 12 27 30 9 49 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑃 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
51 50 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑃 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
52 4 10 25 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
53 28 6 13 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
54 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) )
55 52 53 54 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
56 55 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
57 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
58 1 2 3 4noncolr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
59 34 25 28 57 58 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
60 59 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
61 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) )
62 simprlr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
63 simprrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
64 62 63 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
65 simprrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
66 simprll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
67 64 65 66 jca32 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
68 67 3adant2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
69 1 2 3 4atlem12b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑃 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
70 56 60 61 68 69 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ ( 𝑆 ∨ 𝑃 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
71 51 70 eqtr3d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
72 71 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
73 48 72 jaod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
74 7 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∨ ( 𝑃 ∨ 𝑄 ) ) )
75 5 36 38 74 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∨ ( 𝑃 ∨ 𝑄 ) ) )
76 75 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∨ ( 𝑃 ∨ 𝑄 ) ) )
77 4 25 28 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
78 6 10 13 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
79 77 78 54 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
80 79 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
81 1 2 3 4noncolr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ ¬ 𝑄 ≤ ( ( 𝑅 ∨ 𝑆 ) ∨ 𝑃 ) ) )
82 34 25 28 57 81 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ ¬ 𝑄 ≤ ( ( 𝑅 ∨ 𝑆 ) ∨ 𝑃 ) ) )
83 82 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ ¬ 𝑄 ≤ ( ( 𝑅 ∨ 𝑆 ) ∨ 𝑃 ) ) )
84 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) )
85 simprr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
86 simprl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
87 85 86 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
88 87 3adant2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
89 1 2 3 4atlem12b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ ¬ 𝑄 ≤ ( ( 𝑅 ∨ 𝑆 ) ∨ 𝑃 ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
90 80 83 84 88 89 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
91 76 90 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
92 91 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
93 7 2 latj4rot ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
94 5 9 12 27 30 93 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
95 94 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
96 4 28 6 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
97 10 25 13 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) )
98 96 97 54 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
99 98 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
100 1 2 3 4noncolr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) )
101 34 25 28 57 100 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) )
102 101 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) )
103 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) )
104 65 66 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
105 104 62 63 jca32 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
106 105 3adant2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
107 1 2 3 4atlem12b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( ( 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
108 99 102 103 106 107 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
109 95 108 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
110 109 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
111 92 110 jaod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
112 25 28 14 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) )
113 17 18 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) )
114 1 2 3 4atlem3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∨ ( ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
115 34 112 113 57 114 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑄 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ∨ ( ¬ 𝑅 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
116 73 111 115 mpjaod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
117 41 116 sylbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )