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 )