Metamath Proof Explorer


Definition df-opsr

Description: Define a total order on the set of all power series in s from the index set i given a wellordering r of i and a totally ordered base ring s . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion df-opsr ordPwSer=iV,sVr𝒫i×iimPwSers/ppsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y

Detailed syntax breakdown

Step Hyp Ref Expression
0 copws classordPwSer
1 vi setvari
2 cvv classV
3 vs setvars
4 vr setvarr
5 1 cv setvari
6 5 5 cxp classi×i
7 6 cpw class𝒫i×i
8 cmps classmPwSer
9 3 cv setvars
10 5 9 8 co classimPwSers
11 vp setvarp
12 11 cv setvarp
13 csts classsSet
14 cple classle
15 cnx classndx
16 15 14 cfv classndx
17 vx setvarx
18 vy setvary
19 17 cv setvarx
20 18 cv setvary
21 19 20 cpr classxy
22 cbs classBase
23 12 22 cfv classBasep
24 21 23 wss wffxyBasep
25 vh setvarh
26 cn0 class0
27 cmap class𝑚
28 26 5 27 co class0i
29 25 cv setvarh
30 29 ccnv classh-1
31 cn class
32 30 31 cima classh-1
33 cfn classFin
34 32 33 wcel wffh-1Fin
35 34 25 28 crab classh0i|h-1Fin
36 vd setvard
37 vz setvarz
38 36 cv setvard
39 37 cv setvarz
40 39 19 cfv classxz
41 cplt classlt
42 9 41 cfv class<s
43 39 20 cfv classyz
44 40 43 42 wbr wffxz<syz
45 vw setvarw
46 45 cv setvarw
47 4 cv setvarr
48 cltb class<bag
49 47 5 48 co classr<bagi
50 46 39 49 wbr wffwr<bagiz
51 46 19 cfv classxw
52 46 20 cfv classyw
53 51 52 wceq wffxw=yw
54 50 53 wi wffwr<bagizxw=yw
55 54 45 38 wral wffwdwr<bagizxw=yw
56 44 55 wa wffxz<syzwdwr<bagizxw=yw
57 56 37 38 wrex wffzdxz<syzwdwr<bagizxw=yw
58 57 36 35 wsbc wff[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=yw
59 19 20 wceq wffx=y
60 58 59 wo wff[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
61 24 60 wa wffxyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
62 61 17 18 copab classxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
63 16 62 cop classndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
64 12 63 13 co classpsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
65 11 10 64 csb classimPwSers/ppsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
66 4 7 65 cmpt classr𝒫i×iimPwSers/ppsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
67 1 3 2 2 66 cmpo classiV,sVr𝒫i×iimPwSers/ppsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y
68 0 67 wceq wffordPwSer=iV,sVr𝒫i×iimPwSers/ppsSetndxxy|xyBasep[˙h0i|h-1Fin/d]˙zdxz<syzwdwr<bagizxw=ywx=y