Metamath Proof Explorer

Theorem nnuni

Description: The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Assertion nnuni 
|- ( A e. _om -> U. A e. _om )

Proof

Step Hyp Ref Expression
1 nn0suc 
 |-  ( A e. _om -> ( A = (/) \/ E. x e. _om A = suc x ) )
2 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
3 uni0 
 |-  U. (/) = (/)
4 2 3 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
5 peano1 
 |-  (/) e. _om
6 4 5 eqeltrdi 
 |-  ( A = (/) -> U. A e. _om )
7 nnord 
 |-  ( x e. _om -> Ord x )
8 ordunisuc 
 |-  ( Ord x -> U. suc x = x )
9 7 8 syl 
 |-  ( x e. _om -> U. suc x = x )
10 id 
 |-  ( x e. _om -> x e. _om )
11 9 10 eqeltrd 
 |-  ( x e. _om -> U. suc x e. _om )
12 unieq 
 |-  ( A = suc x -> U. A = U. suc x )
13 12 eleq1d 
 |-  ( A = suc x -> ( U. A e. _om <-> U. suc x e. _om ) )
14 11 13 syl5ibrcom 
 |-  ( x e. _om -> ( A = suc x -> U. A e. _om ) )
15 14 rexlimiv 
 |-  ( E. x e. _om A = suc x -> U. A e. _om )
16 6 15 jaoi 
 |-  ( ( A = (/) \/ E. x e. _om A = suc x ) -> U. A e. _om )
17 1 16 syl 
 |-  ( A e. _om -> U. A e. _om )