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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑁 ≤ 𝑊 )