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 ) ) ) ) } )