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

Definition df-opsr 20675
 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‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
Distinct variable group:   ,𝑑,𝑖,𝑝,𝑟,𝑠,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-opsr
StepHypRef Expression
1 copws 20670 . 2 class ordPwSer
2 vi . . 3 setvar 𝑖
3 vs . . 3 setvar 𝑠
4 cvv 3409 . . 3 class V
5 vr . . . 4 setvar 𝑟
62cv 1537 . . . . . 6 class 𝑖
76, 6cxp 5522 . . . . 5 class (𝑖 × 𝑖)
87cpw 4494 . . . 4 class 𝒫 (𝑖 × 𝑖)
9 vp . . . . 5 setvar 𝑝
103cv 1537 . . . . . 6 class 𝑠
11 cmps 20666 . . . . . 6 class mPwSer
126, 10, 11co 7150 . . . . 5 class (𝑖 mPwSer 𝑠)
139cv 1537 . . . . . 6 class 𝑝
14 cnx 16538 . . . . . . . 8 class ndx
15 cple 16630 . . . . . . . 8 class le
1614, 15cfv 6335 . . . . . . 7 class (le‘ndx)
17 vx . . . . . . . . . . . 12 setvar 𝑥
1817cv 1537 . . . . . . . . . . 11 class 𝑥
19 vy . . . . . . . . . . . 12 setvar 𝑦
2019cv 1537 . . . . . . . . . . 11 class 𝑦
2118, 20cpr 4524 . . . . . . . . . 10 class {𝑥, 𝑦}
22 cbs 16541 . . . . . . . . . . 11 class Base
2313, 22cfv 6335 . . . . . . . . . 10 class (Base‘𝑝)
2421, 23wss 3858 . . . . . . . . 9 wff {𝑥, 𝑦} ⊆ (Base‘𝑝)
25 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
2625cv 1537 . . . . . . . . . . . . . . 15 class 𝑧
2726, 18cfv 6335 . . . . . . . . . . . . . 14 class (𝑥𝑧)
2826, 20cfv 6335 . . . . . . . . . . . . . 14 class (𝑦𝑧)
29 cplt 17617 . . . . . . . . . . . . . . 15 class lt
3010, 29cfv 6335 . . . . . . . . . . . . . 14 class (lt‘𝑠)
3127, 28, 30wbr 5032 . . . . . . . . . . . . 13 wff (𝑥𝑧)(lt‘𝑠)(𝑦𝑧)
32 vw . . . . . . . . . . . . . . . . 17 setvar 𝑤
3332cv 1537 . . . . . . . . . . . . . . . 16 class 𝑤
345cv 1537 . . . . . . . . . . . . . . . . 17 class 𝑟
35 cltb 20669 . . . . . . . . . . . . . . . . 17 class <bag
3634, 6, 35co 7150 . . . . . . . . . . . . . . . 16 class (𝑟 <bag 𝑖)
3733, 26, 36wbr 5032 . . . . . . . . . . . . . . 15 wff 𝑤(𝑟 <bag 𝑖)𝑧
3833, 18cfv 6335 . . . . . . . . . . . . . . . 16 class (𝑥𝑤)
3933, 20cfv 6335 . . . . . . . . . . . . . . . 16 class (𝑦𝑤)
4038, 39wceq 1538 . . . . . . . . . . . . . . 15 wff (𝑥𝑤) = (𝑦𝑤)
4137, 40wi 4 . . . . . . . . . . . . . 14 wff (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))
42 vd . . . . . . . . . . . . . . 15 setvar 𝑑
4342cv 1537 . . . . . . . . . . . . . 14 class 𝑑
4441, 32, 43wral 3070 . . . . . . . . . . . . 13 wff 𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))
4531, 44wa 399 . . . . . . . . . . . 12 wff ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
4645, 25, 43wrex 3071 . . . . . . . . . . 11 wff 𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
47 vh . . . . . . . . . . . . . . . 16 setvar
4847cv 1537 . . . . . . . . . . . . . . 15 class
4948ccnv 5523 . . . . . . . . . . . . . 14 class
50 cn 11674 . . . . . . . . . . . . . 14 class
5149, 50cima 5527 . . . . . . . . . . . . 13 class ( “ ℕ)
52 cfn 8527 . . . . . . . . . . . . 13 class Fin
5351, 52wcel 2111 . . . . . . . . . . . 12 wff ( “ ℕ) ∈ Fin
54 cn0 11934 . . . . . . . . . . . . 13 class 0
55 cmap 8416 . . . . . . . . . . . . 13 class m
5654, 6, 55co 7150 . . . . . . . . . . . 12 class (ℕ0m 𝑖)
5753, 47, 56crab 3074 . . . . . . . . . . 11 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
5846, 42, 57wsbc 3696 . . . . . . . . . 10 wff [{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)))
5917, 19weq 1964 . . . . . . . . . 10 wff 𝑥 = 𝑦
6058, 59wo 844 . . . . . . . . 9 wff ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)
6124, 60wa 399 . . . . . . . 8 wff ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))
6261, 17, 19copab 5094 . . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
6316, 62cop 4528 . . . . . 6 class ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩
64 csts 16539 . . . . . 6 class sSet
6513, 63, 64co 7150 . . . . 5 class (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
669, 12, 65csb 3805 . . . 4 class (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
675, 8, 66cmpt 5112 . . 3 class (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
682, 3, 4, 4, 67cmpo 7152 . 2 class (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
691, 68wceq 1538 1 wff ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
 Colors of variables: wff setvar class This definition is referenced by:  reldmopsr  20805  opsrval  20806
 Copyright terms: Public domain W3C validator