Metamath Proof Explorer

Theorem cdlema1N

Description: A condition for required for proof of Lemma A in Crawley p. 112. (Contributed by NM, 29-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdlema1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlema1.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlema1.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlema1.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlema1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlema1.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
cdlema1.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
Assertion cdlema1N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑅 ) = ( 𝑋 ∨ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 cdlema1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlema1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlema1.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlema1.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlema1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlema1.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
7 cdlema1.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
8 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝐾 ∈ Lat )
10 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
11 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑅 ∈ 𝐴 )
12 1 5 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑅 ∈ 𝐵 )
14 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑅 ) ∈ 𝐵 )
15 9 10 13 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑅 ) ∈ 𝐵 )
16 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
17 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
18 9 10 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
19 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
20 9 10 16 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
21 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑃 ∈ 𝐴 )
22 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
23 21 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑃 ∈ 𝐵 )
24 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ∈ 𝐴 )
25 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
26 24 25 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ∈ 𝐵 )
27 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
28 9 23 26 27 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
29 simp31r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
30 simp32l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑃 ≤ 𝑋 )
31 simp32r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ≤ 𝑌 )
32 1 2 3 latjlej12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑌 ) ) )
33 9 23 10 26 16 32 syl122anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑌 ) ) )
34 30 31 33 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑌 ) )
35 1 2 9 13 28 18 29 34 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑅 ≤ ( 𝑋 ∨ 𝑌 ) )
36 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑅 ≤ ( 𝑋 ∨ 𝑌 ) ) ↔ ( 𝑋 ∨ 𝑅 ) ≤ ( 𝑋 ∨ 𝑌 ) ) )
37 9 10 13 18 36 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑅 ≤ ( 𝑋 ∨ 𝑌 ) ) ↔ ( 𝑋 ∨ 𝑅 ) ≤ ( 𝑋 ∨ 𝑌 ) ) )
38 20 35 37 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑅 ) ≤ ( 𝑋 ∨ 𝑌 ) )
39 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑅 ) )
40 9 10 13 39 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑅 ) )
41 simp331 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 )
42 simp332 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
43 simp333 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ¬ 𝑄 ≤ 𝑋 )
44 1 2 4 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
45 9 10 16 44 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
46 breq1 ⊢ ( 𝑄 = ( 𝑋 ∧ 𝑌 ) → ( 𝑄 ≤ 𝑋 ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) )
47 45 46 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑄 = ( 𝑋 ∧ 𝑌 ) → 𝑄 ≤ 𝑋 ) )
48 47 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( ¬ 𝑄 ≤ 𝑋 → 𝑄 ≠ ( 𝑋 ∧ 𝑌 ) ) )
49 43 48 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ≠ ( 𝑋 ∧ 𝑌 ) )
50 1 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
51 9 10 16 50 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
52 1 2 3 5 6 7 lneq2at ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑄 ≠ ( 𝑋 ∧ 𝑌 ) ) ∧ ( 𝑄 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) ) → 𝑌 = ( 𝑄 ∨ ( 𝑋 ∧ 𝑌 ) ) )
53 8 16 41 24 42 49 31 51 52 syl332anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑌 = ( 𝑄 ∨ ( 𝑋 ∧ 𝑌 ) ) )
54 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
55 9 23 13 54 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
56 11 24 21 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
57 simp31l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑅 ≠ 𝑃 )
58 8 56 57 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑃 ) )
59 2 3 5 hlatexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑃 ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) )
60 58 29 59 sylc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
61 23 10 13 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) )
62 9 61 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) ) )
63 1 2 3 latjlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) ) → ( 𝑃 ≤ 𝑋 → ( 𝑃 ∨ 𝑅 ) ≤ ( 𝑋 ∨ 𝑅 ) ) )
64 62 30 63 sylc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑃 ∨ 𝑅 ) ≤ ( 𝑋 ∨ 𝑅 ) )
65 1 2 9 26 55 15 60 64 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑅 ) )
66 1 2 3 4 latmlej11 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) )
67 9 10 16 13 66 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) )
68 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
69 9 10 16 68 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
70 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑅 ) ∈ 𝐵 ) ) → ( ( 𝑄 ≤ ( 𝑋 ∨ 𝑅 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) ) ↔ ( 𝑄 ∨ ( 𝑋 ∧ 𝑌 ) ) ≤ ( 𝑋 ∨ 𝑅 ) ) )
71 9 26 69 15 70 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( ( 𝑄 ≤ ( 𝑋 ∨ 𝑅 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) ) ↔ ( 𝑄 ∨ ( 𝑋 ∧ 𝑌 ) ) ≤ ( 𝑋 ∨ 𝑅 ) ) )
72 65 67 71 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑄 ∨ ( 𝑋 ∧ 𝑌 ) ) ≤ ( 𝑋 ∨ 𝑅 ) )
73 53 72 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → 𝑌 ≤ ( 𝑋 ∨ 𝑅 ) )
74 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑅 ) ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑅 ) ∧ 𝑌 ≤ ( 𝑋 ∨ 𝑅 ) ) ↔ ( 𝑋 ∨ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) ) )
75 9 10 16 15 74 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑅 ) ∧ 𝑌 ≤ ( 𝑋 ∨ 𝑅 ) ) ↔ ( 𝑋 ∨ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) ) )
76 40 73 75 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑌 ) ≤ ( 𝑋 ∨ 𝑅 ) )
77 1 2 9 15 18 38 76 latasymd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝑌 ) ∈ 𝑁 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ) → ( 𝑋 ∨ 𝑅 ) = ( 𝑋 ∨ 𝑌 ) )