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

Definition df-ltbag 20871
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 20866 . 2 class <bag
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3408 . . 3 class V
5 vx . . . . . . . 8 setvar 𝑥
65cv 1542 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1542 . . . . . . 7 class 𝑦
96, 8cpr 4543 . . . . . 6 class {𝑥, 𝑦}
10 vh . . . . . . . . . . 11 setvar
1110cv 1542 . . . . . . . . . 10 class
1211ccnv 5550 . . . . . . . . 9 class
13 cn 11830 . . . . . . . . 9 class
1412, 13cima 5554 . . . . . . . 8 class ( “ ℕ)
15 cfn 8626 . . . . . . . 8 class Fin
1614, 15wcel 2110 . . . . . . 7 wff ( “ ℕ) ∈ Fin
17 cn0 12090 . . . . . . . 8 class 0
183cv 1542 . . . . . . . 8 class 𝑖
19 cmap 8508 . . . . . . . 8 class m
2017, 18, 19co 7213 . . . . . . 7 class (ℕ0m 𝑖)
2116, 10, 20crab 3065 . . . . . 6 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
229, 21wss 3866 . . . . 5 wff {𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
23 vz . . . . . . . . . 10 setvar 𝑧
2423cv 1542 . . . . . . . . 9 class 𝑧
2524, 6cfv 6380 . . . . . . . 8 class (𝑥𝑧)
2624, 8cfv 6380 . . . . . . . 8 class (𝑦𝑧)
27 clt 10867 . . . . . . . 8 class <
2825, 26, 27wbr 5053 . . . . . . 7 wff (𝑥𝑧) < (𝑦𝑧)
29 vw . . . . . . . . . . 11 setvar 𝑤
3029cv 1542 . . . . . . . . . 10 class 𝑤
312cv 1542 . . . . . . . . . 10 class 𝑟
3224, 30, 31wbr 5053 . . . . . . . . 9 wff 𝑧𝑟𝑤
3330, 6cfv 6380 . . . . . . . . . 10 class (𝑥𝑤)
3430, 8cfv 6380 . . . . . . . . . 10 class (𝑦𝑤)
3533, 34wceq 1543 . . . . . . . . 9 wff (𝑥𝑤) = (𝑦𝑤)
3632, 35wi 4 . . . . . . . 8 wff (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3736, 29, 18wral 3061 . . . . . . 7 wff 𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3828, 37wa 399 . . . . . 6 wff ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
3938, 23, 18wrex 3062 . . . . 5 wff 𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
4022, 39wa 399 . . . 4 wff ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))
4140, 5, 7copab 5115 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))}
422, 3, 4, 4, 41cmpo 7215 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
431, 42wceq 1543 1 wff <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
Colors of variables: wff setvar class
This definition is referenced by:  ltbval  21000
  Copyright terms: Public domain W3C validator