Metamath Proof Explorer


Theorem dfom6

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 ω = On Fin

Proof

Step Hyp Ref Expression
1 limom Lim ω
2 limuni Lim ω ω = ω
3 1 2 ax-mp ω = ω
4 onfin2 ω = On Fin
5 4 unieqi ω = On Fin
6 3 5 eqtri ω = On Fin