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 V
Assertion uniordint A On A = x On | y A y x

Proof

Step Hyp Ref Expression
1 uniordint.1 A V
2 1 ssonunii A On A On
3 intmin A On x On | A x = A
4 unissb A x y A y x
5 4 rabbii x On | A x = x On | y A y x
6 5 inteqi x On | A x = x On | y A y x
7 3 6 eqtr3di A On A = x On | y A y x
8 2 7 syl A On A = x On | y A y x