Step | Hyp | Ref
| Expression |
1 | | mreexmrid.2 |
. 2
mrCls |
2 | | mreexmrid.3 |
. 2
mrInd |
3 | | mreexmrid.1 |
. 2
Moore |
4 | | mreexmrid.5 |
. . . 4
|
5 | 2, 3, 4 | mrissd 16296 |
. . 3
|
6 | | mreexmrid.6 |
. . . 4
|
7 | 6 | snssd 4340 |
. . 3
|
8 | 5, 7 | unssd 3789 |
. 2
|
9 | 3 | 3ad2ant1 1082 |
. . . . . . . . . 10
Moore |
10 | 9 | elfvexd 6222 |
. . . . . . . . 9
|
11 | | mreexmrid.4 |
. . . . . . . . . 10
|
12 | 11 | 3ad2ant1 1082 |
. . . . . . . . 9
|
13 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
14 | 2, 9, 13 | mrissd 16296 |
. . . . . . . . . 10
|
15 | 14 | ssdifssd 3748 |
. . . . . . . . 9
|
16 | 6 | 3ad2ant1 1082 |
. . . . . . . . 9
|
17 | | simp3 1063 |
. . . . . . . . . 10
|
18 | | difundir 3880 |
. . . . . . . . . . . 12
|
19 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
|
20 | 3, 1, 5 | mrcssidd 16285 |
. . . . . . . . . . . . . . . . . 18
|
21 | | mreexmrid.7 |
. . . . . . . . . . . . . . . . . 18
|
22 | 20, 21 | ssneldd 3606 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
24 | | nelneq 2725 |
. . . . . . . . . . . . . . . 16
|
25 | 19, 23, 24 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
26 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
27 | 25, 26 | nsyl 135 |
. . . . . . . . . . . . . 14
|
28 | | difsnb 4337 |
. . . . . . . . . . . . . 14
|
29 | 27, 28 | sylib 208 |
. . . . . . . . . . . . 13
|
30 | 29 | uneq2d 3767 |
. . . . . . . . . . . 12
|
31 | 18, 30 | syl5eq 2668 |
. . . . . . . . . . 11
|
32 | 31 | fveq2d 6195 |
. . . . . . . . . 10
|
33 | 17, 32 | eleqtrd 2703 |
. . . . . . . . 9
|
34 | 1, 2, 9, 13, 19 | ismri2dad 16297 |
. . . . . . . . 9
|
35 | 10, 12, 15, 16, 33, 34 | mreexd 16302 |
. . . . . . . 8
|
36 | 21 | 3ad2ant1 1082 |
. . . . . . . . 9
|
37 | | undif1 4043 |
. . . . . . . . . . 11
|
38 | 19 | snssd 4340 |
. . . . . . . . . . . 12
|
39 | | ssequn2 3786 |
. . . . . . . . . . . 12
|
40 | 38, 39 | sylib 208 |
. . . . . . . . . . 11
|
41 | 37, 40 | syl5eq 2668 |
. . . . . . . . . 10
|
42 | 41 | fveq2d 6195 |
. . . . . . . . 9
|
43 | 36, 42 | neleqtrrd 2723 |
. . . . . . . 8
|
44 | 35, 43 | pm2.65i 185 |
. . . . . . 7
|
45 | | df-3an 1039 |
. . . . . . 7
|
46 | 44, 45 | mtbi 312 |
. . . . . 6
|
47 | 46 | imnani 439 |
. . . . 5
|
48 | 47 | adantlr 751 |
. . . 4
|
49 | 26 | adantl 482 |
. . . . . 6
|
50 | 21 | ad2antrr 762 |
. . . . . 6
|
51 | 49, 50 | eqneltrd 2720 |
. . . . 5
|
52 | 49 | sneqd 4189 |
. . . . . . . . 9
|
53 | 52 | difeq2d 3728 |
. . . . . . . 8
|
54 | | difun2 4048 |
. . . . . . . 8
|
55 | 53, 54 | syl6eq 2672 |
. . . . . . 7
|
56 | | difsnb 4337 |
. . . . . . . . 9
|
57 | 22, 56 | sylib 208 |
. . . . . . . 8
|
58 | 57 | ad2antrr 762 |
. . . . . . 7
|
59 | 55, 58 | eqtrd 2656 |
. . . . . 6
|
60 | 59 | fveq2d 6195 |
. . . . 5
|
61 | 51, 60 | neleqtrrd 2723 |
. . . 4
|
62 | | simpr 477 |
. . . . 5
|
63 | | elun 3753 |
. . . . 5
|
64 | 62, 63 | sylib 208 |
. . . 4
|
65 | 48, 61, 64 | mpjaodan 827 |
. . 3
|
66 | 65 | ralrimiva 2966 |
. 2
|
67 | 1, 2, 3, 8, 66 | ismri2dd 16294 |
1
|