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

Metamath Proof Explorer

Theorem omcl

Description: Closure law for ordinal multiplication. Proposition 8.16 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 3-Aug-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion omcl 
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ( A .o x ) e. On <-> ( A .o (/) ) e. On ) )
3 oveq2 
 |-  ( x = y -> ( A .o x ) = ( A .o y ) )
4 3 eleq1d 
 |-  ( x = y -> ( ( A .o x ) e. On <-> ( A .o y ) e. On ) )
5 oveq2 
 |-  ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
6 5 eleq1d 
 |-  ( x = suc y -> ( ( A .o x ) e. On <-> ( A .o suc y ) e. On ) )
7 oveq2 
 |-  ( x = B -> ( A .o x ) = ( A .o B ) )
8 7 eleq1d 
 |-  ( x = B -> ( ( A .o x ) e. On <-> ( A .o B ) e. On ) )
9 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
10 0elon 
 |-  (/) e. On
11 9 10 eqeltrdi 
 |-  ( A e. On -> ( A .o (/) ) e. On )
12 oacl 
 |-  ( ( ( A .o y ) e. On /\ A e. On ) -> ( ( A .o y ) +o A ) e. On )
13 12 expcom 
 |-  ( A e. On -> ( ( A .o y ) e. On -> ( ( A .o y ) +o A ) e. On ) )
14 13 adantr 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A .o y ) e. On -> ( ( A .o y ) +o A ) e. On ) )
15 omsuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
16 15 eleq1d 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A .o suc y ) e. On <-> ( ( A .o y ) +o A ) e. On ) )
17 14 16 sylibrd 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A .o y ) e. On -> ( A .o suc y ) e. On ) )
18 17 expcom 
 |-  ( y e. On -> ( A e. On -> ( ( A .o y ) e. On -> ( A .o suc y ) e. On ) ) )
19 vex 
 |-  x e. _V
20 iunon 
 |-  ( ( x e. _V /\ A. y e. x ( A .o y ) e. On ) -> U_ y e. x ( A .o y ) e. On )
21 19 20 mpan 
 |-  ( A. y e. x ( A .o y ) e. On -> U_ y e. x ( A .o y ) e. On )
22 omlim 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A .o x ) = U_ y e. x ( A .o y ) )
23 19 22 mpanr1 
 |-  ( ( A e. On /\ Lim x ) -> ( A .o x ) = U_ y e. x ( A .o y ) )
24 23 eleq1d 
 |-  ( ( A e. On /\ Lim x ) -> ( ( A .o x ) e. On <-> U_ y e. x ( A .o y ) e. On ) )
25 21 24 imbitrrid 
 |-  ( ( A e. On /\ Lim x ) -> ( A. y e. x ( A .o y ) e. On -> ( A .o x ) e. On ) )
26 25 expcom 
 |-  ( Lim x -> ( A e. On -> ( A. y e. x ( A .o y ) e. On -> ( A .o x ) e. On ) ) )
27 2 4 6 8 11 18 26 tfinds3 
 |-  ( B e. On -> ( A e. On -> ( A .o B ) e. On ) )
28 27 impcom 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )