Metamath Proof Explorer

Theorem lhpexle2lem

Description: Lemma for lhpexle2 . (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle2lem ( ( ( 𝐾 ∈ 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 lhpexle1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
6 4 5 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
7 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) ) → 𝑝 ≤ 𝑊 )
8 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) ) → 𝑝 ≠ 𝑋 )
9 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) ) → 𝑋 = 𝑌 )
10 8 9 neeqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) ) → 𝑝 ≠ 𝑌 )
11 7 8 10 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )
12 11 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
13 12 reximdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
14 6 13 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )
15 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝐾 ∈ HL )
16 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐴 )
17 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐴 )
18 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
19 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
20 1 19 2 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
21 15 16 17 18 20 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
22 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
23 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ HL )
24 23 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ Lat )
25 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ∈ 𝐴 )
26 22 2 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
27 25 26 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
28 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ∈ 𝐴 )
29 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ∈ 𝐴 )
30 22 19 2 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
31 23 28 29 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
32 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊 ∈ 𝐻 )
33 22 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
34 32 33 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
35 simprr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
36 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ≤ 𝑊 )
37 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ≤ 𝑊 )
38 22 2 atbase ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
39 28 38 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
40 22 2 atbase ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
41 29 40 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
42 22 1 19 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 ) )
43 24 39 41 34 42 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 ) )
44 36 37 43 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ≤ 𝑊 )
45 22 1 24 27 31 34 35 44 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≤ 𝑊 )
46 simprr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≠ 𝑋 )
47 simprr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ≠ 𝑌 )
48 45 46 47 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≠ 𝑌 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )
49 48 exp44 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝑝 ∈ 𝐴 → ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) ) ) )
50 49 imp31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
51 50 reximdva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) ) )
52 21 51 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑋 ≠ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )
53 14 52 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ) )