Metamath Proof Explorer


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 syl5bi
 |-  ( 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 )