| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cvrcmp.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
cvrcmp.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 3 |
|
cvrcmp.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
| 4 |
|
opposet |
⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset ) |
| 5 |
4
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ Poset ) |
| 6 |
|
simp1 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ OP ) |
| 7 |
|
simp22 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑌 ∈ 𝐵 ) |
| 8 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
| 9 |
1 8
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 10 |
6 7 9
|
syl2anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 11 |
|
simp21 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑋 ∈ 𝐵 ) |
| 12 |
1 8
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 13 |
6 11 12
|
syl2anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 14 |
|
simp23 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑍 ∈ 𝐵 ) |
| 15 |
1 8
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) |
| 16 |
6 14 15
|
syl2anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) |
| 17 |
1 8 3
|
cvrcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 18 |
17
|
3adant3r2 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 19 |
1 8 3
|
cvrcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 20 |
19
|
3adant3r1 |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 21 |
18 20
|
anbi12d |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) |
| 22 |
21
|
biimp3a |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 23 |
22
|
ancomd |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 24 |
1 2 3
|
cvrcmp |
⊢ ( ( 𝐾 ∈ Poset ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 25 |
5 10 13 16 23 24
|
syl131anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 26 |
1 2 8
|
oplecon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 27 |
6 11 7 26
|
syl3anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 28 |
1 8
|
opcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 29 |
6 11 7 28
|
syl3anc |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 = 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 30 |
25 27 29
|
3bitr4d |
⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) ) |