Metamath Proof Explorer


Theorem oacl

Description: Closure law for ordinal addition. Proposition 8.2 of TakeutiZaring p. 57. (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 suceloni
 |-  ( ( 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 syl5ibr
 |-  ( ( 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 syl5ibr
 |-  ( ( 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 )