Description: Let _om be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | dfom6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limom | ||
2 | limuni | ||
3 | 1 2 | ax-mp | |
4 | onfin2 | ||
5 | 4 | unieqi | |
6 | 3 5 | eqtri |