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 } ) |
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 } ) |