Metamath Proof Explorer

Theorem 3dim1

Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom P . (Contributed by NM, 25-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3dim0 ⊢ ( 𝐾 ∈ HL → ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
5 4 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
6 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
7 1 2 3 3dimlem1 ⊢ ( ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
8 7 3ad2antl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
9 1 2 3 3dim1lem5 ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
10 6 8 9 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑡 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
11 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑡 ∈ 𝐴 )
12 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑣 ∈ 𝐴 )
13 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑤 ∈ 𝐴 )
14 11 12 13 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
15 14 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
16 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) )
17 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑢 ∈ 𝐴 )
18 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) )
19 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) )
20 17 18 19 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
21 20 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
22 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → 𝑃 ≠ 𝑡 )
23 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) )
24 1 2 3 3dimlem2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑣 ) ) )
25 16 21 22 23 24 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑣 ) ) )
26 1 2 3 3dim1lem5 ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
27 15 25 26 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
28 11 17 13 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
29 28 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
30 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) )
31 17 12 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
32 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → 𝑡 ≠ 𝑢 )
33 32 19 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) )
34 30 31 33 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
35 34 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
36 simplrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → 𝑃 ≠ 𝑡 )
37 simplrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) )
38 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) )
39 1 2 3 3dimlem3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) )
40 35 36 37 38 39 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) )
41 1 2 3 3dim1lem5 ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
42 29 40 41 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
43 11 17 12 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
44 43 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
45 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) )
46 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → 𝑢 ∈ 𝐴 )
47 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → 𝑣 ∈ 𝐴 )
48 46 47 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) )
49 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → 𝑡 ≠ 𝑢 )
50 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) )
51 49 50 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) )
52 45 48 51 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) ) )
53 52 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) ) )
54 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) )
55 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) )
56 1 2 3 3dimlem4 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) )
57 53 54 55 56 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) )
58 1 2 3 3dim1lem5 ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑃 ∨ 𝑡 ) ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑡 ) ∨ 𝑢 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
59 44 57 58 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
60 42 59 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ ( 𝑃 ≠ 𝑡 ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
61 60 anassrs ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) ∧ ¬ 𝑃 ≤ ( 𝑡 ∨ 𝑢 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
62 27 61 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑡 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
63 10 62 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
64 63 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
65 64 3expd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐴 → ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ 𝐴 → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) ) ) )
66 65 3exp ⊢ ( 𝐾 ∈ HL → ( 𝑃 ∈ 𝐴 → ( 𝑡 ∈ 𝐴 → ( 𝑢 ∈ 𝐴 → ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ 𝐴 → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) ) ) ) ) )
67 66 imp43 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ 𝐴 → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) ) )
68 67 impd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
69 68 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
70 69 rexlimdvva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐴 ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ∨ 𝑢 ) ∨ 𝑣 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
71 5 70 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )