Metamath Proof Explorer

Theorem oacl

Description: Closure law for ordinal addition. Proposition 8.2 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 5-May-1995)

Ref Expression
Assertion oacl 
|- ( ( 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 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
10 9 eleq1d 
 |-  ( A e. On -> ( ( A +o (/) ) e. On <-> A e. On ) )
11 10 ibir 
 |-  ( A e. On -> ( A +o (/) ) e. On )
12 onsuc 
 |-  ( ( A +o y ) e. On -> suc ( A +o y ) e. On )
13 oasuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A +o suc y ) = suc ( A +o y ) )
14 13 eleq1d 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A +o suc y ) e. On <-> suc ( A +o y ) e. On ) )
15 12 14 imbitrrid 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A +o y ) e. On -> ( A +o suc y ) e. On ) )
16 15 expcom 
 |-  ( y e. On -> ( A e. On -> ( ( A +o y ) e. On -> ( A +o suc y ) e. On ) ) )
17 vex 
 |-  x e. _V
18 iunon 
 |-  ( ( x e. _V /\ A. y e. x ( A +o y ) e. On ) -> U_ y e. x ( A +o y ) e. On )
19 17 18 mpan 
 |-  ( A. y e. x ( A +o y ) e. On -> U_ y e. x ( A +o y ) e. On )
20 oalim 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A +o x ) = U_ y e. x ( A +o y ) )
21 17 20 mpanr1 
 |-  ( ( A e. On /\ Lim x ) -> ( A +o x ) = U_ y e. x ( A +o y ) )
22 21 eleq1d 
 |-  ( ( A e. On /\ Lim x ) -> ( ( A +o x ) e. On <-> U_ y e. x ( A +o y ) e. On ) )
23 19 22 imbitrrid 
 |-  ( ( A e. On /\ Lim x ) -> ( A. y e. x ( A +o y ) e. On -> ( A +o x ) e. On ) )
24 23 expcom 
 |-  ( Lim x -> ( A e. On -> ( A. y e. x ( A +o y ) e. On -> ( A +o x ) e. On ) ) )
25 2 4 6 8 11 16 24 tfinds3 
 |-  ( B e. On -> ( A e. On -> ( A +o B ) e. On ) )
26 25 impcom 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )