Metamath Proof Explorer

Theorem 3dim3

Description: Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3dim2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) )
5 4 3adant3r1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) )
6 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑣 ∈ 𝐴 )
7 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ HL )
9 simp1r2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑄 ∈ 𝐴 )
10 1 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
12 11 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
13 12 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) )
14 7 13 mtbird ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) )
15 oveq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
16 15 oveq1d ⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) )
17 16 breq2d ⊢ ( 𝑃 = 𝑄 → ( 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) )
18 17 notbid ⊢ ( 𝑃 = 𝑄 → ( ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) )
19 18 biimparc ⊢ ( ( ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
20 14 19 sylan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
21 breq1 ⊢ ( 𝑠 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
22 21 notbid ⊢ ( 𝑠 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
23 22 rspcev ⊢ ( ( 𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
24 6 20 23 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
25 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑣 ∈ 𝐴 )
26 25 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑣 ∈ 𝐴 )
27 7 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) )
28 1 3 hlatjass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) )
29 28 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) )
30 29 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) )
31 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ Lat )
32 simp1r1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑃 ∈ 𝐴 )
33 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
34 33 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
35 32 34 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
36 simp1r3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑅 ∈ 𝐴 )
37 33 1 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
38 8 9 36 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
39 31 35 38 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
40 39 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
41 33 2 1 latleeqj1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) ) )
42 40 41 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) ) )
43 42 biimpa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) )
44 30 43 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
45 44 breq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) )
46 27 45 mtbird ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
47 26 46 23 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
48 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑤 ∈ 𝐴 )
49 48 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑤 ∈ 𝐴 )
50 8 32 9 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
51 50 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
52 36 25 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
53 52 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
54 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) )
55 54 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) )
56 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
57 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) )
58 1 2 3 3dimlem3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
59 51 53 55 56 57 58 syl113anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
60 breq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
61 60 notbid ⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
62 61 rspcev ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
63 49 59 62 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
64 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑣 ∈ 𝐴 )
65 64 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑣 ∈ 𝐴 )
66 50 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
67 52 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
68 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) )
69 68 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) )
70 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
71 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) )
72 1 2 3 3dimlem4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
73 66 67 69 70 71 72 syl113anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
74 65 73 23 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
75 63 74 pm2.61dan ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
76 47 75 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
77 24 76 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
78 77 3exp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )
79 78 rexlimdvv ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
80 5 79 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )