Metamath Proof Explorer

Theorem iunordi

Description: The indexed union of a collection of ordinal numbers B ( x ) is ordinal. (Contributed by Emmett Weisz, 3-Nov-2019)

Ref Expression
Hypothesis iunordi.B 
|- Ord B
Assertion iunordi 
|- Ord U_ x e. A B

Proof

Step Hyp Ref Expression
1 iunordi.B 
 |-  Ord B
2 iunord 
 |-  ( A. x e. A Ord B -> Ord U_ x e. A B )
3 1 a1i 
 |-  ( x e. A -> Ord B )
4 2 3 mprg 
 |-  Ord U_ x e. A B