Metamath Proof Explorer

Theorem om1r

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion om1r 
|- ( A e. On -> ( 1o .o A ) = A )

Proof

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