Metamath Proof Explorer

Theorem 4atlem11

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

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

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 3anass ⊢ ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
5 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
6 5 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
7 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
10 7 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
11 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
12 8 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
13 11 12 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
14 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
15 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑈 ∈ 𝐴 )
16 8 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
17 5 14 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
18 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑉 ∈ 𝐴 )
19 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑊 ∈ 𝐴 )
20 8 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
21 5 18 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
22 8 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
23 6 17 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
24 8 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
25 6 10 13 23 24 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
26 25 anbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) ↔ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
27 4 26 bitrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
28 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
29 8 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
31 8 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
32 5 7 11 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
33 8 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑄 ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
34 6 30 32 23 33 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑄 ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
35 27 34 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑄 ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
36 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
37 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
38 18 19 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) )
39 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
40 1 2 3 4atlem3a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) )
41 36 37 38 39 40 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) )
42 simp1l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
43 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
44 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) )
45 simp3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
46 1 2 3 4atlem11b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
47 42 43 44 45 46 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
48 47 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
49 5 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝐾 ∈ HL )
50 14 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑃 ∈ 𝐴 )
51 28 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑄 ∈ 𝐴 )
52 7 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ∈ 𝐴 )
53 11 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ∈ 𝐴 )
54 2 3 hlatj4 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) )
55 49 50 51 52 53 54 syl122anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) )
56 49 50 52 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
57 51 53 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
58 simp1l3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) )
59 simp1r2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
60 1 2 3 4atlem0be ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑅 )
61 49 50 51 52 59 60 syl131anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑃 ≠ 𝑅 )
62 simp1r1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑃 ≠ 𝑄 )
63 1 2 3 4atlem0ae ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
64 49 50 51 52 62 59 63 syl132anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
65 simp1r3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
66 2 3 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) )
67 49 50 51 52 66 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) )
68 67 breq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) ) )
69 65 68 mtbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) )
70 61 64 69 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) ) )
71 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) )
72 simp32 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
73 simp31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
74 simp33 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
75 1 2 3 4atlem11b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑄 ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
76 56 57 58 70 71 72 73 74 75 syl323anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∨ ( 𝑄 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
77 55 76 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
78 77 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
79 8 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
80 14 79 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
81 8 2 latj4rot ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
82 6 80 30 10 13 81 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
83 2 3 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑃 ) = ( 𝑃 ∨ 𝑆 ) )
84 5 11 14 83 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ∨ 𝑃 ) = ( 𝑃 ∨ 𝑆 ) )
85 84 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑆 ∨ 𝑃 ) ∨ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
86 82 85 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
87 86 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑅 ) ) )
88 5 14 11 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
89 28 7 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
90 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) )
91 88 89 90 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
92 91 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) )
93 1 2 3 4noncolr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) )
94 36 37 39 93 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) )
95 necom ⊢ ( 𝑆 ≠ 𝑃 ↔ 𝑃 ≠ 𝑆 )
96 95 a1i ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≠ 𝑃 ↔ 𝑃 ≠ 𝑆 ) )
97 84 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ↔ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) )
98 97 notbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ↔ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) )
99 84 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) )
100 99 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ↔ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) )
101 100 notbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ↔ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) )
102 96 98 101 3anbi123d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ ( 𝑆 ∨ 𝑃 ) ∧ ¬ 𝑅 ≤ ( ( 𝑆 ∨ 𝑃 ) ∨ 𝑄 ) ) ↔ ( 𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) ) )
103 94 102 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) )
104 103 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) )
105 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) )
106 simpr3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
107 simpr1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
108 simpr2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
109 106 107 108 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
110 109 3adant2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
111 1 2 3 4atlem11b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑆 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) ∧ ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
112 92 104 105 110 111 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
113 87 112 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∧ ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
114 113 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
115 48 78 114 3jaod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ¬ 𝑄 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
116 41 115 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
117 35 116 sylbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑆 ) ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )