Theorem oninfex2

Description: The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfex2	|- ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } e. _V )

Proof

Step	Hyp	Ref	Expression
1		onintunirab	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A = U. { x e. On | A. y e. A x C_ y } )
2		intex	|- ( A =/= (/) <-> |^| A e. _V )
3	2	biimpi	|- ( A =/= (/) -> |^| A e. _V )
4	3	adantl	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. _V )
5	1 4	eqeltrrd	|- ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } e. _V )