| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1cvratex.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
1cvratex.s |
⊢ < = ( lt ‘ 𝐾 ) |
| 3 |
|
1cvratex.u |
⊢ 1 = ( 1. ‘ 𝐾 ) |
| 4 |
|
1cvratex.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
| 5 |
|
1cvratex.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
| 6 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → 𝐾 ∈ HL ) |
| 7 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
| 8 |
1 3 7 4 5
|
1cvrco |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐴 ) ) |
| 9 |
8
|
biimp3a |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐴 ) |
| 10 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 11 |
10 4 5
|
2dim |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 12 |
6 9 11
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 13 |
|
simp11 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ HL ) |
| 14 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
| 15 |
13 14
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ OP ) |
| 16 |
13
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ Lat ) |
| 17 |
|
simp12 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑋 ∈ 𝐵 ) |
| 18 |
1 7
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 19 |
15 17 18
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 20 |
|
simp2l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ∈ 𝐴 ) |
| 21 |
1 5
|
atbase |
⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵 ) |
| 22 |
20 21
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ∈ 𝐵 ) |
| 23 |
1 10
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) |
| 24 |
16 19 22 23
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) |
| 25 |
1 7
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ) |
| 26 |
15 24 25
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ) |
| 27 |
|
simp2r |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑟 ∈ 𝐴 ) |
| 28 |
1 5
|
atbase |
⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵 ) |
| 29 |
27 28
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑟 ∈ 𝐵 ) |
| 30 |
1 10
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) |
| 31 |
16 24 29 30
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) |
| 32 |
1 7
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∈ 𝐵 ) |
| 33 |
15 31 32
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∈ 𝐵 ) |
| 34 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 35 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
| 36 |
1 34 35
|
op0le |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∈ 𝐵 ) → ( 0. ‘ 𝐾 ) ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 37 |
15 33 36
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 0. ‘ 𝐾 ) ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 38 |
|
simp3r |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 39 |
1 2 4
|
cvrlt |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) < ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 40 |
13 24 31 38 39
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) < ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 41 |
1 2 7
|
opltcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) < ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 42 |
15 24 31 41
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) < ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 43 |
40 42
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) |
| 44 |
|
hlpos |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset ) |
| 45 |
13 44
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ Poset ) |
| 46 |
1 35
|
op0cl |
⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ 𝐵 ) |
| 47 |
15 46
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 0. ‘ 𝐾 ) ∈ 𝐵 ) |
| 48 |
1 34 2
|
plelttr |
⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 0. ‘ 𝐾 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ) ) → ( ( ( 0. ‘ 𝐾 ) ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) → ( 0. ‘ 𝐾 ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 49 |
45 47 33 26 48
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( 0. ‘ 𝐾 ) ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) → ( 0. ‘ 𝐾 ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 50 |
37 43 49
|
mp2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 0. ‘ 𝐾 ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) |
| 51 |
2
|
pltne |
⊢ ( ( 𝐾 ∈ HL ∧ ( 0. ‘ 𝐾 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) → ( 0. ‘ 𝐾 ) ≠ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 52 |
13 47 26 51
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 0. ‘ 𝐾 ) < ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) → ( 0. ‘ 𝐾 ) ≠ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) ) |
| 53 |
50 52
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 0. ‘ 𝐾 ) ≠ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) |
| 54 |
53
|
necomd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ≠ ( 0. ‘ 𝐾 ) ) |
| 55 |
1 34 35 5
|
atle |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ≠ ( 0. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) |
| 56 |
13 26 54 55
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ) |
| 57 |
|
simp3l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) |
| 58 |
1 2 4
|
cvrlt |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) < ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) |
| 59 |
13 19 24 57 58
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) < ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) |
| 60 |
1 2 7
|
opltcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) < ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) |
| 61 |
15 19 24 60
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) < ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) |
| 62 |
59 61
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 63 |
1 7
|
opococ |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) |
| 64 |
15 17 63
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) |
| 65 |
62 64
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < 𝑋 ) |
| 66 |
65
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < 𝑋 ) |
| 67 |
|
simpl11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL ) |
| 68 |
67 44
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ Poset ) |
| 69 |
1 5
|
atbase |
⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 ) |
| 70 |
69
|
adantl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 ) |
| 71 |
26
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ) |
| 72 |
|
simpl12 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 ) |
| 73 |
1 34 2
|
plelttr |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < 𝑋 ) → 𝑝 < 𝑋 ) ) |
| 74 |
68 70 71 72 73
|
syl13anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) < 𝑋 ) → 𝑝 < 𝑋 ) ) |
| 75 |
66 74
|
mpan2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑝 < 𝑋 ) ) |
| 76 |
75
|
reximdva |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 ) ) |
| 77 |
56 76
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 ) |
| 78 |
77
|
3exp |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ( ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 ) ) ) |
| 79 |
78
|
rexlimdvv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 ) ) |
| 80 |
12 79
|
mpd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 ) |