Table of Contents Mathbox for Norm Megill < Previous   Next > Related theorems Unicode version

Theorem cmtfval 17604
 Description: Value of commutes relation.
Hypotheses
Ref Expression
cmtfval.b Base
cmtfval.j join
cmtfval.m meet
cmtfval.o oc
cmtfval.c cm
Assertion
Ref Expression
cmtfval
Distinct variable groups:   ,,   ,,

Proof of Theorem cmtfval
StepHypRef Expression
1 elisset 2547 . 2
2 cmtfval.c . . 3 cm
3 fveq2 4765 . . . . . . . 8 Base Base
4 cmtfval.b . . . . . . . 8 Base
53, 4syl6eqr 2195 . . . . . . 7 Base
65eleq2d 2211 . . . . . 6 Base
75eleq2d 2211 . . . . . 6 Base
8 fveq2 4765 . . . . . . . . 9 join join
9 cmtfval.j . . . . . . . . 9 join
108, 9syl6eqr 2195 . . . . . . . 8 join
11 fveq2 4765 . . . . . . . . . 10 meet meet
12 cmtfval.m . . . . . . . . . 10 meet
1311, 12syl6eqr 2195 . . . . . . . . 9 meet
1413opreqd 4995 . . . . . . . 8 meet
15 eqidd 2142 . . . . . . . . 9
16 fveq2 4765 . . . . . . . . . . 11 oc oc
17 cmtfval.o . . . . . . . . . . 11 oc
1816, 17syl6eqr 2195 . . . . . . . . . 10 oc
1918fveq1d 4767 . . . . . . . . 9 oc
2013, 15, 19opreq123d 4999 . . . . . . . 8 meetoc
2110, 14, 20opreq123d 4999 . . . . . . 7 meetjoinmeetoc
2221eqeq2d 2152 . . . . . 6 meetjoinmeetoc
236, 7, 223anbi123d 1441 . . . . 5 Base Base meetjoinmeetoc
2423opabbidv 3569 . . . 4 Base Base meetjoinmeetoc
25 df-cmt 17573 . . . 4 cm Base Base meetjoinmeetoc
26 df-3an 1104 . . . . . 6
2726opabbii 3570 . . . . 5
28 fvex 4778 . . . . . . . 8 Base
294, 28eqeltri 2214 . . . . . . 7
3029, 29xpex 4226 . . . . . 6
31 opabssxp 4193 . . . . . 6
3230, 31ssexi 3623 . . . . 5
3327, 32eqeltri 2214 . . . 4
3424, 25, 33fvmpt 5119 . . 3 cm
352, 34syl5eq 2185 . 2
361, 35syl 13 1
 Colors of variables: wff set class Syntax hints:   wi 3   wa 337   w3a 1102   wceq 1586   wcel 1588  cvv 2538  copab 3565   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