Metamath Proof Explorer

Theorem lhpexle3lem

Description: There exists atom under a co-atom different from any three other atoms. TODO: study if adant*, simp* usage can be improved. (Contributed by NM, 9-Jul-2013)

Ref Expression
Hypotheses lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle3lem ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 1 2 3 lhpexle2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) )
6 4 5 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) )
7 simp31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → 𝑝 ≤ 𝑊 )
8 simp32 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → 𝑝 ≠ 𝑋 )
9 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → 𝑋 = 𝑌 )
10 8 9 neeqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → 𝑝 ≠ 𝑌 )
11 simp33 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → 𝑝 ≠ 𝑍 )
12 8 10 11 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) )
13 7 12 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) ) → ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
14 13 3exp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( 𝑝 ∈ 𝐴 → ( ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) → ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) ) ) )
15 14 reximdvai ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) ) )
16 6 15 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
17 simprrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑝 ≤ 𝑊 )
18 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝐾 ∈ HL )
19 18 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
20 19 hllatd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 2 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
23 22 ad2antrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
24 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ∈ 𝐴 )
25 24 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑋 ∈ 𝐴 )
26 21 2 atbase ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
27 25 26 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
28 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑌 ∈ 𝐴 )
29 28 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑌 ∈ 𝐴 )
30 21 2 atbase ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
31 29 30 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
32 simprrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
33 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
34 21 1 33 latnlej1l ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑝 ≠ 𝑋 )
35 20 23 27 31 32 34 syl131anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑝 ≠ 𝑋 )
36 21 1 33 latnlej1r ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑝 ≠ 𝑌 )
37 20 23 27 31 32 36 syl131anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑝 ≠ 𝑌 )
38 simpl3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
39 nbrne2 ⊢ ( ( 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑍 ≠ 𝑝 )
40 39 necomd ⊢ ( ( 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑝 ≠ 𝑍 )
41 38 32 40 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → 𝑝 ≠ 𝑍 )
42 35 37 41 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) )
43 17 42 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
44 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ≤ 𝑊 )
46 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑌 ≤ 𝑊 )
47 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
48 1 47 33 2 3 lhp2lt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑊 )
49 44 24 45 28 46 48 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑊 )
50 21 33 2 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
51 18 24 28 50 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
52 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑊 ∈ 𝐻 )
53 21 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
54 52 53 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
55 21 1 47 2 hlrelat1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑊 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) )
56 18 51 54 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑊 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) ) )
57 49 56 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ 𝑝 ≤ 𝑊 ) )
58 43 57 reximddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
59 58 3expa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
60 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝐾 ∈ HL )
61 60 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ HL )
62 61 hllatd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ Lat )
63 22 ad2antrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
64 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ∈ 𝐴 )
65 64 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ∈ 𝐴 )
66 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑌 ∈ 𝐴 )
67 66 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ∈ 𝐴 )
68 61 65 67 50 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
69 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑊 ∈ 𝐻 )
70 69 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊 ∈ 𝐻 )
71 70 53 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
72 simprr3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
73 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ≤ 𝑊 )
74 73 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ≤ 𝑊 )
75 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑌 ≤ 𝑊 )
76 75 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ≤ 𝑊 )
77 65 26 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
78 67 30 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
79 21 1 33 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 ) )
80 62 77 78 71 79 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 ) )
81 74 76 80 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 )
82 21 1 62 63 68 71 72 81 lattrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≤ 𝑊 )
83 simprr1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≠ 𝑋 )
84 simprr2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≠ 𝑌 )
85 simpl3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
86 nbrne2 ⊢ ( ( 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑝 ≠ 𝑍 )
87 72 85 86 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≠ 𝑍 )
88 83 84 87 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) )
89 82 88 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
90 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ≠ 𝑌 )
91 1 33 2 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
92 60 64 66 90 91 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
93 89 92 reximddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
94 93 3expa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) ∧ ¬ 𝑍 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
95 59 94 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )
96 16 95 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ) ) )