# Metamath Proof Explorer

## Theorem cmtfvalN

Description: Value of commutes relation. (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtfval.b
`|- B = ( Base ` K )`
cmtfval.j
`|- .\/ = ( join ` K )`
cmtfval.m
`|- ./\ = ( meet ` K )`
cmtfval.o
`|- ._|_ = ( oc ` K )`
cmtfval.c
`|- C = ( cm ` K )`
Assertion cmtfvalN
`|- ( K e. A -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )`

### Proof

Step Hyp Ref Expression
1 cmtfval.b
` |-  B = ( Base ` K )`
2 cmtfval.j
` |-  .\/ = ( join ` K )`
3 cmtfval.m
` |-  ./\ = ( meet ` K )`
4 cmtfval.o
` |-  ._|_ = ( oc ` K )`
5 cmtfval.c
` |-  C = ( cm ` K )`
6 elex
` |-  ( K e. A -> K e. _V )`
7 fveq2
` |-  ( p = K -> ( Base ` p ) = ( Base ` K ) )`
8 7 1 eqtr4di
` |-  ( p = K -> ( Base ` p ) = B )`
9 8 eleq2d
` |-  ( p = K -> ( x e. ( Base ` p ) <-> x e. B ) )`
10 8 eleq2d
` |-  ( p = K -> ( y e. ( Base ` p ) <-> y e. B ) )`
11 fveq2
` |-  ( p = K -> ( join ` p ) = ( join ` K ) )`
12 11 2 eqtr4di
` |-  ( p = K -> ( join ` p ) = .\/ )`
13 fveq2
` |-  ( p = K -> ( meet ` p ) = ( meet ` K ) )`
14 13 3 eqtr4di
` |-  ( p = K -> ( meet ` p ) = ./\ )`
15 14 oveqd
` |-  ( p = K -> ( x ( meet ` p ) y ) = ( x ./\ y ) )`
16 eqidd
` |-  ( p = K -> x = x )`
17 fveq2
` |-  ( p = K -> ( oc ` p ) = ( oc ` K ) )`
18 17 4 eqtr4di
` |-  ( p = K -> ( oc ` p ) = ._|_ )`
19 18 fveq1d
` |-  ( p = K -> ( ( oc ` p ) ` y ) = ( ._|_ ` y ) )`
20 14 16 19 oveq123d
` |-  ( p = K -> ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) = ( x ./\ ( ._|_ ` y ) ) )`
21 12 15 20 oveq123d
` |-  ( p = K -> ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) )`
22 21 eqeq2d
` |-  ( p = K -> ( x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) <-> x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) )`
23 9 10 22 3anbi123d
` |-  ( p = K -> ( ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) <-> ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) ) )`
24 23 opabbidv
` |-  ( p = K -> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )`
25 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 ) ) ) ) } )`
26 df-3an
` |-  ( ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) <-> ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) )`
27 26 opabbii
` |-  { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) }`
28 1 fvexi
` |-  B e. _V`
29 28 28 xpex
` |-  ( B X. B ) e. _V`
30 opabssxp
` |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } C_ ( B X. B )`
31 29 30 ssexi
` |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } e. _V`
32 27 31 eqeltri
` |-  { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } e. _V`
33 24 25 32 fvmpt
` |-  ( K e. _V -> ( cm ` K ) = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )`
34 5 33 syl5eq
` |-  ( K e. _V -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )`
35 6 34 syl
` |-  ( K e. A -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )`