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

Metamath Proof Explorer

Definition df-cmtN

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 
|- cm = ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmtN 
 |-  cm
1 vp 
 |-  p
2 cvv 
 |-  _V
3 vx 
 |-  x
4 vy 
 |-  y
5 3 cv 
 |-  x
6 cbs 
 |-  Base
7 1 cv 
 |-  p
8 7 6 cfv 
 |-  ( Base ` p )
9 5 8 wcel 
 |-  x e. ( Base ` p )
10 4 cv 
 |-  y
11 10 8 wcel 
 |-  y e. ( Base ` p )
12 cmee 
 |-  meet
13 7 12 cfv 
 |-  ( meet ` p )
14 5 10 13 co 
 |-  ( x ( meet ` p ) y )
15 cjn 
 |-  join
16 7 15 cfv 
 |-  ( join ` p )
17 coc 
 |-  oc
18 7 17 cfv 
 |-  ( oc ` p )
19 10 18 cfv 
 |-  ( ( oc ` p ) ` y )
20 5 19 13 co 
 |-  ( x ( meet ` p ) ( ( oc ` p ) ` y ) )
21 14 20 16 co 
 |-  ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) )
22 5 21 wceq 
 |-  x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) )
23 9 11 22 w3a 
 |-  ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) )
24 23 3 4 copab 
 |-  { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) }
25 1 2 24 cmpt 
 |-  ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )
26 0 25 wceq 
 |-  cm = ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )