Step |
Hyp |
Ref |
Expression |
1 |
|
pinn |
|- ( A e. N. -> A e. _om ) |
2 |
|
pinn |
|- ( B e. N. -> B e. _om ) |
3 |
|
nnaordex |
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. N. /\ B e. N. ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) |
5 |
|
ltpiord |
|- ( ( A e. N. /\ B e. N. ) -> ( A A e. B ) ) |
6 |
|
addpiord |
|- ( ( A e. N. /\ x e. N. ) -> ( A +N x ) = ( A +o x ) ) |
7 |
6
|
eqeq1d |
|- ( ( A e. N. /\ x e. N. ) -> ( ( A +N x ) = B <-> ( A +o x ) = B ) ) |
8 |
7
|
pm5.32da |
|- ( A e. N. -> ( ( x e. N. /\ ( A +N x ) = B ) <-> ( x e. N. /\ ( A +o x ) = B ) ) ) |
9 |
|
elni2 |
|- ( x e. N. <-> ( x e. _om /\ (/) e. x ) ) |
10 |
9
|
anbi1i |
|- ( ( x e. N. /\ ( A +o x ) = B ) <-> ( ( x e. _om /\ (/) e. x ) /\ ( A +o x ) = B ) ) |
11 |
|
anass |
|- ( ( ( x e. _om /\ (/) e. x ) /\ ( A +o x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) ) |
12 |
10 11
|
bitri |
|- ( ( x e. N. /\ ( A +o x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) ) |
13 |
8 12
|
bitrdi |
|- ( A e. N. -> ( ( x e. N. /\ ( A +N x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) ) ) |
14 |
13
|
rexbidv2 |
|- ( A e. N. -> ( E. x e. N. ( A +N x ) = B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) |
15 |
14
|
adantr |
|- ( ( A e. N. /\ B e. N. ) -> ( E. x e. N. ( A +N x ) = B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) |
16 |
4 5 15
|
3bitr4d |
|- ( ( A e. N. /\ B e. N. ) -> ( A E. x e. N. ( A +N x ) = B ) ) |