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

Definition df-ltbag 20603
 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 ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
Distinct variable group:   ,𝑖,𝑟,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ltbag
StepHypRef Expression
1 cltb 20598 . 2 class <bag
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3441 . . 3 class V
5 vx . . . . . . . 8 setvar 𝑥
65cv 1537 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1537 . . . . . . 7 class 𝑦
96, 8cpr 4527 . . . . . 6 class {𝑥, 𝑦}
10 vh . . . . . . . . . . 11 setvar
1110cv 1537 . . . . . . . . . 10 class
1211ccnv 5519 . . . . . . . . 9 class
13 cn 11628 . . . . . . . . 9 class
1412, 13cima 5523 . . . . . . . 8 class ( “ ℕ)
15 cfn 8495 . . . . . . . 8 class Fin
1614, 15wcel 2111 . . . . . . 7 wff ( “ ℕ) ∈ Fin
17 cn0 11888 . . . . . . . 8 class 0
183cv 1537 . . . . . . . 8 class 𝑖
19 cmap 8392 . . . . . . . 8 class m
2017, 18, 19co 7136 . . . . . . 7 class (ℕ0m 𝑖)
2116, 10, 20crab 3110 . . . . . 6 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
229, 21wss 3881 . . . . 5 wff {𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
23 vz . . . . . . . . . 10 setvar 𝑧
2423cv 1537 . . . . . . . . 9 class 𝑧
2524, 6cfv 6325 . . . . . . . 8 class (𝑥𝑧)
2624, 8cfv 6325 . . . . . . . 8 class (𝑦𝑧)
27 clt 10667 . . . . . . . 8 class <
2825, 26, 27wbr 5031 . . . . . . 7 wff (𝑥𝑧) < (𝑦𝑧)
29 vw . . . . . . . . . . 11 setvar 𝑤
3029cv 1537 . . . . . . . . . 10 class 𝑤
312cv 1537 . . . . . . . . . 10 class 𝑟
3224, 30, 31wbr 5031 . . . . . . . . 9 wff 𝑧𝑟𝑤
3330, 6cfv 6325 . . . . . . . . . 10 class (𝑥𝑤)
3430, 8cfv 6325 . . . . . . . . . 10 class (𝑦𝑤)
3533, 34wceq 1538 . . . . . . . . 9 wff (𝑥𝑤) = (𝑦𝑤)
3632, 35wi 4 . . . . . . . 8 wff (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3736, 29, 18wral 3106 . . . . . . 7 wff 𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3828, 37wa 399 . . . . . 6 wff ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
3938, 23, 18wrex 3107 . . . . 5 wff 𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
4022, 39wa 399 . . . 4 wff ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))
4140, 5, 7copab 5093 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))}
422, 3, 4, 4, 41cmpo 7138 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
431, 42wceq 1538 1 wff <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
 Colors of variables: wff setvar class This definition is referenced by:  ltbval  20719
 Copyright terms: Public domain W3C validator