Metamath Proof Explorer

Theorem lhprelat3N

Description: The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 . (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhprelat3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhprelat3.l ⊢ ≤ = ( le ‘ 𝐾 )
lhprelat3.s ⊢ < = ( lt ‘ 𝐾 )
lhprelat3.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhprelat3.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lhprelat3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhprelat3N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑤 ∈ 𝐻 ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ∧ ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lhprelat3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhprelat3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhprelat3.s ⊢ < = ( lt ‘ 𝐾 )
4 lhprelat3.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 lhprelat3.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6 lhprelat3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
8 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ HL )
9 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 1 9 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
11 10 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ 𝐵 )
12 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
13 1 12 9 6 lhpoc2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐻 ) )
14 8 11 13 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐻 ) )
15 7 14 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐻 )
16 15 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐻 )
17 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
18 8 17 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
19 8 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ Lat )
20 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ 𝐵 )
21 1 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐵 )
22 18 11 21 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐵 )
23 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐵 ) → ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∈ 𝐵 )
24 19 20 22 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∈ 𝐵 )
25 1 12 5 cvrcon3b ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) )
26 18 24 20 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) )
27 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
28 8 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OL )
29 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
30 1 29 4 12 oldmm3N ⊢ ( ( 𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) )
31 28 20 11 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) )
32 31 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ) )
33 26 32 bitr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ↔ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ) )
34 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ∈ 𝐵 )
35 1 2 12 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∈ 𝐵 ) → ( 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
36 18 34 24 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
37 31 breq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
38 36 37 bitr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
39 33 38 anbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ↔ ( ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ∧ 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ) )
40 39 biimpa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ∧ 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
41 40 ancomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∧ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ) )
42 oveq2 ⊢ ( 𝑤 = ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) → ( 𝑌 ∧ 𝑤 ) = ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) )
43 42 breq2d ⊢ ( 𝑤 = ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) → ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ↔ 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
44 42 breq1d ⊢ ( 𝑤 = ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) → ( ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ↔ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ) )
45 43 44 anbi12d ⊢ ( 𝑤 = ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) → ( ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ∧ ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ) ↔ ( 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∧ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ) ) )
46 45 rspcev ⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ∈ 𝐻 ∧ ( 𝑋 ≤ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ∧ ( 𝑌 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) 𝐶 𝑌 ) ) → ∃ 𝑤 ∈ 𝐻 ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ∧ ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ) )
47 16 41 46 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ∃ 𝑤 ∈ 𝐻 ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ∧ ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ) )
48 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐾 ∈ HL )
49 48 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝐾 ∈ OP )
50 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ 𝐵 )
51 1 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
52 49 50 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
53 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ 𝐵 )
54 1 12 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
55 49 53 54 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
56 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
57 1 3 12 opltcon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) < ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
58 49 53 50 57 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 < 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) < ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
59 56 58 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) < ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) )
60 1 2 3 29 5 9 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) < ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
61 48 52 55 59 60 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
62 47 61 r19.29a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑤 ∈ 𝐻 ( 𝑋 ≤ ( 𝑌 ∧ 𝑤 ) ∧ ( 𝑌 ∧ 𝑤 ) 𝐶 𝑌 ) )