Description: Define the commutes relation for orthoposets. Definition of commutes in Kalmbach p. 20. (Contributed by NM, 6-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cmtN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccmtN | |
|
1 | vp | |
|
2 | cvv | |
|
3 | vx | |
|
4 | vy | |
|
5 | 3 | cv | |
6 | cbs | |
|
7 | 1 | cv | |
8 | 7 6 | cfv | |
9 | 5 8 | wcel | |
10 | 4 | cv | |
11 | 10 8 | wcel | |
12 | cmee | |
|
13 | 7 12 | cfv | |
14 | 5 10 13 | co | |
15 | cjn | |
|
16 | 7 15 | cfv | |
17 | coc | |
|
18 | 7 17 | cfv | |
19 | 10 18 | cfv | |
20 | 5 19 13 | co | |
21 | 14 20 16 | co | |
22 | 5 21 | wceq | |
23 | 9 11 22 | w3a | |
24 | 23 3 4 | copab | |
25 | 1 2 24 | cmpt | |
26 | 0 25 | wceq | |