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 )