Theorem iunon

Description: The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 5-Dec-2016)

	Ref	Expression
Assertion	iunon	|- ( ( A e. V /\ A. x e. A B e. On ) -> U_ x e. A B e. On )

Proof

Step	Hyp	Ref	Expression
1		dfiun3g	|- ( A. x e. A B e. On -> U_ x e. A B = U. ran ( x e. A |-> B ) )
2	1	adantl	|- ( ( A e. V /\ A. x e. A B e. On ) -> U_ x e. A B = U. ran ( x e. A |-> B ) )
3		mptexg	|- ( A e. V -> ( x e. A |-> B ) e. _V )
4		rnexg	|- ( ( x e. A |-> B ) e. _V -> ran ( x e. A |-> B ) e. _V )
5	3 4	syl	|- ( A e. V -> ran ( x e. A |-> B ) e. _V )
6		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
7	6	rnmptss	|- ( A. x e. A B e. On -> ran ( x e. A |-> B ) C_ On )
8		ssonuni	|- ( ran ( x e. A |-> B ) e. _V -> ( ran ( x e. A |-> B ) C_ On -> U. ran ( x e. A |-> B ) e. On ) )
9	8	imp	|- ( ( ran ( x e. A |-> B ) e. _V /\ ran ( x e. A |-> B ) C_ On ) -> U. ran ( x e. A |-> B ) e. On )
10	5 7 9	syl2an	|- ( ( A e. V /\ A. x e. A B e. On ) -> U. ran ( x e. A |-> B ) e. On )
11	2 10	eqeltrd	|- ( ( A e. V /\ A. x e. A B e. On ) -> U_ x e. A B e. On )