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

Metamath Proof Explorer

Theorem lplncvrlvol2

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

Ref Expression
Hypotheses lplncvrlvol2.l ⊢ ≤ = ( le ‘ 𝐾 )
lplncvrlvol2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lplncvrlvol2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
lplncvrlvol2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lplncvrlvol2 ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 )

Proof

Step Hyp Ref Expression
1 lplncvrlvol2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplncvrlvol2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 lplncvrlvol2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 lplncvrlvol2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ HL )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝑉 )
8 3 4 lvolnelpln ⊢ ( ( 𝐾 ∈ 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 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
23 20 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
24 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ 𝑉 )
25 21 4 lvolbase ⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ ( 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 islvol2 ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) ) )
33 32 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) ) )
34 simpr ⊢ ( ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) )
35 21 1 28 29 3 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
36 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) )
37 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 )
38 simp133 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
39 38 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) )
40 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) )
41 37 39 40 3brtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) )
42 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) )
43 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
44 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
45 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
46 43 44 45 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) )
47 simp21r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) )
48 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑣 ∈ ( Atoms ‘ 𝐾 ) )
49 simp22r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑤 ∈ ( Atoms ‘ 𝐾 ) )
50 47 48 49 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) )
51 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑝 ≠ 𝑞 )
52 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
53 36 38 39 3brtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) )
54 simp111 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝐾 ∈ HL )
55 54 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝐾 ∈ Lat )
56 21 28 29 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
57 42 56 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
58 21 29 atbase ⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
59 43 58 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
60 21 28 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
61 55 57 59 60 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
62 21 1 28 2 29 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) )
63 54 61 44 62 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) )
64 53 63 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) )
65 1 28 29 4at2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ↔ ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) )
66 42 46 50 51 52 64 65 syl33anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ↔ ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) )
67 41 66 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) )
68 67 39 40 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) = 𝑌 )
69 36 68 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 𝐶 𝑌 )
70 69 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 ) ) )
71 70 exp4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
72 71 3expd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) )
73 72 rexlimdv3a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
74 73 3expib ⊢ ( 𝐾 ∈ HL → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) )
75 74 rexlimdvv ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
76 75 adantld ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
77 35 76 sylbid ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) )
78 77 imp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
79 34 78 syl7 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) )
80 79 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
81 80 rexlimdvva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
82 81 adantld ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
83 33 82 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( 𝑌 ∈ 𝑉 → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) )
84 83 3impia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) )
85 84 rexlimdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) )
86 85 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 )
87 31 86 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 𝑌 )
88 18 87 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 )