Step | Hyp | Ref
| Expression |
1 | | acsmre 16313 |
. 2
ACS
Moore |
2 | | mresspw 16252 |
. . . . . . . . . . 11
Moore
|
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
ACS
|
4 | | sspwb 4917 |
. . . . . . . . . 10
|
5 | 3, 4 | sylib 208 |
. . . . . . . . 9
ACS
|
6 | 5 | sselda 3603 |
. . . . . . . 8
ACS |
7 | 6 | elpwid 4170 |
. . . . . . 7
ACS
|
8 | | sspwuni 4611 |
. . . . . . 7
|
9 | 7, 8 | sylib 208 |
. . . . . 6
ACS
|
10 | 9 | adantr 481 |
. . . . 5
ACS
toInc
Dirset
|
11 | | inss1 3833 |
. . . . . . . . . . . 12
|
12 | 11 | sseli 3599 |
. . . . . . . . . . 11
|
13 | 12 | elpwid 4170 |
. . . . . . . . . 10
|
14 | | inss2 3834 |
. . . . . . . . . . 11
|
15 | 14 | sseli 3599 |
. . . . . . . . . 10
|
16 | | fissuni 8271 |
. . . . . . . . . 10
|
17 | 13, 15, 16 | syl2anc 693 |
. . . . . . . . 9
|
18 | 17 | ad2antll 765 |
. . . . . . . 8
ACS
toInc Dirset
|
19 | 1 | ad3antrrr 766 |
. . . . . . . . . 10
ACS
toInc Dirset Moore |
20 | | eqid 2622 |
. . . . . . . . . 10
mrCls mrCls |
21 | | simprr 796 |
. . . . . . . . . 10
ACS
toInc Dirset |
22 | | inss1 3833 |
. . . . . . . . . . . . . . 15
|
23 | 22 | sseli 3599 |
. . . . . . . . . . . . . 14
|
24 | 23 | elpwid 4170 |
. . . . . . . . . . . . 13
|
25 | 24 | unissd 4462 |
. . . . . . . . . . . 12
|
26 | 25 | ad2antrl 764 |
. . . . . . . . . . 11
ACS
toInc Dirset |
27 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
ACS
toInc Dirset |
28 | 26, 27 | sstrd 3613 |
. . . . . . . . . 10
ACS
toInc Dirset |
29 | 19, 20, 21, 28 | mrcssd 16284 |
. . . . . . . . 9
ACS
toInc Dirset mrCls
mrCls |
30 | | simpl 473 |
. . . . . . . . . . . . . . 15
toInc Dirset toInc Dirset |
31 | 24 | adantl 482 |
. . . . . . . . . . . . . . 15
toInc Dirset |
32 | | inss2 3834 |
. . . . . . . . . . . . . . . . 17
|
33 | 32 | sseli 3599 |
. . . . . . . . . . . . . . . 16
|
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . 15
toInc Dirset |
35 | | ipodrsfi 17163 |
. . . . . . . . . . . . . . 15
toInc Dirset
|
36 | 30, 31, 34, 35 | syl3anc 1326 |
. . . . . . . . . . . . . 14
toInc Dirset
|
37 | 36 | adantl 482 |
. . . . . . . . . . . . 13
ACS
toInc Dirset |
38 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
ACS
toInc Dirset
Moore |
39 | | simprr 796 |
. . . . . . . . . . . . . . 15
ACS
toInc Dirset
|
40 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . 17
ACS
|
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
ACS
toInc Dirset
|
43 | | simprl 794 |
. . . . . . . . . . . . . . . 16
ACS
toInc Dirset
|
44 | 42, 43 | sseldd 3604 |
. . . . . . . . . . . . . . 15
ACS
toInc Dirset
|
45 | 20 | mrcsscl 16280 |
. . . . . . . . . . . . . . 15
Moore mrCls |
46 | 38, 39, 44, 45 | syl3anc 1326 |
. . . . . . . . . . . . . 14
ACS
toInc Dirset
mrCls |
47 | | elssuni 4467 |
. . . . . . . . . . . . . . 15
|
48 | 47 | ad2antrl 764 |
. . . . . . . . . . . . . 14
ACS
toInc Dirset
|
49 | 46, 48 | sstrd 3613 |
. . . . . . . . . . . . 13
ACS
toInc Dirset
mrCls |
50 | 37, 49 | rexlimddv 3035 |
. . . . . . . . . . . 12
ACS
toInc Dirset mrCls |
51 | 50 | anassrs 680 |
. . . . . . . . . . 11
ACS
toInc Dirset
mrCls |
52 | 51 | adantrr 753 |
. . . . . . . . . 10
ACS
toInc Dirset mrCls |
53 | 52 | adantlrr 757 |
. . . . . . . . 9
ACS
toInc Dirset mrCls |
54 | 29, 53 | sstrd 3613 |
. . . . . . . 8
ACS
toInc Dirset mrCls
|
55 | 18, 54 | rexlimddv 3035 |
. . . . . . 7
ACS
toInc Dirset mrCls
|
56 | 55 | anassrs 680 |
. . . . . 6
ACS
toInc Dirset
mrCls |
57 | 56 | ralrimiva 2966 |
. . . . 5
ACS
toInc
Dirset mrCls
|
58 | 20 | acsfiel 16315 |
. . . . . 6
ACS
mrCls |
59 | 58 | ad2antrr 762 |
. . . . 5
ACS
toInc
Dirset mrCls
|
60 | 10, 57, 59 | mpbir2and 957 |
. . . 4
ACS
toInc
Dirset |
61 | 60 | ex 450 |
. . 3
ACS toInc Dirset
|
62 | 61 | ralrimiva 2966 |
. 2
ACS
toInc Dirset |
63 | 1, 62 | jca 554 |
1
ACS
Moore toInc Dirset |