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

Metamath Proof Explorer

Theorem 3dim2

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

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3dim1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) )
5 4 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) )
6 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑢 ∈ 𝐴 )
7 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑣 ∈ 𝐴 )
8 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑄 ≠ 𝑢 )
9 8 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑢 ≠ 𝑄 )
10 9 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑢 ≠ 𝑄 )
11 oveq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
12 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ HL )
13 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑄 ∈ 𝐴 )
14 1 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
15 12 13 14 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
16 11 15 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∨ 𝑄 ) = 𝑄 )
17 16 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑢 ≤ 𝑄 ) )
18 17 notbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ¬ 𝑢 ≤ 𝑄 ) )
19 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
20 12 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ AtLat )
21 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑢 ∈ 𝐴 )
22 2 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑢 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑢 ≤ 𝑄 ↔ 𝑢 ≠ 𝑄 ) )
23 20 21 13 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ¬ 𝑢 ≤ 𝑄 ↔ 𝑢 ≠ 𝑄 ) )
24 23 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ¬ 𝑢 ≤ 𝑄 ↔ 𝑢 ≠ 𝑄 ) )
25 18 24 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑢 ≠ 𝑄 ) )
26 10 25 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) )
27 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) )
28 16 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) )
29 28 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ↔ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ) )
30 27 29 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) )
31 breq1 ⊢ ( 𝑟 = 𝑢 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
32 31 notbid ⊢ ( 𝑟 = 𝑢 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
33 oveq2 ⊢ ( 𝑟 = 𝑢 → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) )
34 33 breq2d ⊢ ( 𝑟 = 𝑢 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
35 34 notbid ⊢ ( 𝑟 = 𝑢 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
36 32 35 anbi12d ⊢ ( 𝑟 = 𝑢 → ( ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ↔ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) )
37 breq1 ⊢ ( 𝑠 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ↔ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
38 37 notbid ⊢ ( 𝑠 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ↔ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
39 38 anbi2d ⊢ ( 𝑠 = 𝑣 → ( ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ↔ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) )
40 36 39 rspc2ev ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
41 6 7 26 30 40 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
42 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑣 ∈ 𝐴 )
43 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑤 ∈ 𝐴 )
44 42 43 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
45 44 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
46 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
47 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) )
48 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) )
49 21 47 48 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) )
50 49 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) )
51 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → 𝑃 ≠ 𝑄 )
52 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) )
53 1 2 3 3dimlem2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
54 46 50 51 52 53 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
55 3simpc ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) → ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
56 54 55 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
57 breq1 ⊢ ( 𝑟 = 𝑣 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ) )
58 57 notbid ⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ) )
59 oveq2 ⊢ ( 𝑟 = 𝑣 → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) )
60 59 breq2d ⊢ ( 𝑟 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
61 60 notbid ⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
62 58 61 anbi12d ⊢ ( 𝑟 = 𝑣 → ( ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ↔ ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) )
63 breq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
64 63 notbid ⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) )
65 64 anbi2d ⊢ ( 𝑠 = 𝑤 → ( ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ↔ ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) )
66 62 65 rspc2ev ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
67 66 3expa ⊢ ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑣 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
68 45 56 67 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
69 21 43 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
71 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
72 21 42 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
73 8 48 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) )
74 71 72 73 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
75 74 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
76 simpllr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → 𝑃 ≠ 𝑄 )
77 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) )
78 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) )
79 1 2 3 3dimlem3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
80 75 76 77 78 79 syl13anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
81 3simpc ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
82 80 81 syl ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
83 breq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
84 83 notbid ⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
85 84 anbi2d ⊢ ( 𝑠 = 𝑤 → ( ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ↔ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) )
86 36 85 rspc2ev ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
87 86 3expa ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
88 70 82 87 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
89 72 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
90 8 47 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ) )
91 71 72 90 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ) ) )
92 91 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ) ) )
93 simpllr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → 𝑃 ≠ 𝑄 )
94 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) )
95 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) )
96 1 2 3 3dimlem4 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
97 92 93 94 95 96 syl121anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
98 3simpc ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
99 97 98 syl ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) )
100 40 3expa ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑢 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
101 89 99 100 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
102 88 101 pm2.61dan ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑢 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
103 68 102 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
104 41 103 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
105 104 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) ) )
106 105 3expd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐴 → ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ 𝐴 → ( ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) ) ) ) )
107 106 imp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( 𝑤 ∈ 𝐴 → ( ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) ) )
108 107 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) → ( ∃ 𝑤 ∈ 𝐴 ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) )
109 108 rexlimdvva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑄 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) )
110 5 109 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )