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 𝐵
Assertion	iunordi	⊢ Ord ∪ 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		iunordi.B	⊢ Ord 𝐵
2		iunord	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → Ord ∪ 𝑥 ∈ 𝐴 𝐵 )
3	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → Ord 𝐵 )
4	2 3	mprg	⊢ Ord ∪ 𝑥 ∈ 𝐴 𝐵