Step | Hyp | Ref
| Expression |
1 | | peano2nc 6145 |
. . . . . 6
NC
1c
NC |
2 | 1 | adantr 451 |
. . . . 5
NC NC 1c
NC |
3 | 2 | adantr 451 |
. . . 4
NC NC 1c
1c
1c NC |
4 | | elncs 6119 |
. . . . 5
1c
NC 1c
Nc |
5 | | simpr 447 |
. . . . . . . . 9
1c
1c 1c
Nc 1c Nc |
6 | | eqtr2 2371 |
. . . . . . . . 9
1c
1c 1c
Nc 1c Nc |
7 | 5, 6 | jca 518 |
. . . . . . . 8
1c
1c 1c
Nc
1c
Nc 1c
Nc |
8 | | vex 2862 |
. . . . . . . . . . . . . 14
|
9 | 8 | ncid 6123 |
. . . . . . . . . . . . 13
Nc |
10 | | eleq2 2414 |
. . . . . . . . . . . . 13
1c
Nc 1c
Nc |
11 | 9, 10 | mpbiri 224 |
. . . . . . . . . . . 12
1c
Nc
1c |
12 | | elsuc 4413 |
. . . . . . . . . . . . 13
1c
∼ |
13 | 12 | biimpi 186 |
. . . . . . . . . . . 12
1c
∼ |
14 | 11, 13 | syl 15 |
. . . . . . . . . . 11
1c
Nc ∼
|
15 | | eleq2 2414 |
. . . . . . . . . . . . 13
1c
Nc 1c
Nc |
16 | 9, 15 | mpbiri 224 |
. . . . . . . . . . . 12
1c
Nc
1c |
17 | | elsuc 4413 |
. . . . . . . . . . . 12
1c
∼ |
18 | 16, 17 | sylib 188 |
. . . . . . . . . . 11
1c
Nc ∼
|
19 | 14, 18 | anim12i 549 |
. . . . . . . . . 10
1c
Nc 1c
Nc
∼
∼ |
20 | | reeanv 2778 |
. . . . . . . . . . . . 13
∼ ∼
∼
∼ |
21 | 20 | 2rexbii 2641 |
. . . . . . . . . . . 12
∼ ∼
∼
∼ |
22 | | reeanv 2778 |
. . . . . . . . . . . 12
∼
∼
∼
∼
|
23 | 21, 22 | bitri 240 |
. . . . . . . . . . 11
∼ ∼
∼
∼
|
24 | | ncseqnc 6128 |
. . . . . . . . . . . . . . 15
NC Nc |
25 | | ncseqnc 6128 |
. . . . . . . . . . . . . . 15
NC Nc |
26 | 24, 25 | bi2anan9 843 |
. . . . . . . . . . . . . 14
NC NC Nc Nc
|
27 | 26 | biimpar 471 |
. . . . . . . . . . . . 13
NC NC
Nc Nc |
28 | | eqtr2 2371 |
. . . . . . . . . . . . . . . 16
|
29 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | elcompl 3225 |
. . . . . . . . . . . . . . . . 17
∼ |
31 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | elcompl 3225 |
. . . . . . . . . . . . . . . . 17
∼ |
33 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | 33, 34, 29, 31 | enadj 6060 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | 3expb 1152 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | ancoms 439 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | ex 423 |
. . . . . . . . . . . . . . . . 17
|
39 | 30, 32, 38 | syl2anb 465 |
. . . . . . . . . . . . . . . 16
∼
∼ |
40 | 28, 39 | syl5 28 |
. . . . . . . . . . . . . . 15
∼
∼ |
41 | 40 | rexlimivv 2743 |
. . . . . . . . . . . . . 14
∼ ∼ |
42 | | eqeq12 2365 |
. . . . . . . . . . . . . . 15
Nc Nc Nc Nc |
43 | 33 | eqnc 6127 |
. . . . . . . . . . . . . . 15
Nc Nc |
44 | 42, 43 | syl6bb 252 |
. . . . . . . . . . . . . 14
Nc Nc |
45 | 41, 44 | syl5ibr 212 |
. . . . . . . . . . . . 13
Nc Nc ∼ ∼
|
46 | 27, 45 | syl 15 |
. . . . . . . . . . . 12
NC NC ∼
∼ |
47 | 46 | rexlimdvva 2745 |
. . . . . . . . . . 11
NC NC
∼ ∼
|
48 | 23, 47 | syl5bir 209 |
. . . . . . . . . 10
NC NC
∼
∼
|
49 | 19, 48 | syl5 28 |
. . . . . . . . 9
NC NC
1c
Nc 1c
Nc |
50 | 49 | imp 418 |
. . . . . . . 8
NC NC
1c
Nc 1c
Nc
|
51 | 7, 50 | sylan2 460 |
. . . . . . 7
NC NC
1c
1c 1c
Nc
|
52 | 51 | expr 598 |
. . . . . 6
NC NC 1c
1c
1c
Nc |
53 | 52 | exlimdv 1636 |
. . . . 5
NC NC 1c
1c
1c Nc |
54 | 4, 53 | syl5bi 208 |
. . . 4
NC NC 1c
1c
1c
NC |
55 | 3, 54 | mpd 14 |
. . 3
NC NC 1c
1c
|
56 | 55 | ex 423 |
. 2
NC NC
1c
1c |
57 | | addceq1 4383 |
. 2
1c 1c |
58 | 56, 57 | impbid1 194 |
1
NC NC
1c
1c |