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 ) |