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

Definition df-ltbag 16424
 Description: Define a well-order on the set of all finite bags from the index set given a wellordering of . (Contributed by Mario Carneiro, 8-Feb-2015.)
Assertion
Ref Expression
df-ltbag bag
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-ltbag
StepHypRef Expression
1 cltb 16413 . 2 bag
2 vr . . 3
3 vi . . 3
4 cvv 2956 . . 3
5 vx . . . . . . . 8
65cv 1651 . . . . . . 7
7 vy . . . . . . . 8
87cv 1651 . . . . . . 7
96, 8cpr 3815 . . . . . 6
10 vh . . . . . . . . . . 11
1110cv 1651 . . . . . . . . . 10
1211ccnv 4877 . . . . . . . . 9
13 cn 10000 . . . . . . . . 9
1412, 13cima 4881 . . . . . . . 8
15 cfn 7109 . . . . . . . 8
1614, 15wcel 1725 . . . . . . 7
17 cn0 10221 . . . . . . . 8
183cv 1651 . . . . . . . 8
19 cmap 7018 . . . . . . . 8
2017, 18, 19co 6081 . . . . . . 7
2116, 10, 20crab 2709 . . . . . 6
229, 21wss 3320 . . . . 5
23 vz . . . . . . . . . 10
2423cv 1651 . . . . . . . . 9
2524, 6cfv 5454 . . . . . . . 8
2624, 8cfv 5454 . . . . . . . 8
27 clt 9120 . . . . . . . 8
2825, 26, 27wbr 4212 . . . . . . 7
29 vw . . . . . . . . . . 11
3029cv 1651 . . . . . . . . . 10
312cv 1651 . . . . . . . . . 10
3224, 30, 31wbr 4212 . . . . . . . . 9
3330, 6cfv 5454 . . . . . . . . . 10
3430, 8cfv 5454 . . . . . . . . . 10
3533, 34wceq 1652 . . . . . . . . 9
3632, 35wi 4 . . . . . . . 8
3736, 29, 18wral 2705 . . . . . . 7
3828, 37wa 359 . . . . . 6
3938, 23, 18wrex 2706 . . . . 5
4022, 39wa 359 . . . 4
4140, 5, 7copab 4265 . . 3
422, 3, 4, 4, 41cmpt2 6083 . 2
431, 42wceq 1652 1 bag
 Colors of variables: wff set class This definition is referenced by:  ltbval  16532
 Copyright terms: Public domain W3C validator