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 19291
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𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
Distinct variable group:   ,𝑖,𝑟,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ltbag
StepHypRef Expression
1 cltb 19286 . 2 class <bag
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3189 . . 3 class V
5 vx . . . . . . . 8 setvar 𝑥
65cv 1479 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1479 . . . . . . 7 class 𝑦
96, 8cpr 4155 . . . . . 6 class {𝑥, 𝑦}
10 vh . . . . . . . . . . 11 setvar
1110cv 1479 . . . . . . . . . 10 class
1211ccnv 5078 . . . . . . . . 9 class
13 cn 10972 . . . . . . . . 9 class
1412, 13cima 5082 . . . . . . . 8 class ( “ ℕ)
15 cfn 7907 . . . . . . . 8 class Fin
1614, 15wcel 1987 . . . . . . 7 wff ( “ ℕ) ∈ Fin
17 cn0 11244 . . . . . . . 8 class 0
183cv 1479 . . . . . . . 8 class 𝑖
19 cmap 7809 . . . . . . . 8 class 𝑚
2017, 18, 19co 6610 . . . . . . 7 class (ℕ0𝑚 𝑖)
2116, 10, 20crab 2911 . . . . . 6 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
229, 21wss 3559 . . . . 5 wff {𝑥, 𝑦} ⊆ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
23 vz . . . . . . . . . 10 setvar 𝑧
2423cv 1479 . . . . . . . . 9 class 𝑧
2524, 6cfv 5852 . . . . . . . 8 class (𝑥𝑧)
2624, 8cfv 5852 . . . . . . . 8 class (𝑦𝑧)
27 clt 10026 . . . . . . . 8 class <
2825, 26, 27wbr 4618 . . . . . . 7 wff (𝑥𝑧) < (𝑦𝑧)
29 vw . . . . . . . . . . 11 setvar 𝑤
3029cv 1479 . . . . . . . . . 10 class 𝑤
312cv 1479 . . . . . . . . . 10 class 𝑟
3224, 30, 31wbr 4618 . . . . . . . . 9 wff 𝑧𝑟𝑤
3330, 6cfv 5852 . . . . . . . . . 10 class (𝑥𝑤)
3430, 8cfv 5852 . . . . . . . . . 10 class (𝑦𝑤)
3533, 34wceq 1480 . . . . . . . . 9 wff (𝑥𝑤) = (𝑦𝑤)
3632, 35wi 4 . . . . . . . 8 wff (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3736, 29, 18wral 2907 . . . . . . 7 wff 𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))
3828, 37wa 384 . . . . . 6 wff ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
3938, 23, 18wrex 2908 . . . . 5 wff 𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤)))
4022, 39wa 384 . . . 4 wff ({𝑥, 𝑦} ⊆ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))
4140, 5, 7copab 4677 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))}
422, 3, 4, 4, 41cmpt2 6612 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
431, 42wceq 1480 1 wff <bag = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∧ ∃𝑧𝑖 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝑖 (𝑧𝑟𝑤 → (𝑥𝑤) = (𝑦𝑤))))})
Colors of variables: wff setvar class
This definition is referenced by:  ltbval  19403
  Copyright terms: Public domain W3C validator