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

Metamath Proof Explorer

Theorem cdlemb

Description: Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in Crawley p. 112. (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 ‘ 𝐾 )
Assertion cdlemb ( ( ( 𝐾 ∈ 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 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
8 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
9 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐴 )
10 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
11 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑄 )
12 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑋 𝐶 1 )
13 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑋 )
14 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
15 1 2 3 14 4 5 6 1cvrat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∈ 𝐴 )
16 7 8 9 10 11 12 13 15 syl133anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∈ 𝐴 )
17 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
18 1 6 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
19 8 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
20 1 6 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
21 9 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐵 )
22 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
23 17 19 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
24 1 2 14 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ≤ 𝑋 )
25 17 23 10 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ≤ 𝑋 )
26 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
27 1 2 26 4 5 6 1cvratlt ⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ( lt ‘ 𝐾 ) 𝑋 )
28 7 16 10 12 25 27 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ( lt ‘ 𝐾 ) 𝑋 )
29 1 26 6 2atlt ⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ( lt ‘ 𝐾 ) 𝑋 ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) )
30 7 16 10 28 29 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) )
31 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝐾 ∈ HL )
32 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑃 ∈ 𝐴 )
33 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑢 ∈ 𝐴 )
34 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ¬ 𝑃 ≤ 𝑋 )
35 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑢 ( lt ‘ 𝐾 ) 𝑋 )
36 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
37 2 26 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑢 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑢 ( lt ‘ 𝐾 ) 𝑋 → 𝑢 ≤ 𝑋 ) )
38 31 33 36 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑢 ( lt ‘ 𝐾 ) 𝑋 → 𝑢 ≤ 𝑋 ) )
39 35 38 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑢 ≤ 𝑋 )
40 breq1 ⊢ ( 𝑃 = 𝑢 → ( 𝑃 ≤ 𝑋 ↔ 𝑢 ≤ 𝑋 ) )
41 39 40 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑃 = 𝑢 → 𝑃 ≤ 𝑋 ) )
42 41 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ( ¬ 𝑃 ≤ 𝑋 → 𝑃 ≠ 𝑢 ) )
43 34 42 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → 𝑃 ≠ 𝑢 )
44 2 3 6 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑢 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) )
45 31 32 33 43 44 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) )
46 eqid ⊢ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) = ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 )
47 1 2 3 4 5 6 26 14 46 cdlemblem ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
48 47 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) )
49 48 exp4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) → ( 𝑟 ∈ 𝐴 → ( ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) ) )
50 49 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑟 ∈ 𝐴 → ( ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) → ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) )
51 50 reximdvai ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
52 45 51 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 ≠ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ∧ 𝑢 ( lt ‘ 𝐾 ) 𝑋 ) ) ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
53 30 52 rexlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )