Step | Hyp | Ref
| Expression |
1 | | nfv 1508 |
. . . . . . 7
Markov |
2 | | nfra1 2466 |
. . . . . . 7
DECID |
3 | 1, 2 | nfan 1544 |
. . . . . 6
Markov
DECID
|
4 | | simpr 109 |
. . . . . . . . 9
Markov
DECID
|
5 | | 0lt2o 6338 |
. . . . . . . . . . . 12
|
6 | 5 | a1i 9 |
. . . . . . . . . . 11
DECID
|
7 | | 1lt2o 6339 |
. . . . . . . . . . . 12
|
8 | 7 | a1i 9 |
. . . . . . . . . . 11
DECID
|
9 | | rsp 2480 |
. . . . . . . . . . . 12
DECID
DECID |
10 | 9 | imp 123 |
. . . . . . . . . . 11
DECID
DECID |
11 | 6, 8, 10 | ifcldcd 3507 |
. . . . . . . . . 10
DECID
|
12 | 11 | adantll 467 |
. . . . . . . . 9
Markov
DECID
|
13 | | eqid 2139 |
. . . . . . . . . 10
|
14 | 13 | fvmpt2 5504 |
. . . . . . . . 9
|
15 | 4, 12, 14 | syl2anc 408 |
. . . . . . . 8
Markov
DECID
|
16 | 15 | eqeq1d 2148 |
. . . . . . 7
Markov
DECID
|
17 | | 1n0 6329 |
. . . . . . . . . 10
|
18 | 17 | nesymi 2354 |
. . . . . . . . 9
|
19 | | iftrue 3479 |
. . . . . . . . . 10
|
20 | 19 | eqeq1d 2148 |
. . . . . . . . 9
|
21 | 18, 20 | mtbiri 664 |
. . . . . . . 8
|
22 | 21 | con2i 616 |
. . . . . . 7
|
23 | 16, 22 | syl6bi 162 |
. . . . . 6
Markov
DECID
|
24 | 3, 23 | ralimdaa 2498 |
. . . . 5
Markov
DECID
|
25 | 24 | con3d 620 |
. . . 4
Markov
DECID
|
26 | 25 | 3impia 1178 |
. . 3
Markov
DECID
|
27 | | mptexg 5645 |
. . . . 5
Markov |
28 | 27 | 3ad2ant1 1002 |
. . . 4
Markov
DECID
|
29 | | ismkv 7027 |
. . . . . 6
Markov Markov |
30 | 29 | ibi 175 |
. . . . 5
Markov |
31 | 30 | 3ad2ant1 1002 |
. . . 4
Markov
DECID
|
32 | | nfra1 2466 |
. . . . . . 7
|
33 | 32 | nfn 1636 |
. . . . . 6
|
34 | 1, 2, 33 | nf3an 1545 |
. . . . 5
Markov
DECID
|
35 | 11 | 3ad2antl2 1144 |
. . . . 5
Markov
DECID
|
36 | 34, 35, 13 | fmptdf 5577 |
. . . 4
Markov
DECID
|
37 | | feq1 5255 |
. . . . . 6
|
38 | | nfmpt1 4021 |
. . . . . . . . . 10
|
39 | 38 | nfeq2 2293 |
. . . . . . . . 9
|
40 | | fveq1 5420 |
. . . . . . . . . 10
|
41 | 40 | eqeq1d 2148 |
. . . . . . . . 9
|
42 | 39, 41 | ralbid 2435 |
. . . . . . . 8
|
43 | 42 | notbid 656 |
. . . . . . 7
|
44 | 40 | eqeq1d 2148 |
. . . . . . . 8
|
45 | 39, 44 | rexbid 2436 |
. . . . . . 7
|
46 | 43, 45 | imbi12d 233 |
. . . . . 6
|
47 | 37, 46 | imbi12d 233 |
. . . . 5
|
48 | 47 | spcgv 2773 |
. . . 4
|
49 | 28, 31, 36, 48 | syl3c 63 |
. . 3
Markov
DECID
|
50 | 26, 49 | mpd 13 |
. 2
Markov
DECID
|
51 | | simpr 109 |
. . . . . 6
Markov
DECID
|
52 | 51, 35, 14 | syl2anc 408 |
. . . . 5
Markov
DECID
|
53 | 52 | eqeq1d 2148 |
. . . 4
Markov
DECID
|
54 | 9 | 3ad2ant2 1003 |
. . . . . . 7
Markov
DECID
DECID |
55 | 54 | imp 123 |
. . . . . 6
Markov
DECID
DECID |
56 | 17 | neii 2310 |
. . . . . . . . 9
|
57 | | simpr 109 |
. . . . . . . . . . 11
Markov DECID
|
58 | 57 | iffalsed 3484 |
. . . . . . . . . 10
Markov DECID
|
59 | 58 | eqeq1d 2148 |
. . . . . . . . 9
Markov DECID
|
60 | 56, 59 | mtbiri 664 |
. . . . . . . 8
Markov DECID
|
61 | 60 | ex 114 |
. . . . . . 7
Markov
DECID
|
62 | 61 | con2d 613 |
. . . . . 6
Markov
DECID
|
63 | | notnotrdc 828 |
. . . . . 6
DECID |
64 | 55, 62, 63 | sylsyld 58 |
. . . . 5
Markov
DECID
|
65 | 64, 19 | impbid1 141 |
. . . 4
Markov
DECID
|
66 | 53, 65 | bitrd 187 |
. . 3
Markov
DECID
|
67 | 34, 66 | rexbida 2432 |
. 2
Markov
DECID
|
68 | 50, 67 | mpbid 146 |
1
Markov
DECID
|