Theorem uniordint

Description: The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of BellMachover p. 471. (Contributed by NM, 20-Sep-2003)

	Ref	Expression
Hypothesis	uniordint.1	|- A e. _V
Assertion	uniordint	|- ( A C_ On -> U. A = |^| { x e. On | A. y e. A y C_ x } )

Proof

Step	Hyp	Ref	Expression
1		uniordint.1	|- A e. _V
2	1	ssonunii	|- ( A C_ On -> U. A e. On )
3		unissb	|- ( U. A C_ x <-> A. y e. A y C_ x )
4	3	rabbii	|- { x e. On | U. A C_ x } = { x e. On | A. y e. A y C_ x }
5	4	inteqi	|- |^| { x e. On | U. A C_ x } = |^| { x e. On | A. y e. A y C_ x }
6		intmin	|- ( U. A e. On -> |^| { x e. On | U. A C_ x } = U. A )
7	5 6	syl5reqr	|- ( U. A e. On -> U. A = |^| { x e. On | A. y e. A y C_ x } )
8	2 7	syl	|- ( A C_ On -> U. A = |^| { x e. On | A. y e. A y C_ x } )