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	$$⊢{<}_{bag}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltb	$$class{<}_{bag}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4		vx	$$setvarx$$
5		vy	$$setvary$$
6	4	cv	$$setvarx$$
7	5	cv	$$setvary$$
8	6 7	cpr	$$class\left\{x,y\right\}$$
9		vh	$$setvarh$$
10		cn0	$$class{\mathbb{N}}_0$$
11		cmap	$$class{\uparrow }_{𝑚}$$
12	3	cv	$$setvari$$
13	10 12 11	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
14	9	cv	$$setvarh$$
15	14	ccnv	$$class{h}^{-1}$$
16		cn	$$class\mathbb{N}$$
17	15 16	cima	$$class{h}^{-1}\left[\mathbb{N}\right]$$
18		cfn	$$class\mathrm{Fin}$$
19	17 18	wcel	$$wff{h}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
20	19 9 13	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
21	8 20	wss	$$wff\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
22		vz	$$setvarz$$
23	22	cv	$$setvarz$$
24	23 6	cfv	$$classx\left(z\right)$$
25		clt	$$class<$$
26	23 7	cfv	$$classy\left(z\right)$$
27	24 26 25	wbr	$$wffx\left(z\right)<y\left(z\right)$$
28		vw	$$setvarw$$
29	1	cv	$$setvarr$$
30	28	cv	$$setvarw$$
31	23 30 29	wbr	$$wffzrw$$
32	30 6	cfv	$$classx\left(w\right)$$
33	30 7	cfv	$$classy\left(w\right)$$
34	32 33	wceq	$$wffx\left(w\right)=y\left(w\right)$$
35	31 34	wi	$$wff\left(zrw\to x\left(w\right)=y\left(w\right)\right)$$
36	35 28 12	wral	$$wff\forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)$$
37	27 36	wa	$$wff\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)$$
38	37 22 12	wrex	$$wff\exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)$$
39	21 38	wa	$$wff\left(\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)\right)$$
40	39 4 5	copab	$$class\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)\right)\right\}$$
41	1 3 2 2 40	cmpo	$$class\left(r\in \mathrm{V},i\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)\right)\right\}\right)$$
42	0 41	wceq	$$wff{<}_{bag}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \exists z\in i\left(x\left(z\right)<y\left(z\right)\wedge \forall w\in i\left(zrw\to x\left(w\right)=y\left(w\right)\right)\right)\right)\right\}\right)$$