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 ⊢ < bag = r ∈ V , i ∈ V ⟼ x y | x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ∧ ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltb class < bag
1 vr setvar r
2 cvv class V
3 vi setvar i
4 vx setvar x
5 vy setvar y
6 4 cv setvar x
7 5 cv setvar y
8 6 7 cpr class x y
9 vh setvar h
10 cn0 class ℕ 0
11 cmap class ↑ 𝑚
12 3 cv setvar i
13 10 12 11 co class ℕ 0 i
14 9 cv setvar h
15 14 ccnv class h -1
16 cn class ℕ
17 15 16 cima class h -1 ℕ
18 cfn class Fin
19 17 18 wcel wff h -1 ℕ ∈ Fin
20 19 9 13 crab class h ∈ ℕ 0 i | h -1 ℕ ∈ Fin
21 8 20 wss wff x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin
22 vz setvar z
23 22 cv setvar z
24 23 6 cfv class x ⁡ z
25 clt class <
26 23 7 cfv class y ⁡ z
27 24 26 25 wbr wff x ⁡ z < y ⁡ z
28 vw setvar w
29 1 cv setvar r
30 28 cv setvar w
31 23 30 29 wbr wff z r w
32 30 6 cfv class x ⁡ w
33 30 7 cfv class y ⁡ w
34 32 33 wceq wff x ⁡ w = y ⁡ w
35 31 34 wi wff z r w → x ⁡ w = y ⁡ w
36 35 28 12 wral wff ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
37 27 36 wa wff x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
38 37 22 12 wrex wff ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
39 21 38 wa wff x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ∧ ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
40 39 4 5 copab class x y | x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ∧ ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
41 1 3 2 2 40 cmpo class r ∈ V , i ∈ V ⟼ x y | x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ∧ ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w
42 0 41 wceq wff < bag = r ∈ V , i ∈ V ⟼ x y | x y ⊆ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ∧ ∃ z ∈ i x ⁡ z < y ⁡ z ∧ ∀ w ∈ i z r w → x ⁡ w = y ⁡ w