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

Metamath Proof Explorer

Theorem cdlemf1

Description: Part of Lemma F in Crawley p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013)

Ref Expression
Hypotheses cdlemf1.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemf1.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemf1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemf1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemf1 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemf1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemf1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemf1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemf1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
6 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
7 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑈 ∈ 𝐴 )
8 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑈 ≤ 𝑊 )
9 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ¬ 𝑃 ≤ 𝑊 )
10 nbrne2 ⊢ ( ( 𝑈 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑈 ≠ 𝑃 )
11 10 necomd ⊢ ( ( 𝑈 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑃 ≠ 𝑈 )
12 8 9 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≠ 𝑈 )
13 1 2 3 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑈 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) )
14 5 6 7 12 13 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) )
15 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑞 ≠ 𝑃 )
16 15 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑃 ≠ 𝑞 )
17 simp13r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ¬ 𝑃 ≤ 𝑊 )
18 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑈 ≤ 𝑊 )
19 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝐾 ∈ HL )
20 19 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝐾 ∈ Lat )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 3 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
23 22 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
24 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑈 ∈ 𝐴 )
25 21 3 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
27 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑊 ∈ 𝐻 )
28 21 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29 27 28 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
30 21 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) )
31 20 23 26 29 30 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( ( 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) )
32 31 biimpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( ( 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) → ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) )
33 18 32 mpan2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑞 ≤ 𝑊 → ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) )
34 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) )
35 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
36 19 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝐾 ∈ CvLat )
37 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑞 ∈ 𝐴 )
38 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑃 ∈ 𝐴 )
39 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑞 ≠ 𝑈 )
40 1 2 3 cvlatexch2 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ 𝑞 ≠ 𝑈 ) → ( 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑃 ≤ ( 𝑞 ∨ 𝑈 ) ) )
41 36 37 38 24 39 40 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑃 ≤ ( 𝑞 ∨ 𝑈 ) ) )
42 34 41 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑃 ≤ ( 𝑞 ∨ 𝑈 ) )
43 21 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
44 38 43 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
45 21 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑞 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑞 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
46 19 37 24 45 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑞 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
47 21 1 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑞 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑞 ∨ 𝑈 ) ∧ ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
48 20 44 46 29 47 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( ( 𝑃 ≤ ( 𝑞 ∨ 𝑈 ) ∧ ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
49 42 48 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( ( 𝑞 ∨ 𝑈 ) ≤ 𝑊 → 𝑃 ≤ 𝑊 ) )
50 33 49 syld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑞 ≤ 𝑊 → 𝑃 ≤ 𝑊 ) )
51 17 50 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ¬ 𝑞 ≤ 𝑊 )
52 1 2 3 cvlatexch1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )
53 36 37 24 38 15 52 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )
54 34 53 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) )
55 16 51 54 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) ) → ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )
56 55 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) → ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) ) ) )
57 56 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≠ 𝑈 ∧ 𝑞 ≤ ( 𝑃 ∨ 𝑈 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) ) )
58 14 57 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )