Metamath Proof Explorer

Theorem nnunifi

Description: The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Assertion nnunifi 
|- ( ( S C_ _om /\ S e. Fin ) -> U. S e. _om )

Proof

Step Hyp Ref Expression
1 unieq 
 |-  ( S = (/) -> U. S = U. (/) )
2 uni0 
 |-  U. (/) = (/)
3 peano1 
 |-  (/) e. _om
4 2 3 eqeltri 
 |-  U. (/) e. _om
5 1 4 eqeltrdi 
 |-  ( S = (/) -> U. S e. _om )
6 5 adantl 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S = (/) ) -> U. S e. _om )
7 simpll 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> S C_ _om )
8 omsson 
 |-  _om C_ On
9 7 8 sstrdi 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> S C_ On )
10 simplr 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> S e. Fin )
11 simpr 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> S =/= (/) )
12 ordunifi 
 |-  ( ( S C_ On /\ S e. Fin /\ S =/= (/) ) -> U. S e. S )
13 9 10 11 12 syl3anc 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> U. S e. S )
14 7 13 sseldd 
 |-  ( ( ( S C_ _om /\ S e. Fin ) /\ S =/= (/) ) -> U. S e. _om )
15 6 14 pm2.61dane 
 |-  ( ( S C_ _om /\ S e. Fin ) -> U. S e. _om )