Metamath Proof Explorer


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 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 -> U. A = |^| { x e. On | A. y e. A y C_ x } )