Metamath Proof Explorer

Theorem cdlemblem

Description: Lemma for cdlemb . (Contributed by NM, 8-May-2012)

Ref Expression
Hypotheses cdlemb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemb.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemb.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemb.u ⊢ 1 = ( 1. ‘ 𝐾 )
cdlemb.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
cdlemb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemblem.s ⊢ < = ( lt ‘ 𝐾 )
cdlemblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemblem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 )
Assertion cdlemblem ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemb.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemb.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemb.u ⊢ 1 = ( 1. ‘ 𝐾 )
5 cdlemb.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6 cdlemb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 cdlemblem.s ⊢ < = ( lt ‘ 𝐾 )
8 cdlemblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
9 cdlemblem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 )
10 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ¬ 𝑃 ≤ 𝑋 )
11 simp111 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝐾 ∈ HL )
12 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 ∈ 𝐴 )
13 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑋 ∈ 𝐵 )
14 11 12 13 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑢 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) )
15 simp2rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 < 𝑋 )
16 2 7 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑢 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑢 < 𝑋 → 𝑢 ≤ 𝑋 ) )
17 14 15 16 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 ≤ 𝑋 )
18 11 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝐾 ∈ Lat )
19 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑟 ∈ 𝐴 )
20 1 6 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵 )
21 19 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑟 ∈ 𝐵 )
22 1 6 atbase ⊢ ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵 )
23 12 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 ∈ 𝐵 )
24 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑟 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑢 ≤ 𝑋 ) ↔ ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) )
25 18 21 23 13 24 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑢 ≤ 𝑋 ) ↔ ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) )
26 25 biimpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑢 ≤ 𝑋 ) → ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) )
27 17 26 mpan2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ 𝑋 → ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) )
28 simp112 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑃 ∈ 𝐴 )
29 19 28 12 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) )
30 simp3r2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑟 ≠ 𝑢 )
31 11 29 30 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑢 ) )
32 simp3r3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) )
33 2 3 6 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑢 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) → 𝑃 ≤ ( 𝑟 ∨ 𝑢 ) ) )
34 31 32 33 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑃 ≤ ( 𝑟 ∨ 𝑢 ) )
35 1 6 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
36 28 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑃 ∈ 𝐵 )
37 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑟 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑟 ∨ 𝑢 ) ∈ 𝐵 )
38 18 21 23 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ∨ 𝑢 ) ∈ 𝐵 )
39 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑟 ∨ 𝑢 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ ( 𝑟 ∨ 𝑢 ) ∧ ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
40 18 36 38 13 39 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑃 ≤ ( 𝑟 ∨ 𝑢 ) ∧ ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
41 34 40 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑟 ∨ 𝑢 ) ≤ 𝑋 → 𝑃 ≤ 𝑋 ) )
42 27 41 syld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ 𝑋 → 𝑃 ≤ 𝑋 ) )
43 10 42 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ¬ 𝑟 ≤ 𝑋 )
44 simp2rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 ≠ 𝑉 )
45 simp113 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑄 ∈ 𝐴 )
46 simp3r1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑟 ≠ 𝑃 )
47 2 3 6 hlatexchb1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑃 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑟 ) = ( 𝑃 ∨ 𝑄 ) ) )
48 11 19 45 28 46 47 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑟 ) = ( 𝑃 ∨ 𝑄 ) ) )
49 19 12 28 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
50 11 49 46 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑃 ) )
51 2 3 6 hlatexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑃 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑃 ∨ 𝑟 ) ) )
52 50 32 51 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑢 ≤ ( 𝑃 ∨ 𝑟 ) )
53 breq2 ⊢ ( ( 𝑃 ∨ 𝑟 ) = ( 𝑃 ∨ 𝑄 ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑟 ) ↔ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
54 52 53 syl5ibcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑃 ∨ 𝑟 ) = ( 𝑃 ∨ 𝑄 ) → 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
55 48 54 sylbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
56 55 17 jctird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑋 ) ) )
57 1 6 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
58 45 57 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑄 ∈ 𝐵 )
59 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
60 18 36 58 59 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
61 1 2 8 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑢 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑋 ) ↔ 𝑢 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
62 18 23 60 13 61 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑋 ) ↔ 𝑢 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
63 9 breq2i ⊢ ( 𝑢 ≤ 𝑉 ↔ 𝑢 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) )
64 62 63 bitr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑋 ) ↔ 𝑢 ≤ 𝑉 ) )
65 56 64 sylibd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑢 ≤ 𝑉 ) )
66 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
67 11 66 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝐾 ∈ AtLat )
68 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑃 ≠ 𝑄 )
69 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑋 𝐶 1 )
70 1 2 3 8 4 5 6 1cvrat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )
71 11 28 45 13 68 69 10 70 syl133anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )
72 9 71 eqeltrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → 𝑉 ∈ 𝐴 )
73 2 6 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑢 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑢 ≤ 𝑉 ↔ 𝑢 = 𝑉 ) )
74 67 12 72 73 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑢 ≤ 𝑉 ↔ 𝑢 = 𝑉 ) )
75 65 74 sylibd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑢 = 𝑉 ) )
76 75 necon3ad ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( 𝑢 ≠ 𝑉 → ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
77 44 76 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) )
78 43 77 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )