Metamath Proof Explorer

Theorem oa0r

Description: Ordinal addition with zero. Proposition 8.3 of TakeutiZaring p. 57. (Contributed by NM, 5-May-1995)

Ref Expression
Assertion oa0r 
|- ( A e. On -> ( (/) +o A ) = A )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( (/) +o x ) = ( (/) +o (/) ) )
2 id 
 |-  ( x = (/) -> x = (/) )
3 1 2 eqeq12d 
 |-  ( x = (/) -> ( ( (/) +o x ) = x <-> ( (/) +o (/) ) = (/) ) )
4 oveq2 
 |-  ( x = y -> ( (/) +o x ) = ( (/) +o y ) )
5 id 
 |-  ( x = y -> x = y )
6 4 5 eqeq12d 
 |-  ( x = y -> ( ( (/) +o x ) = x <-> ( (/) +o y ) = y ) )
7 oveq2 
 |-  ( x = suc y -> ( (/) +o x ) = ( (/) +o suc y ) )
8 id 
 |-  ( x = suc y -> x = suc y )
9 7 8 eqeq12d 
 |-  ( x = suc y -> ( ( (/) +o x ) = x <-> ( (/) +o suc y ) = suc y ) )
10 oveq2 
 |-  ( x = A -> ( (/) +o x ) = ( (/) +o A ) )
11 id 
 |-  ( x = A -> x = A )
12 10 11 eqeq12d 
 |-  ( x = A -> ( ( (/) +o x ) = x <-> ( (/) +o A ) = A ) )
13 0elon 
 |-  (/) e. On
14 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
15 13 14 ax-mp 
 |-  ( (/) +o (/) ) = (/)
16 oasuc 
 |-  ( ( (/) e. On /\ y e. On ) -> ( (/) +o suc y ) = suc ( (/) +o y ) )
17 13 16 mpan 
 |-  ( y e. On -> ( (/) +o suc y ) = suc ( (/) +o y ) )
18 suceq 
 |-  ( ( (/) +o y ) = y -> suc ( (/) +o y ) = suc y )
19 17 18 sylan9eq 
 |-  ( ( y e. On /\ ( (/) +o y ) = y ) -> ( (/) +o suc y ) = suc y )
20 19 ex 
 |-  ( y e. On -> ( ( (/) +o y ) = y -> ( (/) +o suc y ) = suc y ) )
21 iuneq2 
 |-  ( A. y e. x ( (/) +o y ) = y -> U_ y e. x ( (/) +o y ) = U_ y e. x y )
22 uniiun 
 |-  U. x = U_ y e. x y
23 21 22 eqtr4di 
 |-  ( A. y e. x ( (/) +o y ) = y -> U_ y e. x ( (/) +o y ) = U. x )
24 vex 
 |-  x e. _V
25 oalim 
 |-  ( ( (/) e. On /\ ( x e. _V /\ Lim x ) ) -> ( (/) +o x ) = U_ y e. x ( (/) +o y ) )
26 13 25 mpan 
 |-  ( ( x e. _V /\ Lim x ) -> ( (/) +o x ) = U_ y e. x ( (/) +o y ) )
27 24 26 mpan 
 |-  ( Lim x -> ( (/) +o x ) = U_ y e. x ( (/) +o y ) )
28 limuni 
 |-  ( Lim x -> x = U. x )
29 27 28 eqeq12d 
 |-  ( Lim x -> ( ( (/) +o x ) = x <-> U_ y e. x ( (/) +o y ) = U. x ) )
30 23 29 syl5ibr 
 |-  ( Lim x -> ( A. y e. x ( (/) +o y ) = y -> ( (/) +o x ) = x ) )
31 3 6 9 12 15 20 30 tfinds 
 |-  ( A e. On -> ( (/) +o A ) = A )