Step | Hyp | Ref
| Expression |
1 | | eldif 3485 |
. . . . . 6
|
2 | | sneq 4039 |
. . . . . . . . . 10
|
3 | 2 | imaeq2d 5342 |
. . . . . . . . 9
|
4 | 3 | neeq1d 2734 |
. . . . . . . 8
|
5 | 4 | elrab 3257 |
. . . . . . 7
|
6 | | ianor 488 |
. . . . . . . 8
|
7 | 2 | imaeq2d 5342 |
. . . . . . . . . 10
|
8 | 7 | neeq1d 2734 |
. . . . . . . . 9
|
9 | 8 | elrab 3257 |
. . . . . . . 8
|
10 | 6, 9 | xchnxbir 309 |
. . . . . . 7
|
11 | | ianor 488 |
. . . . . . . . . . 11
|
12 | | dmres 5299 |
. . . . . . . . . . . 12
|
13 | 12 | elin2 3688 |
. . . . . . . . . . 11
|
14 | 11, 13 | xchnxbir 309 |
. . . . . . . . . 10
|
15 | | simpl 457 |
. . . . . . . . . . . . . . 15
|
16 | 15 | anim2i 569 |
. . . . . . . . . . . . . 14
|
17 | 16 | ancomd 451 |
. . . . . . . . . . . . 13
|
18 | | eldif 3485 |
. . . . . . . . . . . . 13
|
19 | 17, 18 | sylibr 212 |
. . . . . . . . . . . 12
|
20 | 19 | ex 434 |
. . . . . . . . . . 11
|
21 | | pm2.24 109 |
. . . . . . . . . . . . 13
|
22 | 21 | adantr 465 |
. . . . . . . . . . . 12
|
23 | 22 | com12 31 |
. . . . . . . . . . 11
|
24 | 20, 23 | jaoi 379 |
. . . . . . . . . 10
|
25 | 14, 24 | sylbi 195 |
. . . . . . . . 9
|
26 | 15 | adantl 466 |
. . . . . . . . . . 11
|
27 | | snssi 4174 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | 27 | adantl 466 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | | resima2 5312 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 28, 29 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 30 | eqcomd 2465 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
33 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
|
34 | 32, 33 | eqtrd 2498 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | ex 434 |
. . . . . . . . . . . . . . 15
|
36 | 35 | necon3d 2681 |
. . . . . . . . . . . . . 14
|
37 | 36 | impancom 440 |
. . . . . . . . . . . . 13
|
38 | 37 | con3d 133 |
. . . . . . . . . . . 12
|
39 | 38 | impcom 430 |
. . . . . . . . . . 11
|
40 | 26, 39 | eldifd 3486 |
. . . . . . . . . 10
|
41 | 40 | ex 434 |
. . . . . . . . 9
|
42 | 25, 41 | jaoi 379 |
. . . . . . . 8
|
43 | 42 | impcom 430 |
. . . . . . 7
|
44 | 5, 10, 43 | syl2anb 479 |
. . . . . 6
|
45 | 1, 44 | sylbi 195 |
. . . . 5
|
46 | 45 | a1i 11 |
. . . 4
|
47 | 46 | ssrdv 3509 |
. . 3
|
48 | | ssundif 3911 |
. . 3
|
49 | 47, 48 | sylibr 212 |
. 2
|
50 | | suppval 6920 |
. 2
|
51 | | resexg 5321 |
. . . 4
|
52 | | suppval 6920 |
. . . 4
|
53 | 51, 52 | sylan 471 |
. . 3
|
54 | 53 | uneq1d 3656 |
. 2
|
55 | 49, 50, 54 | 3sstr4d 3546 |
1
|