Step | Hyp | Ref
| Expression |
1 | | nacsacs 37272 |
. . . 4
NoeACS
ACS |
2 | 1 | acsmred 16317 |
. . 3
NoeACS
Moore |
3 | | simpll 790 |
. . . . . . . 8
NoeACS toInc Dirset
NoeACS |
4 | 1 | ad2antrr 762 |
. . . . . . . . 9
NoeACS toInc Dirset
ACS |
5 | | elpwi 4168 |
. . . . . . . . . 10
|
6 | 5 | ad2antlr 763 |
. . . . . . . . 9
NoeACS toInc Dirset
|
7 | | simpr 477 |
. . . . . . . . 9
NoeACS toInc Dirset
toInc
Dirset |
8 | | acsdrsel 17167 |
. . . . . . . . 9
ACS toInc Dirset |
9 | 4, 6, 7, 8 | syl3anc 1326 |
. . . . . . . 8
NoeACS toInc Dirset
|
10 | | eqid 2622 |
. . . . . . . . 9
mrCls mrCls |
11 | 10 | nacsfg 37268 |
. . . . . . . 8
NoeACS
mrCls |
12 | 3, 9, 11 | syl2anc 693 |
. . . . . . 7
NoeACS toInc Dirset
mrCls |
13 | 10 | mrefg2 37270 |
. . . . . . . . 9
Moore
mrCls mrCls |
14 | 2, 13 | syl 17 |
. . . . . . . 8
NoeACS
mrCls mrCls |
15 | 14 | ad2antrr 762 |
. . . . . . 7
NoeACS toInc Dirset
mrCls mrCls |
16 | 12, 15 | mpbid 222 |
. . . . . 6
NoeACS toInc Dirset
mrCls |
17 | | elfpw 8268 |
. . . . . . . . 9
|
18 | | fissuni 8271 |
. . . . . . . . 9
|
19 | 17, 18 | sylbi 207 |
. . . . . . . 8
|
20 | | elfpw 8268 |
. . . . . . . . . . . 12
|
21 | | ipodrsfi 17163 |
. . . . . . . . . . . . 13
toInc Dirset
|
22 | 21 | 3expb 1266 |
. . . . . . . . . . . 12
toInc Dirset
|
23 | 20, 22 | sylan2b 492 |
. . . . . . . . . . 11
toInc Dirset
|
24 | | sstr 3611 |
. . . . . . . . . . . . . . 15
|
25 | 24 | ancoms 469 |
. . . . . . . . . . . . . 14
|
26 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
NoeACS
mrCls
mrCls |
27 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
NoeACS Moore |
28 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . 21
NoeACS |
29 | 5 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
NoeACS |
30 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
NoeACS |
31 | 29, 30 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
NoeACS |
32 | 10 | mrcsscl 16280 |
. . . . . . . . . . . . . . . . . . . . 21
Moore mrCls |
33 | 27, 28, 31, 32 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
NoeACS mrCls |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
NoeACS
mrCls
mrCls
|
35 | 26, 34 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . 18
NoeACS
mrCls
|
36 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
NoeACS
mrCls
|
37 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
NoeACS
mrCls
|
39 | 35, 38 | eqssd 3620 |
. . . . . . . . . . . . . . . . 17
NoeACS
mrCls
|
40 | 39, 36 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
NoeACS
mrCls
|
41 | 40 | ex 450 |
. . . . . . . . . . . . . . 15
NoeACS
mrCls |
42 | 41 | expr 643 |
. . . . . . . . . . . . . 14
NoeACS
mrCls |
43 | 25, 42 | syl5 34 |
. . . . . . . . . . . . 13
NoeACS
mrCls |
44 | 43 | expd 452 |
. . . . . . . . . . . 12
NoeACS
mrCls
|
45 | 44 | rexlimdva 3031 |
. . . . . . . . . . 11
NoeACS
mrCls
|
46 | 23, 45 | syl5 34 |
. . . . . . . . . 10
NoeACS toInc Dirset mrCls |
47 | 46 | expdimp 453 |
. . . . . . . . 9
NoeACS toInc Dirset
mrCls |
48 | 47 | rexlimdv 3030 |
. . . . . . . 8
NoeACS toInc Dirset
mrCls |
49 | 19, 48 | syl5 34 |
. . . . . . 7
NoeACS toInc Dirset
mrCls |
50 | 49 | rexlimdv 3030 |
. . . . . 6
NoeACS toInc Dirset
mrCls |
51 | 16, 50 | mpd 15 |
. . . . 5
NoeACS toInc Dirset
|
52 | 51 | ex 450 |
. . . 4
NoeACS toInc Dirset
|
53 | 52 | ralrimiva 2966 |
. . 3
NoeACS
toInc Dirset |
54 | 2, 53 | jca 554 |
. 2
NoeACS
Moore toInc Dirset |
55 | | simpl 473 |
. . . 4
Moore
toInc Dirset
Moore |
56 | 5 | adantl 482 |
. . . . . . . 8
Moore
|
57 | 56 | sseld 3602 |
. . . . . . 7
Moore
|
58 | 57 | imim2d 57 |
. . . . . 6
Moore toInc Dirset toInc Dirset |
59 | 58 | ralimdva 2962 |
. . . . 5
Moore
toInc Dirset
toInc Dirset |
60 | 59 | imp 445 |
. . . 4
Moore
toInc Dirset
toInc Dirset |
61 | | isacs3 17174 |
. . . 4
ACS Moore toInc Dirset |
62 | 55, 60, 61 | sylanbrc 698 |
. . 3
Moore
toInc Dirset
ACS |
63 | 10 | mrcid 16273 |
. . . . . . . . . 10
Moore mrCls |
64 | 63 | adantlr 751 |
. . . . . . . . 9
Moore
toInc Dirset
mrCls |
65 | 62 | adantr 481 |
. . . . . . . . . 10
Moore
toInc Dirset
ACS |
66 | | mress 16253 |
. . . . . . . . . . 11
Moore |
67 | 66 | adantlr 751 |
. . . . . . . . . 10
Moore
toInc Dirset
|
68 | 65, 10, 67 | acsficld 17175 |
. . . . . . . . 9
Moore
toInc Dirset
mrCls mrCls
|
69 | 64, 68 | eqtr3d 2658 |
. . . . . . . 8
Moore
toInc Dirset
mrCls |
70 | 10 | mrcf 16269 |
. . . . . . . . . . . . 13
Moore
mrCls |
71 | | ffn 6045 |
. . . . . . . . . . . . 13
mrCls
mrCls |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
Moore
mrCls |
73 | 72 | adantr 481 |
. . . . . . . . . . 11
Moore mrCls |
74 | 10 | mrcss 16276 |
. . . . . . . . . . . . 13
Moore mrCls mrCls |
75 | 74 | 3expb 1266 |
. . . . . . . . . . . 12
Moore
mrCls
mrCls |
76 | 75 | adantlr 751 |
. . . . . . . . . . 11
Moore
mrCls
mrCls |
77 | | vex 3203 |
. . . . . . . . . . . 12
|
78 | | fpwipodrs 17164 |
. . . . . . . . . . . 12
toInc Dirset |
79 | 77, 78 | mp1i 13 |
. . . . . . . . . . 11
Moore toInc Dirset |
80 | | inss1 3833 |
. . . . . . . . . . . 12
|
81 | | sspwb 4917 |
. . . . . . . . . . . . 13
|
82 | 66, 81 | sylib 208 |
. . . . . . . . . . . 12
Moore |
83 | 80, 82 | syl5ss 3614 |
. . . . . . . . . . 11
Moore
|
84 | | fvex 6201 |
. . . . . . . . . . . . 13
mrCls |
85 | | imaexg 7103 |
. . . . . . . . . . . . 13
mrCls mrCls |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . 12
mrCls
|
87 | 86 | a1i 11 |
. . . . . . . . . . 11
Moore mrCls |
88 | 73, 76, 79, 83, 87 | ipodrsima 17165 |
. . . . . . . . . 10
Moore toIncmrCls Dirset |
89 | 88 | adantlr 751 |
. . . . . . . . 9
Moore
toInc Dirset
toIncmrCls
Dirset |
90 | | imassrn 5477 |
. . . . . . . . . . . . . 14
mrCls
mrCls |
91 | | frn 6053 |
. . . . . . . . . . . . . . 15
mrCls
mrCls |
92 | 70, 91 | syl 17 |
. . . . . . . . . . . . . 14
Moore
mrCls |
93 | 90, 92 | syl5ss 3614 |
. . . . . . . . . . . . 13
Moore
mrCls
|
94 | 93 | adantr 481 |
. . . . . . . . . . . 12
Moore mrCls |
95 | 86 | elpw 4164 |
. . . . . . . . . . . 12
mrCls
mrCls
|
96 | 94, 95 | sylibr 224 |
. . . . . . . . . . 11
Moore mrCls |
97 | 96 | adantlr 751 |
. . . . . . . . . 10
Moore
toInc Dirset
mrCls |
98 | | simplr 792 |
. . . . . . . . . 10
Moore
toInc Dirset
toInc Dirset |
99 | | fveq2 6191 |
. . . . . . . . . . . . 13
mrCls
toInc toIncmrCls |
100 | 99 | eleq1d 2686 |
. . . . . . . . . . . 12
mrCls
toInc Dirset
toIncmrCls Dirset |
101 | | unieq 4444 |
. . . . . . . . . . . . 13
mrCls
mrCls
|
102 | | id 22 |
. . . . . . . . . . . . 13
mrCls
mrCls |
103 | 101, 102 | eleq12d 2695 |
. . . . . . . . . . . 12
mrCls
mrCls mrCls |
104 | 100, 103 | imbi12d 334 |
. . . . . . . . . . 11
mrCls
toInc Dirset toIncmrCls Dirset mrCls
mrCls
|
105 | 104 | rspcva 3307 |
. . . . . . . . . 10
mrCls toInc Dirset
toIncmrCls Dirset mrCls mrCls
|
106 | 97, 98, 105 | syl2anc 693 |
. . . . . . . . 9
Moore
toInc Dirset
toIncmrCls Dirset mrCls
mrCls
|
107 | 89, 106 | mpd 15 |
. . . . . . . 8
Moore
toInc Dirset
mrCls
mrCls
|
108 | 69, 107 | eqeltrd 2701 |
. . . . . . 7
Moore
toInc Dirset
mrCls
|
109 | | fvelimab 6253 |
. . . . . . . . 9
mrCls
mrCls
mrCls |
110 | 73, 83, 109 | syl2anc 693 |
. . . . . . . 8
Moore mrCls
mrCls |
111 | 110 | adantlr 751 |
. . . . . . 7
Moore
toInc Dirset
mrCls
mrCls |
112 | 108, 111 | mpbid 222 |
. . . . . 6
Moore
toInc Dirset
mrCls |
113 | | eqcom 2629 |
. . . . . . 7
mrCls mrCls |
114 | 113 | rexbii 3041 |
. . . . . 6
mrCls mrCls |
115 | 112, 114 | sylibr 224 |
. . . . 5
Moore
toInc Dirset
mrCls |
116 | 10 | mrefg2 37270 |
. . . . . 6
Moore
mrCls mrCls |
117 | 116 | ad2antrr 762 |
. . . . 5
Moore
toInc Dirset
mrCls
mrCls |
118 | 115, 117 | mpbird 247 |
. . . 4
Moore
toInc Dirset
mrCls |
119 | 118 | ralrimiva 2966 |
. . 3
Moore
toInc Dirset
mrCls |
120 | 10 | isnacs 37267 |
. . 3
NoeACS ACS
mrCls |
121 | 62, 119, 120 | sylanbrc 698 |
. 2
Moore
toInc Dirset
NoeACS |
122 | 54, 121 | impbii 199 |
1
NoeACS Moore toInc Dirset |