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

Definition df-opsr 19129
Description: Define a total order on the set of all power series in 𝑠 from the index set 𝑖 given a wellordering 𝑟 of 𝑖 and a totally ordered base ring 𝑠. (Contributed by Mario Carneiro, 8-Feb-2015.)
Assertion
Ref Expression
df-opsr ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
Distinct variable group:   ,𝑑,𝑖,𝑝,𝑟,𝑠,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-opsr
StepHypRef Expression
1 copws 19124 . 2 class ordPwSer
2 vi . . 3 setvar 𝑖
3 vs . . 3 setvar 𝑠
4 cvv 3172 . . 3 class V
5 vr . . . 4 setvar 𝑟
62cv 1473 . . . . . 6 class 𝑖
76, 6cxp 5025 . . . . 5 class (𝑖 × 𝑖)
87cpw 4107 . . . 4 class 𝒫 (𝑖 × 𝑖)
9 vp . . . . 5 setvar 𝑝
103cv 1473 . . . . . 6 class 𝑠
11 cmps 19120 . . . . . 6 class mPwSer
126, 10, 11co 6526 . . . . 5 class (𝑖 mPwSer 𝑠)
139cv 1473 . . . . . 6 class 𝑝
14 cnx 15640 . . . . . . . 8 class ndx
15 cple 15723 . . . . . . . 8 class le
1614, 15cfv 5789 . . . . . . 7 class (le‘ndx)
17 vx . . . . . . . . . . . 12 setvar 𝑥
1817cv 1473 . . . . . . . . . . 11 class 𝑥
19 vy . . . . . . . . . . . 12 setvar 𝑦
2019cv 1473 . . . . . . . . . . 11 class 𝑦
2118, 20cpr 4126 . . . . . . . . . 10 class {𝑥, 𝑦}
22 cbs 15643 . . . . . . . . . . 11 class Base
2313, 22cfv 5789 . . . . . . . . . 10 class (Base‘𝑝)
2421, 23wss 3539 . . . . . . . . 9 wff {𝑥, 𝑦} ⊆ (Base‘𝑝)
25 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
2625cv 1473 . . . . . . . . . . . . . . 15 class 𝑧
2726, 18cfv 5789 . . . . . . . . . . . . . 14 class (𝑥𝑧)
2826, 20cfv 5789 . . . . . . . . . . . . . 14 class (𝑦𝑧)
29 cplt 16712 . . . . . . . . . . . . . . 15 class lt
3010, 29cfv 5789 . . . . . . . . . . . . . 14 class (lt‘𝑠)
3127, 28, 30wbr 4577 . . . . . . . . . . . . 13 wff (𝑥𝑧)(lt‘𝑠)(𝑦𝑧)
32 vw . . . . . . . . . . . . . . . . 17 setvar 𝑤
3332cv 1473 . . . . . . . . . . . . . . . 16 class 𝑤
345cv 1473 . . . . . . . . . . . . . . . . 17 class 𝑟
35 cltb 19123 . . . . . . . . . . . . . . . . 17 class <bag
3634, 6, 35co 6526 . . . . . . . . . . . . . . . 16 class (𝑟 <bag 𝑖)
3733, 26, 36wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑤(𝑟 <bag 𝑖)𝑧
3833, 18cfv 5789 . . . . . . . . . . . . . . . 16 class (𝑥𝑤)
3933, 20cfv 5789 . . . . . . . . . . . . . . . 16 class (𝑦𝑤)
4038, 39wceq 1474 . . . . . . . . . . . . . . 15 wff (𝑥𝑤) = (𝑦𝑤)
4137, 40wi 4 . . . . . . . . . . . . . 14 wff (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))
42 vd . . . . . . . . . . . . . . 15 setvar 𝑑
4342cv 1473 . . . . . . . . . . . . . 14 class 𝑑
4441, 32, 43wral 2895 . . . . . . . . . . . . 13 wff 𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))
4531, 44wa 382 . . . . . . . . . . . 12 wff ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
4645, 25, 43wrex 2896 . . . . . . . . . . 11 wff 𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
47 vh . . . . . . . . . . . . . . . 16 setvar
4847cv 1473 . . . . . . . . . . . . . . 15 class
4948ccnv 5026 . . . . . . . . . . . . . 14 class
50 cn 10869 . . . . . . . . . . . . . 14 class
5149, 50cima 5030 . . . . . . . . . . . . 13 class ( “ ℕ)
52 cfn 7818 . . . . . . . . . . . . 13 class Fin
5351, 52wcel 1976 . . . . . . . . . . . 12 wff ( “ ℕ) ∈ Fin
54 cn0 11141 . . . . . . . . . . . . 13 class 0
55 cmap 7721 . . . . . . . . . . . . 13 class 𝑚
5654, 6, 55co 6526 . . . . . . . . . . . 12 class (ℕ0𝑚 𝑖)
5753, 47, 56crab 2899 . . . . . . . . . . 11 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
5846, 42, 57wsbc 3401 . . . . . . . . . 10 wff [{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
5917, 19weq 1860 . . . . . . . . . 10 wff 𝑥 = 𝑦
6058, 59wo 381 . . . . . . . . 9 wff ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)
6124, 60wa 382 . . . . . . . 8 wff ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))
6261, 17, 19copab 4636 . . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
6316, 62cop 4130 . . . . . 6 class ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩
64 csts 15641 . . . . . 6 class sSet
6513, 63, 64co 6526 . . . . 5 class (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
669, 12, 65csb 3498 . . . 4 class (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
675, 8, 66cmpt 4637 . . 3 class (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
682, 3, 4, 4, 67cmpt2 6528 . 2 class (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
691, 68wceq 1474 1 wff ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmopsr  19242  opsrval  19243
  Copyright terms: Public domain W3C validator