Theorem onuniintrab

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

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

Proof

Step	Hyp	Ref	Expression
1		ssonuni	|- ( A e. V -> ( A C_ On -> U. A e. On ) )
2	1	impcom	|- ( ( A C_ On /\ A e. V ) -> U. A e. On )
3		intmin	|- ( U. A e. On -> |^| { x e. On | U. A C_ x } = U. A )
4		unissb	|- ( U. A C_ x <-> A. y e. A y C_ x )
5	4	rabbii	|- { x e. On | U. A C_ x } = { x e. On | A. y e. A y C_ x }
6	5	inteqi	|- |^| { x e. On | U. A C_ x } = |^| { x e. On | A. y e. A y C_ x }
7	3 6	eqtr3di	|- ( U. A e. On -> U. A = |^| { x e. On | A. y e. A y C_ x } )
8	2 7	syl	|- ( ( A C_ On /\ A e. V ) -> U. A = |^| { x e. On | A. y e. A y C_ x } )