Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
|
2 | | difeq2 3188 |
. . . 4
|
3 | 1, 2 | uneq12d 3231 |
. . 3
|
4 | 3 | eqeq2d 2151 |
. 2
|
5 | | id 19 |
. . . 4
|
6 | | difeq2 3188 |
. . . 4
|
7 | 5, 6 | uneq12d 3231 |
. . 3
|
8 | 7 | eqeq2d 2151 |
. 2
|
9 | | id 19 |
. . . 4
|
10 | | difeq2 3188 |
. . . 4
|
11 | 9, 10 | uneq12d 3231 |
. . 3
|
12 | 11 | eqeq2d 2151 |
. 2
|
13 | | id 19 |
. . . 4
|
14 | | difeq2 3188 |
. . . 4
|
15 | 13, 14 | uneq12d 3231 |
. . 3
|
16 | 15 | eqeq2d 2151 |
. 2
|
17 | | un0 3396 |
. . . 4
|
18 | | uncom 3220 |
. . . 4
|
19 | | dif0 3433 |
. . . 4
|
20 | 17, 18, 19 | 3eqtr3ri 2169 |
. . 3
|
21 | 20 | a1i 9 |
. 2
DECID
|
22 | | difundi 3328 |
. . . . . . 7
|
23 | 22 | uneq2i 3227 |
. . . . . 6
|
24 | | undi 3324 |
. . . . . 6
|
25 | 23, 24 | eqtri 2160 |
. . . . 5
|
26 | | simp3 983 |
. . . . . . . . . . . 12
DECID
|
27 | 26 | ad3antrrr 483 |
. . . . . . . . . . 11
DECID
|
28 | | simplrr 525 |
. . . . . . . . . . . 12
DECID
|
29 | 28 | eldifad 3082 |
. . . . . . . . . . 11
DECID
|
30 | 27, 29 | sseldd 3098 |
. . . . . . . . . 10
DECID
|
31 | 30 | snssd 3665 |
. . . . . . . . 9
DECID
|
32 | | ssequn1 3246 |
. . . . . . . . 9
|
33 | 31, 32 | sylib 121 |
. . . . . . . 8
DECID
|
34 | | simpr 109 |
. . . . . . . . 9
DECID
|
35 | 34 | uneq2d 3230 |
. . . . . . . 8
DECID
|
36 | 33, 35 | eqtr3d 2174 |
. . . . . . 7
DECID
|
37 | | uncom 3220 |
. . . . . . . . 9
|
38 | 37 | uneq1i 3226 |
. . . . . . . 8
|
39 | | unass 3233 |
. . . . . . . 8
|
40 | 38, 39 | eqtri 2160 |
. . . . . . 7
|
41 | 36, 40 | syl6reqr 2191 |
. . . . . 6
DECID
|
42 | | unass 3233 |
. . . . . . . 8
|
43 | | uncom 3220 |
. . . . . . . . . 10
|
44 | | simp1 981 |
. . . . . . . . . . . 12
DECID
DECID
|
45 | 44 | ad3antrrr 483 |
. . . . . . . . . . 11
DECID
DECID |
46 | | dcdifsnid 6400 |
. . . . . . . . . . 11
DECID
|
47 | 45, 30, 46 | syl2anc 408 |
. . . . . . . . . 10
DECID
|
48 | 43, 47 | syl5eq 2184 |
. . . . . . . . 9
DECID
|
49 | 48 | uneq2d 3230 |
. . . . . . . 8
DECID
|
50 | 42, 49 | syl5eq 2184 |
. . . . . . 7
DECID
|
51 | | simplrl 524 |
. . . . . . . . 9
DECID
|
52 | 51, 27 | sstrd 3107 |
. . . . . . . 8
DECID
|
53 | | ssequn1 3246 |
. . . . . . . 8
|
54 | 52, 53 | sylib 121 |
. . . . . . 7
DECID
|
55 | 50, 54 | eqtrd 2172 |
. . . . . 6
DECID
|
56 | 41, 55 | ineq12d 3278 |
. . . . 5
DECID
|
57 | 25, 56 | syl5eq 2184 |
. . . 4
DECID
|
58 | | inidm 3285 |
. . . 4
|
59 | 57, 58 | syl6req 2189 |
. . 3
DECID
|
60 | 59 | ex 114 |
. 2
DECID
|
61 | | simp2 982 |
. 2
DECID
|
62 | 4, 8, 12, 16, 21, 60, 61 | findcard2sd 6786 |
1
DECID
|