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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | copws | |
|
1 | vi | |
|
2 | cvv | |
|
3 | vs | |
|
4 | vr | |
|
5 | 1 | cv | |
6 | 5 5 | cxp | |
7 | 6 | cpw | |
8 | cmps | |
|
9 | 3 | cv | |
10 | 5 9 8 | co | |
11 | vp | |
|
12 | 11 | cv | |
13 | csts | |
|
14 | cple | |
|
15 | cnx | |
|
16 | 15 14 | cfv | |
17 | vx | |
|
18 | vy | |
|
19 | 17 | cv | |
20 | 18 | cv | |
21 | 19 20 | cpr | |
22 | cbs | |
|
23 | 12 22 | cfv | |
24 | 21 23 | wss | |
25 | vh | |
|
26 | cn0 | |
|
27 | cmap | |
|
28 | 26 5 27 | co | |
29 | 25 | cv | |
30 | 29 | ccnv | |
31 | cn | |
|
32 | 30 31 | cima | |
33 | cfn | |
|
34 | 32 33 | wcel | |
35 | 34 25 28 | crab | |
36 | vd | |
|
37 | vz | |
|
38 | 36 | cv | |
39 | 37 | cv | |
40 | 39 19 | cfv | |
41 | cplt | |
|
42 | 9 41 | cfv | |
43 | 39 20 | cfv | |
44 | 40 43 42 | wbr | |
45 | vw | |
|
46 | 45 | cv | |
47 | 4 | cv | |
48 | cltb | |
|
49 | 47 5 48 | co | |
50 | 46 39 49 | wbr | |
51 | 46 19 | cfv | |
52 | 46 20 | cfv | |
53 | 51 52 | wceq | |
54 | 50 53 | wi | |
55 | 54 45 38 | wral | |
56 | 44 55 | wa | |
57 | 56 37 38 | wrex | |
58 | 57 36 35 | wsbc | |
59 | 19 20 | wceq | |
60 | 58 59 | wo | |
61 | 24 60 | wa | |
62 | 61 17 18 | copab | |
63 | 16 62 | cop | |
64 | 12 63 13 | co | |
65 | 11 10 64 | csb | |
66 | 4 7 65 | cmpt | |
67 | 1 3 2 2 66 | cmpo | |
68 | 0 67 | wceq | |