Definition df-ltbag 19359

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

Step	Hyp	Ref	Expression
1		cltb 19354	. 2 class <bag
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 3200	. . 3 class _V
5		vx	. . . . . . . 8 setvar x
6	5	cv 1482	. . . . . . 7 class x
7		vy	. . . . . . . 8 setvar y
8	7	cv 1482	. . . . . . 7 class y
9	6, 8	cpr 4179	. . . . . 6 class { x , y }
10		vh	. . . . . . . . . . 11 setvar h
11	10	cv 1482	. . . . . . . . . 10 class h
12	11	ccnv 5113	. . . . . . . . 9 class `' h
13		cn 11020	. . . . . . . . 9 class NN
14	12, 13	cima 5117	. . . . . . . 8 class ( `' h " NN )
15		cfn 7955	. . . . . . . 8 class Fin
16	14, 15	wcel 1990	. . . . . . 7 wff ( `' h " NN ) e. Fin
17		cn0 11292	. . . . . . . 8 class NN0
18	3	cv 1482	. . . . . . . 8 class i
19		cmap 7857	. . . . . . . 8 class ^m
20	17, 18, 19	co 6650	. . . . . . 7 class ( NN0 ^m i )
21	16, 10, 20	crab 2916	. . . . . 6 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
22	9, 21	wss 3574	. . . . 5 wff { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
23		vz	. . . . . . . . . 10 setvar z
24	23	cv 1482	. . . . . . . . 9 class z
25	24, 6	cfv 5888	. . . . . . . 8 class ( x ` z )
26	24, 8	cfv 5888	. . . . . . . 8 class ( y ` z )
27		clt 10074	. . . . . . . 8 class <
28	25, 26, 27	wbr 4653	. . . . . . 7 wff ( x ` z ) < ( y ` z )
29		vw	. . . . . . . . . . 11 setvar w
30	29	cv 1482	. . . . . . . . . 10 class w
31	2	cv 1482	. . . . . . . . . 10 class r
32	24, 30, 31	wbr 4653	. . . . . . . . 9 wff z r w
33	30, 6	cfv 5888	. . . . . . . . . 10 class ( x ` w )
34	30, 8	cfv 5888	. . . . . . . . . 10 class ( y ` w )
35	33, 34	wceq 1483	. . . . . . . . 9 wff ( x ` w ) = ( y ` w )
36	32, 35	wi 4	. . . . . . . 8 wff ( z r w -> ( x ` w ) = ( y ` w ) )
37	36, 29, 18	wral 2912	. . . . . . 7 wff A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) )
38	28, 37	wa 384	. . . . . 6 wff ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) )
39	38, 23, 18	wrex 2913	. . . . 5 wff E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) )
40	22, 39	wa 384	. . . 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 ) ) ) )
41	40, 5, 7	copab 4712	. . 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 ) ) ) ) }
42	2, 3, 4, 4, 41	cmpt2 6652	. 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 ) ) ) ) } )
43	1, 42	wceq 1483	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 ) ) ) ) } )

This definition is referenced by:  ltbval  19471