Description: Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | df3o2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3o | |
|
2 | df2o3 | |
|
3 | 2 | uneq1i | |
4 | df-suc | |
|
5 | df-tp | |
|
6 | 3 4 5 | 3eqtr4i | |
7 | 1 6 | eqtri | |