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

Metamath Proof Explorer

Theorem llncvrlpln2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses llncvrlpln2.l ⊢ ≤ = ( le ‘ 𝐾 )
llncvrlpln2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
llncvrlpln2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
llncvrlpln2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion llncvrlpln2 ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 )

Proof

Step Hyp Ref Expression
1 llncvrlpln2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 llncvrlpln2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 llncvrlpln2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
4 llncvrlpln2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ HL )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝑃 )
8 3 4 lplnnelln ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑌 ∈ 𝑁 )
9 6 7 8 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑌 ∈ 𝑁 )
10 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝑁 )
11 eleq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑁 ) )
12 10 11 syl5ibcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 = 𝑌 → 𝑌 ∈ 𝑁 ) )
13 12 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( ¬ 𝑌 ∈ 𝑁 → 𝑋 ≠ 𝑌 ) )
14 9 13 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≠ 𝑌 )
15 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
16 1 15 pltval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
17 16 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
18 5 14 17 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
19 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝐾 ∈ HL )
20 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ 𝑁 )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 3 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
23 20 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
24 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ 𝑃 )
25 21 4 lplnbase ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
27 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
28 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
29 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
30 21 1 15 28 2 29 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) )
31 19 23 26 27 30 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) )
32 21 1 28 29 4 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) )
33 32 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) )
34 simp3 ⊢ ( ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
35 21 28 29 3 islln2 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) )
36 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) )
37 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 )
38 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
39 38 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
40 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
41 37 39 40 3brtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
42 simp111 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝐾 ∈ HL )
43 simp112 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
44 simp113 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
45 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
46 43 44 45 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) )
47 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
48 simp13r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
49 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) )
50 47 48 49 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) )
51 36 38 39 3brtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
52 21 28 29 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
53 42 43 44 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
54 21 1 28 2 29 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) )
55 42 53 45 54 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) )
56 51 55 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
57 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑝 ≠ 𝑞 )
58 1 28 29 3at ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) )
59 42 46 50 56 57 58 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) )
60 41 59 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) )
61 60 39 40 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = 𝑌 )
62 36 61 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 )
63 62 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) )
64 63 3expd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
65 64 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
66 65 3expib ⊢ ( 𝐾 ∈ HL → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) )
67 66 rexlimdvv ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
68 67 adantld ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
69 35 68 sylbid ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
70 69 imp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
71 34 70 syl7 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
72 71 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
73 72 rexlimdvva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
74 73 adantld ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
75 33 74 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( 𝑌 ∈ 𝑃 → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
76 75 3impia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) )
77 76 rexlimdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) )
78 77 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 )
79 31 78 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 𝑌 )
80 18 79 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 )