Theorem iunord

Description: The indexed union of a collection of ordinal numbers B ( x ) is ordinal. This proof is based on the proof of ssorduni , but does not use it directly, since ssorduni does not work when B is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019)

	Ref	Expression
Assertion	iunord	|- ( A. x e. A Ord B -> Ord U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		ordtr	|- ( Ord B -> Tr B )
2	1	ralimi	|- ( A. x e. A Ord B -> A. x e. A Tr B )
3		triun	|- ( A. x e. A Tr B -> Tr U_ x e. A B )
4	2 3	syl	|- ( A. x e. A Ord B -> Tr U_ x e. A B )
5		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
6		nfra1	|- F/ x A. x e. A Ord B
7		nfv	|- F/ x y e. On
8		rsp	|- ( A. x e. A Ord B -> ( x e. A -> Ord B ) )
9		ordelon	|- ( ( Ord B /\ y e. B ) -> y e. On )
10	9	ex	|- ( Ord B -> ( y e. B -> y e. On ) )
11	8 10	syl6	|- ( A. x e. A Ord B -> ( x e. A -> ( y e. B -> y e. On ) ) )
12	6 7 11	rexlimd	|- ( A. x e. A Ord B -> ( E. x e. A y e. B -> y e. On ) )
13	5 12	biimtrid	|- ( A. x e. A Ord B -> ( y e. U_ x e. A B -> y e. On ) )
14	13	ssrdv	|- ( A. x e. A Ord B -> U_ x e. A B C_ On )
15		ordon	|- Ord On
16		trssord	|- ( ( Tr U_ x e. A B /\ U_ x e. A B C_ On /\ Ord On ) -> Ord U_ x e. A B )
17	16	3exp	|- ( Tr U_ x e. A B -> ( U_ x e. A B C_ On -> ( Ord On -> Ord U_ x e. A B ) ) )
18	15 17	mpii	|- ( Tr U_ x e. A B -> ( U_ x e. A B C_ On -> Ord U_ x e. A B ) )
19	4 14 18	sylc	|- ( A. x e. A Ord B -> Ord U_ x e. A B )