Step |
Hyp |
Ref |
Expression |
1 |
|
ssexg |
|- ( ( _om C_ B /\ B e. On ) -> _om e. _V ) |
2 |
1
|
ex |
|- ( _om C_ B -> ( B e. On -> _om e. _V ) ) |
3 |
|
omelon2 |
|- ( _om e. _V -> _om e. On ) |
4 |
2 3
|
syl6com |
|- ( B e. On -> ( _om C_ B -> _om e. On ) ) |
5 |
4
|
imp |
|- ( ( B e. On /\ _om C_ B ) -> _om e. On ) |
6 |
5
|
adantll |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> _om e. On ) |
7 |
|
simplr |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> B e. On ) |
8 |
6 7
|
jca |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( _om e. On /\ B e. On ) ) |
9 |
|
oawordeu |
|- ( ( ( _om e. On /\ B e. On ) /\ _om C_ B ) -> E! x e. On ( _om +o x ) = B ) |
10 |
8 9
|
sylancom |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> E! x e. On ( _om +o x ) = B ) |
11 |
|
reurex |
|- ( E! x e. On ( _om +o x ) = B -> E. x e. On ( _om +o x ) = B ) |
12 |
10 11
|
syl |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> E. x e. On ( _om +o x ) = B ) |
13 |
|
nnon |
|- ( A e. _om -> A e. On ) |
14 |
13
|
ad3antrrr |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> A e. On ) |
15 |
6
|
adantr |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> _om e. On ) |
16 |
|
simpr |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> x e. On ) |
17 |
|
oaass |
|- ( ( A e. On /\ _om e. On /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( A +o ( _om +o x ) ) ) |
18 |
14 15 16 17
|
syl3anc |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( A +o ( _om +o x ) ) ) |
19 |
|
simpll |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> A e. _om ) |
20 |
|
oaabslem |
|- ( ( _om e. On /\ A e. _om ) -> ( A +o _om ) = _om ) |
21 |
6 19 20
|
syl2anc |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( A +o _om ) = _om ) |
22 |
21
|
adantr |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( A +o _om ) = _om ) |
23 |
22
|
oveq1d |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( _om +o x ) ) |
24 |
18 23
|
eqtr3d |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( A +o ( _om +o x ) ) = ( _om +o x ) ) |
25 |
|
oveq2 |
|- ( ( _om +o x ) = B -> ( A +o ( _om +o x ) ) = ( A +o B ) ) |
26 |
|
id |
|- ( ( _om +o x ) = B -> ( _om +o x ) = B ) |
27 |
25 26
|
eqeq12d |
|- ( ( _om +o x ) = B -> ( ( A +o ( _om +o x ) ) = ( _om +o x ) <-> ( A +o B ) = B ) ) |
28 |
24 27
|
syl5ibcom |
|- ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( _om +o x ) = B -> ( A +o B ) = B ) ) |
29 |
28
|
rexlimdva |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( E. x e. On ( _om +o x ) = B -> ( A +o B ) = B ) ) |
30 |
12 29
|
mpd |
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( A +o B ) = B ) |