Definition df-ltbag 21933

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 = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))})

Distinct variable group:   ℎ,𝑖,𝑟,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ltbag

Step	Hyp	Ref	Expression
1		cltb 21928	. 2 class <bag
2		vr	. . 3 setvar 𝑟
3		vi	. . 3 setvar 𝑖
4		cvv 3479	. . 3 class V
5		vx	. . . . . . . 8 setvar 𝑥
6	5	cv 1538	. . . . . . 7 class 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1538	. . . . . . 7 class 𝑦
9	6, 8	cpr 4627	. . . . . 6 class {𝑥, 𝑦}
10		vh	. . . . . . . . . . 11 setvar ℎ
11	10	cv 1538	. . . . . . . . . 10 class ℎ
12	11	ccnv 5683	. . . . . . . . 9 class ◡ℎ
13		cn 12267	. . . . . . . . 9 class ℕ
14	12, 13	cima 5687	. . . . . . . 8 class (◡ℎ “ ℕ)
15		cfn 8986	. . . . . . . 8 class Fin
16	14, 15	wcel 2107	. . . . . . 7 wff (◡ℎ “ ℕ) ∈ Fin
17		cn0 12528	. . . . . . . 8 class ℕ0
18	3	cv 1538	. . . . . . . 8 class 𝑖
19		cmap 8867	. . . . . . . 8 class ↑m
20	17, 18, 19	co 7432	. . . . . . 7 class (ℕ0 ↑m 𝑖)
21	16, 10, 20	crab 3435	. . . . . 6 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
22	9, 21	wss 3950	. . . . 5 wff {𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
23		vz	. . . . . . . . . 10 setvar 𝑧
24	23	cv 1538	. . . . . . . . 9 class 𝑧
25	24, 6	cfv 6560	. . . . . . . 8 class (𝑥‘𝑧)
26	24, 8	cfv 6560	. . . . . . . 8 class (𝑦‘𝑧)
27		clt 11296	. . . . . . . 8 class <
28	25, 26, 27	wbr 5142	. . . . . . 7 wff (𝑥‘𝑧) < (𝑦‘𝑧)
29		vw	. . . . . . . . . . 11 setvar 𝑤
30	29	cv 1538	. . . . . . . . . 10 class 𝑤
31	2	cv 1538	. . . . . . . . . 10 class 𝑟
32	24, 30, 31	wbr 5142	. . . . . . . . 9 wff 𝑧𝑟𝑤
33	30, 6	cfv 6560	. . . . . . . . . 10 class (𝑥‘𝑤)
34	30, 8	cfv 6560	. . . . . . . . . 10 class (𝑦‘𝑤)
35	33, 34	wceq 1539	. . . . . . . . 9 wff (𝑥‘𝑤) = (𝑦‘𝑤)
36	32, 35	wi 4	. . . . . . . 8 wff (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))
37	36, 29, 18	wral 3060	. . . . . . 7 wff ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))
38	28, 37	wa 395	. . . . . 6 wff ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))
39	38, 23, 18	wrex 3069	. . . . 5 wff ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))
40	22, 39	wa 395	. . . 4 wff ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
41	40, 5, 7	copab 5204	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}
42	2, 3, 4, 4, 41	cmpo 7434	. 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))})
43	1, 42	wceq 1539	1 wff <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))})

This definition is referenced by:  ltbval  22062