Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-alg Unicode version

Definition df-alg 25716
Description:  Ded and  Cat
OLD structure. Metamath for internal reasons doesn't like too large definitions. Then  Cat OLD has been split giving birth to  Ded and  Alg. If  Ded has a real mathematical use,  Alg is only here to give relief to Metamath. (Contributed by FL, 24-Oct-2007.)
Assertion
Ref Expression
df-alg  |-  Alg  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) ) }
Distinct variable group:    x, d, c, j, r

Detailed syntax breakdown of Definition df-alg
StepHypRef Expression
1 calg 25711 . 2  class  Alg
2 vx . . . . . . . . . 10  set  x
32cv 1622 . . . . . . . . 9  class  x
4 vd . . . . . . . . . . . 12  set  d
54cv 1622 . . . . . . . . . . 11  class  d
6 vc . . . . . . . . . . . 12  set  c
76cv 1622 . . . . . . . . . . 11  class  c
85, 7cop 3643 . . . . . . . . . 10  class  <. d ,  c >.
9 vj . . . . . . . . . . . 12  set  j
109cv 1622 . . . . . . . . . . 11  class  j
11 vr . . . . . . . . . . . 12  set  r
1211cv 1622 . . . . . . . . . . 11  class  r
1310, 12cop 3643 . . . . . . . . . 10  class  <. j ,  r >.
148, 13cop 3643 . . . . . . . . 9  class  <. <. d ,  c >. ,  <. j ,  r >. >.
153, 14wceq 1623 . . . . . . . 8  wff  x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.
165cdm 4689 . . . . . . . . . 10  class  dom  d
1710cdm 4689 . . . . . . . . . 10  class  dom  j
1816, 17, 5wf 5251 . . . . . . . . 9  wff  d : dom  d --> dom  j
1916, 17, 7wf 5251 . . . . . . . . 9  wff  c : dom  d --> dom  j
2017, 16, 10wf 5251 . . . . . . . . 9  wff  j : dom  j --> dom  d
2118, 19, 20w3a 934 . . . . . . . 8  wff  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d )
2212wfun 5249 . . . . . . . . 9  wff  Fun  r
2312cdm 4689 . . . . . . . . . 10  class  dom  r
2416, 16cxp 4687 . . . . . . . . . 10  class  ( dom  d  X.  dom  d
)
2523, 24wss 3152 . . . . . . . . 9  wff  dom  r  C_  ( dom  d  X. 
dom  d )
2612crn 4690 . . . . . . . . . 10  class  ran  r
2726, 16wss 3152 . . . . . . . . 9  wff  ran  r  C_ 
dom  d
2822, 25, 27w3a 934 . . . . . . . 8  wff  ( Fun  r  /\  dom  r  C_  ( dom  d  X. 
dom  d )  /\  ran  r  C_  dom  d
)
2915, 21, 28w3a 934 . . . . . . 7  wff  ( x  =  <. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) )
3029, 11wex 1528 . . . . . 6  wff  E. r
( x  =  <. <.
d ,  c >. ,  <. j ,  r
>. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) )
3130, 9wex 1528 . . . . 5  wff  E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) )
3231, 6wex 1528 . . . 4  wff  E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d )  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X. 
dom  d )  /\  ran  r  C_  dom  d
) )
3332, 4wex 1528 . . 3  wff  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) )
3433, 2cab 2269 . 2  class  { x  |  E. d E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d )  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X. 
dom  d )  /\  ran  r  C_  dom  d
) ) }
351, 34wceq 1623 1  wff  Alg  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( d : dom  d --> dom  j  /\  c : dom  d --> dom  j  /\  j : dom  j --> dom  d
)  /\  ( Fun  r  /\  dom  r  C_  ( dom  d  X.  dom  d )  /\  ran  r  C_  dom  d ) ) }
Colors of variables: wff set class
This definition is referenced by:  isalg  25721  algi  25727
  Copyright terms: Public domain W3C validator