Metamath Proof Explorer

Theorem cdlemg18c

Description: Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-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 ‘ 𝐾 ) ‘ 𝑊 )
cdlemg18b.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion cdlemg18c ( ( ( 𝐾 ∈ 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 cdlemg18b.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
9 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
10 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
11 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
12 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
13 simp22l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
14 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
15 1 2 3 4 5 8 cdleme0a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
16 9 11 12 13 14 15 syl212anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑈 ∈ 𝐴 )
17 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐹 ∈ 𝑇 )
19 1 4 5 6 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 )
20 17 18 13 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 )
21 1 4 5 6 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
22 17 18 10 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
23 1 2 3 4 5 6 7 8 cdlemg18b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑃 ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) )
24 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 )
25 24 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ≠ ( 𝐹 ‘ 𝑃 ) )
26 23 25 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑃 ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑄 ≠ ( 𝐹 ‘ 𝑃 ) ) )
27 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) )
28 1 2 3 4 5 6 7 cdlemg18a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑄 ) ) ≠ ( 𝑄 ∨ ( 𝐹 ‘ 𝑃 ) ) )
29 17 10 13 18 14 27 28 syl132anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑄 ) ) ≠ ( 𝑄 ∨ ( 𝐹 ‘ 𝑃 ) ) )
30 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
31 9 10 13 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
32 1 2 3 4 5 8 cdleme0cp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) )
33 9 11 12 13 32 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) )
34 31 33 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) )
35 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) )
36 9 20 22 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) )
37 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
38 5 6 1 2 4 3 8 cdlemg2kq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ 𝑈 ) )
39 17 12 37 18 38 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ 𝑈 ) )
40 2 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) )
41 9 22 20 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) )
42 2 4 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑄 ) ∨ 𝑈 ) = ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) )
43 9 20 16 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑄 ) ∨ 𝑈 ) = ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) )
44 39 41 43 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) = ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) )
45 36 44 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) )
46 34 45 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) ∧ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) ) )
47 1 2 3 4 ps-2c ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑄 ) ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑄 ≠ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ ( 𝐹 ‘ 𝑄 ) ) ≠ ( 𝑄 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ 𝑈 ) ∧ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑈 ∨ ( 𝐹 ‘ 𝑄 ) ) ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ ( 𝑄 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∈ 𝐴 )
48 9 10 16 20 13 22 26 29 46 47 syl333anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑄 ∧ ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ 𝑃 ) ) ≠ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ ( 𝑄 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∈ 𝐴 )