This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem om0r

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( (/) .o x ) = ( (/) .o (/) ) )
2 1 eqeq1d 
 |-  ( x = (/) -> ( ( (/) .o x ) = (/) <-> ( (/) .o (/) ) = (/) ) )
3 oveq2 
 |-  ( x = y -> ( (/) .o x ) = ( (/) .o y ) )
4 3 eqeq1d 
 |-  ( x = y -> ( ( (/) .o x ) = (/) <-> ( (/) .o y ) = (/) ) )
5 oveq2 
 |-  ( x = suc y -> ( (/) .o x ) = ( (/) .o suc y ) )
6 5 eqeq1d 
 |-  ( x = suc y -> ( ( (/) .o x ) = (/) <-> ( (/) .o suc y ) = (/) ) )
7 oveq2 
 |-  ( x = A -> ( (/) .o x ) = ( (/) .o A ) )
8 7 eqeq1d 
 |-  ( x = A -> ( ( (/) .o x ) = (/) <-> ( (/) .o A ) = (/) ) )
9 0elon 
 |-  (/) e. On
10 om0 
 |-  ( (/) e. On -> ( (/) .o (/) ) = (/) )
11 9 10 ax-mp 
 |-  ( (/) .o (/) ) = (/)
12 oveq1 
 |-  ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) )
13 omsuc 
 |-  ( ( (/) e. On /\ y e. On ) -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
14 9 13 mpan 
 |-  ( y e. On -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
15 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
16 9 15 ax-mp 
 |-  ( (/) +o (/) ) = (/)
17 16 eqcomi 
 |-  (/) = ( (/) +o (/) )
18 17 a1i 
 |-  ( y e. On -> (/) = ( (/) +o (/) ) )
19 14 18 eqeq12d 
 |-  ( y e. On -> ( ( (/) .o suc y ) = (/) <-> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) ) )
20 12 19 imbitrrid 
 |-  ( y e. On -> ( ( (/) .o y ) = (/) -> ( (/) .o suc y ) = (/) ) )
21 iuneq2 
 |-  ( A. y e. x ( (/) .o y ) = (/) -> U_ y e. x ( (/) .o y ) = U_ y e. x (/) )
22 iun0 
 |-  U_ y e. x (/) = (/)
23 21 22 eqtrdi 
 |-  ( A. y e. x ( (/) .o y ) = (/) -> U_ y e. x ( (/) .o y ) = (/) )
24 vex 
 |-  x e. _V
25 omlim 
 |-  ( ( (/) e. On /\ ( x e. _V /\ Lim x ) ) -> ( (/) .o x ) = U_ y e. x ( (/) .o y ) )
26 9 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 27 eqeq1d 
 |-  ( Lim x -> ( ( (/) .o x ) = (/) <-> U_ y e. x ( (/) .o y ) = (/) ) )
29 23 28 imbitrrid 
 |-  ( Lim x -> ( A. y e. x ( (/) .o y ) = (/) -> ( (/) .o x ) = (/) ) )
30 2 4 6 8 11 20 29 tfinds 
 |-  ( A e. On -> ( (/) .o A ) = (/) )