MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ltbag Unicode version

Definition df-ltbag 16105
Description: Define a well-order on the set of all finite bags from the index set  i given a wellordering  r of  i. (Contributed by Mario Carneiro, 8-Feb-2015.)
Assertion
Ref Expression
df-ltbag  |-  <bag  =  ( r  e.  _V , 
i  e.  _V  |->  {
<. x ,  y >.  |  ( { x ,  y }  C_  { h  e.  ( NN0 
^m  i )  |  ( `' h " NN )  e.  Fin }  /\  E. z  e.  i  ( ( x `
 z )  < 
( y `  z
)  /\  A. w  e.  i  ( z
r w  ->  (
x `  w )  =  ( y `  w ) ) ) ) } )
Distinct variable group:    h, i, r, w, x, y, z

Detailed syntax breakdown of Definition df-ltbag
StepHypRef Expression
1 cltb 16094 . 2  class  <bag
2 vr . . 3  set  r
3 vi . . 3  set  i
4 cvv 2788 . . 3  class  _V
5 vx . . . . . . . 8  set  x
65cv 1622 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1622 . . . . . . 7  class  y
96, 8cpr 3641 . . . . . 6  class  { x ,  y }
10 vh . . . . . . . . . . 11  set  h
1110cv 1622 . . . . . . . . . 10  class  h
1211ccnv 4688 . . . . . . . . 9  class  `' h
13 cn 9746 . . . . . . . . 9  class  NN
1412, 13cima 4692 . . . . . . . 8  class  ( `' h " NN )
15 cfn 6863 . . . . . . . 8  class  Fin
1614, 15wcel 1684 . . . . . . 7  wff  ( `' h " NN )  e.  Fin
17 cn0 9965 . . . . . . . 8  class  NN0
183cv 1622 . . . . . . . 8  class  i
19 cmap 6772 . . . . . . . 8  class  ^m
2017, 18, 19co 5858 . . . . . . 7  class  ( NN0 
^m  i )
2116, 10, 20crab 2547 . . . . . 6  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
229, 21wss 3152 . . . . 5  wff  { x ,  y }  C_  { h  e.  ( NN0 
^m  i )  |  ( `' h " NN )  e.  Fin }
23 vz . . . . . . . . . 10  set  z
2423cv 1622 . . . . . . . . 9  class  z
2524, 6cfv 5255 . . . . . . . 8  class  ( x `
 z )
2624, 8cfv 5255 . . . . . . . 8  class  ( y `
 z )
27 clt 8867 . . . . . . . 8  class  <
2825, 26, 27wbr 4023 . . . . . . 7  wff  ( x `
 z )  < 
( y `  z
)
29 vw . . . . . . . . . . 11  set  w
3029cv 1622 . . . . . . . . . 10  class  w
312cv 1622 . . . . . . . . . 10  class  r
3224, 30, 31wbr 4023 . . . . . . . . 9  wff  z r w
3330, 6cfv 5255 . . . . . . . . . 10  class  ( x `
 w )
3430, 8cfv 5255 . . . . . . . . . 10  class  ( y `
 w )
3533, 34wceq 1623 . . . . . . . . 9  wff  ( x `
 w )  =  ( y `  w
)
3632, 35wi 4 . . . . . . . 8  wff  ( z r w  ->  (
x `  w )  =  ( y `  w ) )
3736, 29, 18wral 2543 . . . . . . 7  wff  A. w  e.  i  ( z
r w  ->  (
x `  w )  =  ( y `  w ) )
3828, 37wa 358 . . . . . 6  wff  ( ( x `  z )  <  ( y `  z )  /\  A. w  e.  i  (
z r w  -> 
( x `  w
)  =  ( y `
 w ) ) )
3938, 23, 18wrex 2544 . . . . 5  wff  E. z  e.  i  ( (
x `  z )  <  ( y `  z
)  /\  A. w  e.  i  ( z
r w  ->  (
x `  w )  =  ( y `  w ) ) )
4022, 39wa 358 . . . 4  wff  ( { x ,  y } 
C_  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  /\  E. z  e.  i  ( ( x `  z
)  <  ( y `  z )  /\  A. w  e.  i  (
z r w  -> 
( x `  w
)  =  ( y `
 w ) ) ) )
4140, 5, 7copab 4076 . . 3  class  { <. x ,  y >.  |  ( { x ,  y }  C_  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  /\  E. z  e.  i  ( ( x `  z
)  <  ( y `  z )  /\  A. w  e.  i  (
z r w  -> 
( x `  w
)  =  ( y `
 w ) ) ) ) }
422, 3, 4, 4, 41cmpt2 5860 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  { <. x ,  y >.  |  ( { x ,  y }  C_  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  /\  E. z  e.  i  ( ( x `  z
)  <  ( y `  z )  /\  A. w  e.  i  (
z r w  -> 
( x `  w
)  =  ( y `
 w ) ) ) ) } )
431, 42wceq 1623 1  wff  <bag  =  ( r  e.  _V , 
i  e.  _V  |->  {
<. x ,  y >.  |  ( { x ,  y }  C_  { h  e.  ( NN0 
^m  i )  |  ( `' h " NN )  e.  Fin }  /\  E. z  e.  i  ( ( x `
 z )  < 
( y `  z
)  /\  A. w  e.  i  ( z
r w  ->  (
x `  w )  =  ( y `  w ) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ltbval  16213
  Copyright terms: Public domain W3C validator