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	$$⊢\mathrm{Ord}B$$
Assertion	iunordi	$$⊢\mathrm{Ord}\bigcup _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		iunordi.B	$$⊢\mathrm{Ord}B$$
2		iunord	$$⊢\forall x\in A\mathrm{Ord}B\to \mathrm{Ord}\bigcup _{x\in A}B$$
3	1	a1i	$$⊢x\in A\to \mathrm{Ord}B$$
4	2 3	mprg	$$⊢\mathrm{Ord}\bigcup _{x\in A}B$$