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 
|- _om = U. ( On i^i Fin )

Proof

Step Hyp Ref Expression
1 limom 
 |-  Lim _om
2 limuni 
 |-  ( Lim _om -> _om = U. _om )
3 1 2 ax-mp 
 |-  _om = U. _om
4 onfin2 
 |-  _om = ( On i^i Fin )
5 4 unieqi 
 |-  U. _om = U. ( On i^i Fin )
6 3 5 eqtri 
 |-  _om = U. ( On i^i Fin )