Theorem cdlemg31c

Description: Show that when N is an atom, it is not under W . TODO: Is there a shorter direct proof? TODO: should we eliminate ( FP ) =/= P here? (Contributed by NM, 29-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemg12.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemg12.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemg12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemg12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemg12.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemg12b.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdlemg31.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑣 ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
Assertion	cdlemg31c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑁 ≤ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg12.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg12.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemg12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemg12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemg12.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemg12b.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemg31.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑣 ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
9		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
10		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑊 ∈ 𝐻 )
11	9 10	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
13		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) )
14	13	necomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑣 )
15		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
16		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝐹 ∈ 𝑇 )
17		simp32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 )
18	1 4 5 6 7	trlat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
19	11 15 16 17 18	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
20	1 5 6 7	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
21	11 16 20	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
22		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) )
23	1 2 4 5	lhp2atnle	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑣 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
24	11 12 14 19 21 22 23	syl321anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
25		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
26		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
27		simp2ll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑣 ∈ 𝐴 )
28	1 2 3 4 5 6 7 8	cdlemg31a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝐹 ∈ 𝑇 ) ) → 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) )
29	9 10 25 26 27 16 28	syl222anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) )
30	29	adantr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) )
31		simp111	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32		simp112	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
33		simp3	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → 𝑁 ≠ 𝑣 )
34	33	necomd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → 𝑣 ≠ 𝑁 )
35		simp12l	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) )
36		simp133	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → 𝑁 ∈ 𝐴 )
37		simp2	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → 𝑁 ≤ 𝑊 )
38	1 2 4 5	lhp2atnle	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑣 ≠ 𝑁 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ≤ 𝑊 ) ) → ¬ 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) )
39	31 32 34 35 36 37 38	syl312anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ∧ 𝑁 ≠ 𝑣 ) → ¬ 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) )
40	39	3expia	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → ( 𝑁 ≠ 𝑣 → ¬ 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) ) )
41	40	necon4ad	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → ( 𝑁 ≤ ( 𝑃 ∨ 𝑣 ) → 𝑁 = 𝑣 ) )
42	30 41	mpd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → 𝑁 = 𝑣 )
43	1 2 3 4 5 6 7 8	cdlemg31b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝐹 ∈ 𝑇 ) ) → 𝑁 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
44	9 10 25 26 27 16 43	syl222anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → 𝑁 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
45	44	adantr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → 𝑁 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
46	42 45	eqbrtrrd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) ∧ 𝑁 ≤ 𝑊 ) → 𝑣 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
47	24 46	mtand	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑁 ≤ 𝑊 )