Step | Hyp | Ref
| Expression |
1 | | nnc0suc 4412 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | addceq2 4384 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) 0c![)](rp.gif) ![)](rp.gif) |
3 | | addcid1 4405 |
. . . . . . . . . 10
![(](lp.gif) 0c
![A](_ca.gif) |
4 | 2, 3 | syl6req 2402 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | addceq2 4384 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | addcass 4415 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | syl6eqr 2403 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
8 | 7 | reximi 2721 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
9 | 4, 8 | orim12i 502 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![x](_x.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 1, 9 | sylbi 187 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | orcomd 377 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif)
![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | rexbidv 2635 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | eqeq2 2362 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif)
![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | orbi12d 690 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 11, 15 | syl5ibrcom 213 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | rexlimiv 2732 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 6 | eqeq2i 2363 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c
![(](lp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | peano2 4403 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
20 | 5 | eqeq2d 2364 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | rspcev 2955 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 19, 21 | sylan 457 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 18, 22 | sylan2b 461 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | rexlimiva 2733 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | peano1 4402 |
. . . . . . 7
0c
Nn |
26 | 3 | eqcomi 2357 |
. . . . . . 7
![(](lp.gif)
0c![)](rp.gif) |
27 | 2 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | rspcev 2955 |
. . . . . . 7
![(](lp.gif) 0c Nn ![(](lp.gif)
0c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 25, 26, 28 | mp2an 653 |
. . . . . 6
![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) |
30 | | eqeq1 2359 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![x](_x.gif) ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | rexbidv 2635 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 29, 31 | mpbii 202 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 24, 32 | jaoi 368 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![E.](exists.gif) Nn ![(](lp.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 17, 33 | impbii 180 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | a1i 10 |
. 2
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | opklefing 4448 |
. . 3
![(](lp.gif) ![(](lp.gif)
![W](_cw.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | 3adant3 975 |
. 2
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | opkltfing 4449 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
![W](_cw.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | adantr 451 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![W](_cw.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | ibar 490 |
. . . . . 6
![(](lp.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | adantl 452 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![W](_cw.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 39, 41 | bitr4d 247 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![W](_cw.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | orbi1d 683 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![W](_cw.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![B](_cb.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | 3impa 1146 |
. 2
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![B](_cb.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 35, 37, 44 | 3bitr4d 276 |
1
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |