Metamath Proof Explorer

Theorem 4atlem10

Description: Lemma for 4at . Combine both possible cases. (Contributed by NM, 9-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
5 4 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
6 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
9 6 8 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
10 simp21r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
11 7 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
13 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
14 13 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
15 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑉 ∈ 𝐴 )
16 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑊 ∈ 𝐴 )
17 7 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
18 4 15 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
19 7 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑉 ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
20 5 14 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
21 7 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
22 5 9 12 20 21 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ↔ ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
23 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
24 6 10 15 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) )
25 24 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) )
26 16 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑊 ∈ 𝐴 )
27 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) )
28 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
29 28 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
30 26 27 29 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
31 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
32 1 2 3 4atlem10b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
33 23 25 30 31 32 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
34 33 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
35 2 3 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑆 ) )
36 4 10 6 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑆 ) )
37 36 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
38 37 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
39 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
40 10 6 15 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) )
41 40 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) )
42 16 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑊 ∈ 𝐴 )
43 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) )
44 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
45 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
46 44 45 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
47 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
48 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
49 1 2 3 4atlem0a ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
50 4 46 47 48 28 49 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
51 50 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
52 42 43 51 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) )
53 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
54 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
55 53 54 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
56 55 3adant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
57 1 2 3 4atlem10b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ) ∧ ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
58 39 41 52 56 57 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑅 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
59 38 58 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
60 59 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) )
61 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
62 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
63 1 2 3 4atlem3b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ) )
64 61 6 10 16 62 63 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∨ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ) )
65 34 60 64 mpjaod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
66 22 65 sylbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑅 ∨ 𝑆 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )