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 21685
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 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩)))
Distinct variable group:   β„Ž,𝑑,𝑖,𝑝,π‘Ÿ,𝑠,𝑀,π‘₯,𝑦,𝑧

Detailed syntax breakdown of Definition df-opsr
StepHypRef Expression
1 copws 21680 . 2 class ordPwSer
2 vi . . 3 setvar 𝑖
3 vs . . 3 setvar 𝑠
4 cvv 3472 . . 3 class V
5 vr . . . 4 setvar π‘Ÿ
62cv 1538 . . . . . 6 class 𝑖
76, 6cxp 5673 . . . . 5 class (𝑖 Γ— 𝑖)
87cpw 4601 . . . 4 class 𝒫 (𝑖 Γ— 𝑖)
9 vp . . . . 5 setvar 𝑝
103cv 1538 . . . . . 6 class 𝑠
11 cmps 21676 . . . . . 6 class mPwSer
126, 10, 11co 7411 . . . . 5 class (𝑖 mPwSer 𝑠)
139cv 1538 . . . . . 6 class 𝑝
14 cnx 17130 . . . . . . . 8 class ndx
15 cple 17208 . . . . . . . 8 class le
1614, 15cfv 6542 . . . . . . 7 class (leβ€˜ndx)
17 vx . . . . . . . . . . . 12 setvar π‘₯
1817cv 1538 . . . . . . . . . . 11 class π‘₯
19 vy . . . . . . . . . . . 12 setvar 𝑦
2019cv 1538 . . . . . . . . . . 11 class 𝑦
2118, 20cpr 4629 . . . . . . . . . 10 class {π‘₯, 𝑦}
22 cbs 17148 . . . . . . . . . . 11 class Base
2313, 22cfv 6542 . . . . . . . . . 10 class (Baseβ€˜π‘)
2421, 23wss 3947 . . . . . . . . 9 wff {π‘₯, 𝑦} βŠ† (Baseβ€˜π‘)
25 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
2625cv 1538 . . . . . . . . . . . . . . 15 class 𝑧
2726, 18cfv 6542 . . . . . . . . . . . . . 14 class (π‘₯β€˜π‘§)
2826, 20cfv 6542 . . . . . . . . . . . . . 14 class (π‘¦β€˜π‘§)
29 cplt 18265 . . . . . . . . . . . . . . 15 class lt
3010, 29cfv 6542 . . . . . . . . . . . . . 14 class (ltβ€˜π‘ )
3127, 28, 30wbr 5147 . . . . . . . . . . . . 13 wff (π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§)
32 vw . . . . . . . . . . . . . . . . 17 setvar 𝑀
3332cv 1538 . . . . . . . . . . . . . . . 16 class 𝑀
345cv 1538 . . . . . . . . . . . . . . . . 17 class π‘Ÿ
35 cltb 21679 . . . . . . . . . . . . . . . . 17 class <bag
3634, 6, 35co 7411 . . . . . . . . . . . . . . . 16 class (π‘Ÿ <bag 𝑖)
3733, 26, 36wbr 5147 . . . . . . . . . . . . . . 15 wff 𝑀(π‘Ÿ <bag 𝑖)𝑧
3833, 18cfv 6542 . . . . . . . . . . . . . . . 16 class (π‘₯β€˜π‘€)
3933, 20cfv 6542 . . . . . . . . . . . . . . . 16 class (π‘¦β€˜π‘€)
4038, 39wceq 1539 . . . . . . . . . . . . . . 15 wff (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)
4137, 40wi 4 . . . . . . . . . . . . . 14 wff (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))
42 vd . . . . . . . . . . . . . . 15 setvar 𝑑
4342cv 1538 . . . . . . . . . . . . . 14 class 𝑑
4441, 32, 43wral 3059 . . . . . . . . . . . . 13 wff βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))
4531, 44wa 394 . . . . . . . . . . . 12 wff ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))
4645, 25, 43wrex 3068 . . . . . . . . . . 11 wff βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))
47 vh . . . . . . . . . . . . . . . 16 setvar β„Ž
4847cv 1538 . . . . . . . . . . . . . . 15 class β„Ž
4948ccnv 5674 . . . . . . . . . . . . . 14 class β—‘β„Ž
50 cn 12216 . . . . . . . . . . . . . 14 class β„•
5149, 50cima 5678 . . . . . . . . . . . . 13 class (β—‘β„Ž β€œ β„•)
52 cfn 8941 . . . . . . . . . . . . 13 class Fin
5351, 52wcel 2104 . . . . . . . . . . . 12 wff (β—‘β„Ž β€œ β„•) ∈ Fin
54 cn0 12476 . . . . . . . . . . . . 13 class β„•0
55 cmap 8822 . . . . . . . . . . . . 13 class ↑m
5654, 6, 55co 7411 . . . . . . . . . . . 12 class (β„•0 ↑m 𝑖)
5753, 47, 56crab 3430 . . . . . . . . . . 11 class {β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin}
5846, 42, 57wsbc 3776 . . . . . . . . . 10 wff [{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))
5917, 19weq 1964 . . . . . . . . . 10 wff π‘₯ = 𝑦
6058, 59wo 843 . . . . . . . . 9 wff ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦)
6124, 60wa 394 . . . . . . . 8 wff ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))
6261, 17, 19copab 5209 . . . . . . 7 class {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}
6316, 62cop 4633 . . . . . 6 class ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩
64 csts 17100 . . . . . 6 class sSet
6513, 63, 64co 7411 . . . . 5 class (𝑝 sSet ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩)
669, 12, 65csb 3892 . . . 4 class ⦋(𝑖 mPwSer 𝑠) / π‘β¦Œ(𝑝 sSet ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩)
675, 8, 66cmpt 5230 . . 3 class (π‘Ÿ ∈ 𝒫 (𝑖 Γ— 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / π‘β¦Œ(𝑝 sSet ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩))
682, 3, 4, 4, 67cmpo 7413 . 2 class (𝑖 ∈ V, 𝑠 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (𝑖 Γ— 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / π‘β¦Œ(𝑝 sSet ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩)))
691, 68wceq 1539 1 wff ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (𝑖 Γ— 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / π‘β¦Œ(𝑝 sSet ⟨(leβ€˜ndx), {⟨π‘₯, π‘¦βŸ© ∣ ({π‘₯, 𝑦} βŠ† (Baseβ€˜π‘) ∧ ([{β„Ž ∈ (β„•0 ↑m 𝑖) ∣ (β—‘β„Ž β€œ β„•) ∈ Fin} / 𝑑]βˆƒπ‘§ ∈ 𝑑 ((π‘₯β€˜π‘§)(ltβ€˜π‘ )(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝑑 (𝑀(π‘Ÿ <bag 𝑖)𝑧 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∨ π‘₯ = 𝑦))}⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmopsr  21819  opsrval  21820
  Copyright terms: Public domain W3C validator