Theorem cmtfval 17604

Description: Value of commutes relation.

Hypotheses

Ref	Expression
cmtfval.b	|- B = (Base` K)
cmtfval.j	|- J = (join` K)
cmtfval.m	|- M = (meet` K)
cmtfval.o	|- O = (oc` K)
cmtfval.c	|- C = (cm` K)

Assertion

Ref	Expression
cmtfval	|- (K e. A -> C = {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))})

Distinct variable groups:   x,y,B   x,K,y

Proof of Theorem cmtfval

Step	Hyp	Ref	Expression
1		elisset 2547	. 2 |- (K e. A -> K e. _V)
2		cmtfval.c	. . 3 |- C = (cm` K)
3		fveq2 4765	. . . . . . . 8 |- (p = K -> (Base` p) = (Base` K))
4		cmtfval.b	. . . . . . . 8 |- B = (Base` K)
5	3, 4	syl6eqr 2195	. . . . . . 7 |- (p = K -> (Base` p) = B)
6	5	eleq2d 2211	. . . . . 6 |- (p = K -> (x e. (Base` p) <-> x e. B))
7	5	eleq2d 2211	. . . . . 6 |- (p = K -> (y e. (Base` p) <-> y e. B))
8		fveq2 4765	. . . . . . . . 9 |- (p = K -> (join` p) = (join` K))
9		cmtfval.j	. . . . . . . . 9 |- J = (join` K)
10	8, 9	syl6eqr 2195	. . . . . . . 8 |- (p = K -> (join` p) = J)
11		fveq2 4765	. . . . . . . . . 10 |- (p = K -> (meet` p) = (meet` K))
12		cmtfval.m	. . . . . . . . . 10 |- M = (meet` K)
13	11, 12	syl6eqr 2195	. . . . . . . . 9 |- (p = K -> (meet` p) = M)
14	13	opreqd 4995	. . . . . . . 8 |- (p = K -> (x(meet` p)y) = (xMy))
15		eqidd 2142	. . . . . . . . 9 |- (p = K -> x = x)
16		fveq2 4765	. . . . . . . . . . 11 |- (p = K -> (oc` p) = (oc` K))
17		cmtfval.o	. . . . . . . . . . 11 |- O = (oc` K)
18	16, 17	syl6eqr 2195	. . . . . . . . . 10 |- (p = K -> (oc` p) = O)
19	18	fveq1d 4767	. . . . . . . . 9 |- (p = K -> ((oc` p)` y) = (O` y))
20	13, 15, 19	opreq123d 4999	. . . . . . . 8 |- (p = K -> (x(meet` p)((oc` p)` y)) = (xM(O` y)))
21	10, 14, 20	opreq123d 4999	. . . . . . 7 |- (p = K -> ((x(meet` p)y)(join` p)(x(meet` p)((oc` p)` y))) = ((xMy)J(xM(O` y))))
22	21	eqeq2d 2152	. . . . . 6 |- (p = K -> (x = ((x(meet` p)y)(join` p)(x(meet` p)((oc` p)` y))) <-> x = ((xMy)J(xM(O` y)))))
23	6, 7, 22	3anbi123d 1441	. . . . 5 |- (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 = ((xMy)J(xM(O` y))))))
24	23	opabbidv 3569	. . . 4 |- (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 = ((xMy)J(xM(O` y))))})
25		df-cmt 17573	. . . 4 |- 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 1104	. . . . . 6 |- ((x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y)))) <-> ((x e. B /\ y e. B) /\ x = ((xMy)J(xM(O` y)))))
27	26	opabbii 3570	. . . . 5 |- {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))} = {<.x, y>. | ((x e. B /\ y e. B) /\ x = ((xMy)J(xM(O` y))))}
28		fvex 4778	. . . . . . . 8 |- (Base` K) e. _V
29	4, 28	eqeltri 2214	. . . . . . 7 |- B e. _V
30	29, 29	xpex 4226	. . . . . 6 |- (B X. B) e. _V
31		opabssxp 4193	. . . . . 6 |- {<.x, y>. | ((x e. B /\ y e. B) /\ x = ((xMy)J(xM(O` y))))} C_ (B X. B)
32	30, 31	ssexi 3623	. . . . 5 |- {<.x, y>. | ((x e. B /\ y e. B) /\ x = ((xMy)J(xM(O` y))))} e. _V
33	27, 32	eqeltri 2214	. . . 4 |- {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))} e. _V
34	24, 25, 33	fvmpt 5119	. . 3 |- (K e. _V -> (cm` K) = {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))})
35	2, 34	syl5eq 2185	. 2 |- (K e. _V -> C = {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))})
36	1, 35	syl 13	1 |- (K e. A -> C = {<.x, y>. | (x e. B /\ y e. B /\ x = ((xMy)J(xM(O` y))))})

Syntax hints:   -> wi 3   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  _Vcvv 2538  {copab 3565   X. cxp 4117  ` cfv 4131  (class class class)co 4981  Basecbs 9437  joincjn 9542  meetcmee 9543  occoc 17566  cmccmt 17568

This theorem is referenced by:  cmtval 17605

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fv 4147  df-opr 4983  df-mpt 5099  df-cmt 17573

Copyright terms: Public domain