Theorem oninfunirab

Description: The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfunirab	|- ( ( A C_ On /\ A =/= (/) ) -> inf ( A , On , _E ) = U. { x e. On | A. y e. A x C_ y } )

Proof

Step	Hyp	Ref	Expression
1		oninfint	|- ( ( A C_ On /\ A =/= (/) ) -> inf ( A , On , _E ) = |^| A )
2		onintunirab	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A = U. { x e. On | A. y e. A x C_ y } )
3	1 2	eqtrd	|- ( ( A C_ On /\ A =/= (/) ) -> inf ( A , On , _E ) = U. { x e. On | A. y e. A x C_ y } )