Metamath Proof Explorer


Definition df-oi

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 OrdIsoRA=ifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR classR
1 cA classA
2 1 0 coi classOrdIsoRA
3 1 0 wwe wffRWeA
4 1 0 wse wffRSeA
5 3 4 wa wffRWeARSeA
6 vh setvarh
7 cvv classV
8 vv setvarv
9 vw setvarw
10 vj setvarj
11 6 cv setvarh
12 11 crn classranh
13 10 cv setvarj
14 9 cv setvarw
15 13 14 0 wbr wffjRw
16 15 10 12 wral wffjranhjRw
17 16 9 1 crab classwA|jranhjRw
18 vu setvaru
19 18 cv setvaru
20 8 cv setvarv
21 19 20 0 wbr wffuRv
22 21 wn wff¬uRv
23 22 18 17 wral wffuwA|jranhjRw¬uRv
24 23 8 17 crio classιvwA|jranhjRw|uwA|jranhjRw¬uRv
25 6 7 24 cmpt classhVιvwA|jranhjRw|uwA|jranhjRw¬uRv
26 25 crecs classrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRv
27 vx setvarx
28 con0 classOn
29 vt setvart
30 vz setvarz
31 27 cv setvarx
32 26 31 cima classrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvx
33 30 cv setvarz
34 29 cv setvart
35 33 34 0 wbr wffzRt
36 35 30 32 wral wffzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
37 36 29 1 wrex wfftAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
38 37 27 28 crab classxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
39 26 38 cres classrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
40 c0 class
41 5 39 40 cif classifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
42 2 41 wceq wffOrdIsoRA=ifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt