This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ltbag

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)

Ref Expression
Assertion df-ltbag 
|-  { <. 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 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltb 
 |-
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vi 
 |-  i
4 vx 
 |-  x
5 vy 
 |-  y
6 4 cv 
 |-  x
7 5 cv 
 |-  y
8 6 7 cpr 
 |-  { x , y }
9 vh 
 |-  h
10 cn0 
 |-  NN0
11 cmap 
 |-  ^m
12 3 cv 
 |-  i
13 10 12 11 co 
 |-  ( NN0 ^m i )
14 9 cv 
 |-  h
15 14 ccnv 
 |-  `' h
16 cn 
 |-  NN
17 15 16 cima 
 |-  ( `' h " NN )
18 cfn 
 |-  Fin
19 17 18 wcel 
 |-  ( `' h " NN ) e. Fin
20 19 9 13 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
21 8 20 wss 
 |-  { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
22 vz 
 |-  z
23 22 cv 
 |-  z
24 23 6 cfv 
 |-  ( x ` z )
25 clt 
 |-  <
26 23 7 cfv 
 |-  ( y ` z )
27 24 26 25 wbr 
 |-  ( x ` z ) < ( y ` z )
28 vw 
 |-  w
29 1 cv 
 |-  r
30 28 cv 
 |-  w
31 23 30 29 wbr 
 |-  z r w
32 30 6 cfv 
 |-  ( x ` w )
33 30 7 cfv 
 |-  ( y ` w )
34 32 33 wceq 
 |-  ( x ` w ) = ( y ` w )
35 31 34 wi 
 |-  ( z r w -> ( x ` w ) = ( y ` w ) )
36 35 28 12 wral 
 |-  A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) )
37 27 36 wa 
 |-  ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) )
38 37 22 12 wrex 
 |-  E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) )
39 21 38 wa 
 |-  ( { 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 ) ) ) )
40 39 4 5 copab 
 |-  { <. 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 ) ) ) ) }
41 1 3 2 2 40 cmpo 
 |-  ( 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 ) ) ) ) } )
42 0 41 wceq 
 |-   { <. 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 ) ) ) ) } )