Theorem onuniintrab2

Description: The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	onuniintrab2	|- ( A e. ~P On -> U. A = |^| { x e. On | A. y e. A y C_ x } )

Proof

Step	Hyp	Ref	Expression
1		elpwb	|- ( A e. ~P On <-> ( A e. _V /\ A C_ On ) )
2		onuniintrab	|- ( ( A C_ On /\ A e. _V ) -> U. A = |^| { x e. On | A. y e. A y C_ x } )
3	2	ancoms	|- ( ( A e. _V /\ A C_ On ) -> U. A = |^| { x e. On | A. y e. A y C_ x } )
4	1 3	sylbi	|- ( A e. ~P On -> U. A = |^| { x e. On | A. y e. A y C_ x } )