Description: Define the canonical order isomorphism from the well-order R on A to an ordinal. (Contributed by Mario Carneiro, 23-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-oi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cR | |
|
1 | cA | |
|
2 | 1 0 | coi | |
3 | 1 0 | wwe | |
4 | 1 0 | wse | |
5 | 3 4 | wa | |
6 | vh | |
|
7 | cvv | |
|
8 | vv | |
|
9 | vw | |
|
10 | vj | |
|
11 | 6 | cv | |
12 | 11 | crn | |
13 | 10 | cv | |
14 | 9 | cv | |
15 | 13 14 0 | wbr | |
16 | 15 10 12 | wral | |
17 | 16 9 1 | crab | |
18 | vu | |
|
19 | 18 | cv | |
20 | 8 | cv | |
21 | 19 20 0 | wbr | |
22 | 21 | wn | |
23 | 22 18 17 | wral | |
24 | 23 8 17 | crio | |
25 | 6 7 24 | cmpt | |
26 | 25 | crecs | |
27 | vx | |
|
28 | con0 | |
|
29 | vt | |
|
30 | vz | |
|
31 | 27 | cv | |
32 | 26 31 | cima | |
33 | 30 | cv | |
34 | 29 | cv | |
35 | 33 34 0 | wbr | |
36 | 35 30 32 | wral | |
37 | 36 29 1 | wrex | |
38 | 37 27 28 | crab | |
39 | 26 38 | cres | |
40 | c0 | |
|
41 | 5 39 40 | cif | |
42 | 2 41 | wceq | |