This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )