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

Metamath Proof Explorer

Theorem lplnnle2at

Description: A lattice line (or atom) cannot majorize a lattice plane. (Contributed by NM, 8-Jul-2012)

Ref Expression
Hypotheses lplnnle2at.l ⊢ ≤ = ( le ‘ 𝐾 )
lplnnle2at.j ⊢ ∨ = ( join ‘ 𝐾 )
lplnnle2at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lplnnle2at.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnnle2at ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lplnnle2at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplnnle2at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lplnnle2at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lplnnle2at.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑋 ∈ 𝑃 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
8 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
9 6 7 8 4 islpln ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
10 9 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
11 5 10 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
12 11 simprd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 )
13 oveq1 ⊢ ( 𝑄 = 𝑅 → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑅 ) )
14 13 breq2d ⊢ ( 𝑄 = 𝑅 → ( 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ↔ 𝑋 ≤ ( 𝑅 ∨ 𝑅 ) ) )
15 14 notbid ⊢ ( 𝑄 = 𝑅 → ( ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ¬ 𝑋 ≤ ( 𝑅 ∨ 𝑅 ) ) )
16 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝐾 ∈ HL )
17 simpl3l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑦 ∈ ( LLines ‘ 𝐾 ) )
18 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑄 ∈ 𝐴 )
19 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑅 ∈ 𝐴 )
20 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑄 ≠ 𝑅 )
21 2 3 8 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( LLines ‘ 𝐾 ) )
22 16 18 19 20 21 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( LLines ‘ 𝐾 ) )
23 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
24 23 8 llnnlt ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( LLines ‘ 𝐾 ) ) → ¬ 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
25 16 17 22 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ¬ 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
26 6 8 llnbase ⊢ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
27 17 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
28 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑋 ∈ 𝑃 )
29 6 4 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
31 simpl3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 )
32 6 23 7 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑦 ( lt ‘ 𝐾 ) 𝑋 )
33 16 27 30 31 32 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) 𝑋 )
34 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
35 16 34 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝐾 ∈ Poset )
36 6 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
37 16 18 19 36 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
38 6 1 23 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
39 35 27 30 37 38 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
40 33 39 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
41 25 40 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑄 ≠ 𝑅 ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) )
42 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ HL )
43 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ∈ ( LLines ‘ 𝐾 ) )
44 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑅 ∈ 𝐴 )
45 1 3 8 llnnleat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑅 ∈ 𝐴 ) → ¬ 𝑦 ≤ 𝑅 )
46 42 43 44 45 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑦 ≤ 𝑅 )
47 43 26 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
48 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ 𝑃 )
49 48 29 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
50 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 )
51 42 47 49 50 32 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ( lt ‘ 𝐾 ) 𝑋 )
52 34 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ Poset )
53 6 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
54 44 53 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
55 6 1 23 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) 𝑅 ) )
56 52 47 49 54 55 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) 𝑅 ) )
57 51 56 mpand ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ 𝑅 → 𝑦 ( lt ‘ 𝐾 ) 𝑅 ) )
58 1 23 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑅 ∈ 𝐴 ) → ( 𝑦 ( lt ‘ 𝐾 ) 𝑅 → 𝑦 ≤ 𝑅 ) )
59 42 43 44 58 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑦 ( lt ‘ 𝐾 ) 𝑅 → 𝑦 ≤ 𝑅 ) )
60 57 59 syld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ 𝑅 → 𝑦 ≤ 𝑅 ) )
61 46 60 mtod ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ 𝑅 )
62 2 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
63 42 44 62 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
64 63 breq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( 𝑅 ∨ 𝑅 ) ↔ 𝑋 ≤ 𝑅 ) )
65 61 64 mtbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( 𝑅 ∨ 𝑅 ) )
66 15 41 65 pm2.61ne ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) )
67 66 3exp ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
68 67 exp4a ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑦 ∈ ( LLines ‘ 𝐾 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) )
69 68 imp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑦 ∈ ( LLines ‘ 𝐾 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
70 69 rexlimdv ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) )
71 12 70 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) )