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}={\mathrm{Base}}_{{K}}$
cmtfval.j
cmtfval.m
cmtfval.o
cmtfval.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion cmtfvalN

Proof

Step Hyp Ref Expression
1 cmtfval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cmtfval.j
3 cmtfval.m
4 cmtfval.o
5 cmtfval.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
6 elex ${⊢}{K}\in {A}\to {K}\in \mathrm{V}$
7 fveq2 ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={\mathrm{Base}}_{{K}}$
8 7 1 eqtr4di ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={B}$
9 8 eleq2d ${⊢}{p}={K}\to \left({x}\in {\mathrm{Base}}_{{p}}↔{x}\in {B}\right)$
10 8 eleq2d ${⊢}{p}={K}\to \left({y}\in {\mathrm{Base}}_{{p}}↔{y}\in {B}\right)$
11 fveq2 ${⊢}{p}={K}\to \mathrm{join}\left({p}\right)=\mathrm{join}\left({K}\right)$
12 11 2 eqtr4di
13 fveq2 ${⊢}{p}={K}\to \mathrm{meet}\left({p}\right)=\mathrm{meet}\left({K}\right)$
14 13 3 eqtr4di
15 14 oveqd
16 eqidd ${⊢}{p}={K}\to {x}={x}$
17 fveq2 ${⊢}{p}={K}\to \mathrm{oc}\left({p}\right)=\mathrm{oc}\left({K}\right)$
18 17 4 eqtr4di
19 18 fveq1d
20 14 16 19 oveq123d
21 12 15 20 oveq123d
22 21 eqeq2d
23 9 10 22 3anbi123d
24 23 opabbidv
25 df-cmtN ${⊢}\mathrm{cm}=\left({p}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)\right\}\right)$
26 df-3an
27 26 opabbii
28 1 fvexi ${⊢}{B}\in \mathrm{V}$
29 28 28 xpex ${⊢}{B}×{B}\in \mathrm{V}$
30 opabssxp
31 29 30 ssexi
32 27 31 eqeltri
33 24 25 32 fvmpt
34 5 33 syl5eq
35 6 34 syl