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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑞 ) ) )