Step | Hyp | Ref
| Expression |
1 | | nacsacs 35545 |
. . . 4
 NoeACS 
ACS    |
2 | 1 | acsmred 15555 |
. . 3
 NoeACS 
Moore    |
3 | | simpll 759 |
. . . . . . . 8
   NoeACS    toInc  Dirset
NoeACS    |
4 | 1 | ad2antrr 731 |
. . . . . . . . 9
   NoeACS    toInc  Dirset
ACS    |
5 | | elpwi 3959 |
. . . . . . . . . 10
 
  |
6 | 5 | ad2antlr 732 |
. . . . . . . . 9
   NoeACS    toInc  Dirset
  |
7 | | simpr 463 |
. . . . . . . . 9
   NoeACS    toInc  Dirset
toInc 
Dirset |
8 | | acsdrsel 16406 |
. . . . . . . . 9
  ACS  toInc  Dirset    |
9 | 4, 6, 7, 8 | syl3anc 1267 |
. . . . . . . 8
   NoeACS    toInc  Dirset
   |
10 | | eqid 2450 |
. . . . . . . . 9
mrCls  mrCls   |
11 | 10 | nacsfg 35541 |
. . . . . . . 8
  NoeACS  
        mrCls       |
12 | 3, 9, 11 | syl2anc 666 |
. . . . . . 7
   NoeACS    toInc  Dirset
       mrCls       |
13 | 10 | mrefg2 35543 |
. . . . . . . . 9
 Moore 
 
    
 mrCls             mrCls        |
14 | 2, 13 | syl 17 |
. . . . . . . 8
 NoeACS 
 
    
 mrCls             mrCls        |
15 | 14 | ad2antrr 731 |
. . . . . . 7
   NoeACS    toInc  Dirset
 
    
 mrCls             mrCls        |
16 | 12, 15 | mpbid 214 |
. . . . . 6
   NoeACS    toInc  Dirset
        mrCls       |
17 | | elfpw 7873 |
. . . . . . . . 9
    
     |
18 | | fissuni 7876 |
. . . . . . . . 9
 

         |
19 | 17, 18 | sylbi 199 |
. . . . . . . 8
     
 
 
   |
20 | | elfpw 7873 |
. . . . . . . . . . . 12
   
    |
21 | | ipodrsfi 16402 |
. . . . . . . . . . . . 13
  toInc  Dirset
     |
22 | 21 | 3expb 1208 |
. . . . . . . . . . . 12
  toInc  Dirset    
   |
23 | 20, 22 | sylan2b 478 |
. . . . . . . . . . 11
  toInc  Dirset     
   |
24 | | sstr 3439 |
. . . . . . . . . . . . . . 15
 
  
  |
25 | 24 | ancoms 455 |
. . . . . . . . . . . . . 14
  
 
  |
26 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
    NoeACS 
       mrCls     
  mrCls       |
27 | 2 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . 21
   NoeACS       Moore    |
28 | | simprr 765 |
. . . . . . . . . . . . . . . . . . . . 21
   NoeACS         |
29 | 5 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
   NoeACS         |
30 | | simprl 763 |
. . . . . . . . . . . . . . . . . . . . . 22
   NoeACS         |
31 | 29, 30 | sseldd 3432 |
. . . . . . . . . . . . . . . . . . . . 21
   NoeACS         |
32 | 10 | mrcsscl 15519 |
. . . . . . . . . . . . . . . . . . . . 21
  Moore    mrCls       |
33 | 27, 28, 31, 32 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . 20
   NoeACS        mrCls       |
34 | 33 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
    NoeACS 
       mrCls     
 mrCls    
  |
35 | 26, 34 | eqsstrd 3465 |
. . . . . . . . . . . . . . . . . 18
    NoeACS 
       mrCls     
   |
36 | | simplrl 769 |
. . . . . . . . . . . . . . . . . . 19
    NoeACS 
       mrCls     
  |
37 | | elssuni 4226 |
. . . . . . . . . . . . . . . . . . 19
    |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    NoeACS 
       mrCls     
   |
39 | 35, 38 | eqssd 3448 |
. . . . . . . . . . . . . . . . 17
    NoeACS 
       mrCls     
   |
40 | 39, 36 | eqeltrd 2528 |
. . . . . . . . . . . . . . . 16
    NoeACS 
       mrCls     
   |
41 | 40 | ex 436 |
. . . . . . . . . . . . . . 15
   NoeACS        
 mrCls         |
42 | 41 | expr 619 |
. . . . . . . . . . . . . 14
   NoeACS   
     mrCls          |
43 | 25, 42 | syl5 33 |
. . . . . . . . . . . . 13
   NoeACS   
       
 mrCls          |
44 | 43 | expd 438 |
. . . . . . . . . . . 12
   NoeACS   
    
 
 mrCls    
      |
45 | 44 | rexlimdva 2878 |
. . . . . . . . . . 11
  NoeACS        
 
 mrCls    
      |
46 | 23, 45 | syl5 33 |
. . . . . . . . . 10
  NoeACS      toInc  Dirset          mrCls           |
47 | 46 | expdimp 439 |
. . . . . . . . 9
   NoeACS    toInc  Dirset
    
    mrCls           |
48 | 47 | rexlimdv 2876 |
. . . . . . . 8
   NoeACS    toInc  Dirset
 
      
 mrCls          |
49 | 19, 48 | syl5 33 |
. . . . . . 7
   NoeACS    toInc  Dirset
      
 mrCls          |
50 | 49 | rexlimdv 2876 |
. . . . . 6
   NoeACS    toInc  Dirset
 
     
 mrCls         |
51 | 16, 50 | mpd 15 |
. . . . 5
   NoeACS    toInc  Dirset
   |
52 | 51 | ex 436 |
. . . 4
  NoeACS     toInc  Dirset
    |
53 | 52 | ralrimiva 2801 |
. . 3
 NoeACS 
   toInc  Dirset     |
54 | 2, 53 | jca 535 |
. 2
 NoeACS 
 Moore     toInc  Dirset      |
55 | | simpl 459 |
. . . 4
  Moore  
  toInc  Dirset
  
Moore    |
56 | 5 | adantl 468 |
. . . . . . . 8
  Moore   
  |
57 | 56 | sseld 3430 |
. . . . . . 7
  Moore     
    |
58 | 57 | imim2d 54 |
. . . . . 6
  Moore      toInc  Dirset    toInc  Dirset      |
59 | 58 | ralimdva 2795 |
. . . . 5
 Moore 
 
  toInc  Dirset
     toInc  Dirset      |
60 | 59 | imp 431 |
. . . 4
  Moore  
  toInc  Dirset
   
  toInc  Dirset     |
61 | | isacs3 16413 |
. . . 4
 ACS   Moore     toInc  Dirset      |
62 | 55, 60, 61 | sylanbrc 669 |
. . 3
  Moore  
  toInc  Dirset
  
ACS    |
63 | 10 | mrcid 15512 |
. . . . . . . . . 10
  Moore    mrCls       |
64 | 63 | adantlr 720 |
. . . . . . . . 9
   Moore  
  toInc  Dirset
  
  mrCls       |
65 | 62 | adantr 467 |
. . . . . . . . . 10
   Moore  
  toInc  Dirset
  
 ACS    |
66 | | mress 15492 |
. . . . . . . . . . 11
  Moore     |
67 | 66 | adantlr 720 |
. . . . . . . . . 10
   Moore  
  toInc  Dirset
  

  |
68 | 65, 10, 67 | acsficld 16414 |
. . . . . . . . 9
   Moore  
  toInc  Dirset
  
  mrCls       mrCls     
    |
69 | 64, 68 | eqtr3d 2486 |
. . . . . . . 8
   Moore  
  toInc  Dirset
  
   mrCls          |
70 | 10 | mrcf 15508 |
. . . . . . . . . . . . 13
 Moore 
mrCls         |
71 | | ffn 5726 |
. . . . . . . . . . . . 13
 mrCls      
mrCls     |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
 Moore 
mrCls     |
73 | 72 | adantr 467 |
. . . . . . . . . . 11
  Moore   mrCls     |
74 | 10 | mrcss 15515 |
. . . . . . . . . . . . 13
  Moore    mrCls      mrCls       |
75 | 74 | 3expb 1208 |
. . . . . . . . . . . 12
  Moore  
   mrCls    
 mrCls       |
76 | 75 | adantlr 720 |
. . . . . . . . . . 11
   Moore   
   mrCls    
 mrCls       |
77 | | vex 3047 |
. . . . . . . . . . . 12
 |
78 | | fpwipodrs 16403 |
. . . . . . . . . . . 12
 toInc     Dirset |
79 | 77, 78 | mp1i 13 |
. . . . . . . . . . 11
  Moore   toInc     Dirset |
80 | | inss1 3651 |
. . . . . . . . . . . 12
     |
81 | | sspwb 4648 |
. . . . . . . . . . . . 13

    |
82 | 66, 81 | sylib 200 |
. . . . . . . . . . . 12
  Moore       |
83 | 80, 82 | syl5ss 3442 |
. . . . . . . . . . 11
  Moore    
    |
84 | | fvex 5873 |
. . . . . . . . . . . . 13
mrCls   |
85 | | imaexg 6727 |
. . . . . . . . . . . . 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 16404 |
. . . . . . . . . 10
  Moore   toInc  mrCls         Dirset |
89 | 88 | adantlr 720 |
. . . . . . . . 9
   Moore  
  toInc  Dirset
  
 toInc  mrCls     
   Dirset |
90 | | imassrn 5178 |
. . . . . . . . . . . . . 14
 mrCls     
 
mrCls   |
91 | | frn 5733 |
. . . . . . . . . . . . . . 15
 mrCls      
mrCls    |
92 | 70, 91 | syl 17 |
. . . . . . . . . . . . . 14
 Moore 
mrCls    |
93 | 90, 92 | syl5ss 3442 |
. . . . . . . . . . . . 13
 Moore 
 mrCls     
 
  |
94 | 93 | adantr 467 |
. . . . . . . . . . . 12
  Moore    mrCls          |
95 | 86 | elpw 3956 |
. . . . . . . . . . . 12
  mrCls        
 mrCls     
 
  |
96 | 94, 95 | sylibr 216 |
. . . . . . . . . . 11
  Moore    mrCls           |
97 | 96 | adantlr 720 |
. . . . . . . . . 10
   Moore  
  toInc  Dirset
  
  mrCls           |
98 | | simplr 761 |
. . . . . . . . . 10
   Moore  
  toInc  Dirset
  
    toInc  Dirset     |
99 | | fveq2 5863 |
. . . . . . . . . . . . 13
  mrCls     
 
toInc  toInc  mrCls           |
100 | 99 | eleq1d 2512 |
. . . . . . . . . . . 12
  mrCls     
 
 toInc  Dirset
toInc  mrCls         Dirset  |
101 | | unieq 4205 |
. . . . . . . . . . . . 13
  mrCls     
 
   mrCls     
    |
102 | | id 22 |
. . . . . . . . . . . . 13
  mrCls     
 
 mrCls          |
103 | 101, 102 | eleq12d 2522 |
. . . . . . . . . . . 12
  mrCls     
 
 
  mrCls         mrCls           |
104 | 100, 103 | imbi12d 322 |
. . . . . . . . . . 11
  mrCls     
 
  toInc  Dirset    toInc  mrCls         Dirset   mrCls     
   mrCls     
      |
105 | 104 | rspcva 3147 |
. . . . . . . . . 10
   mrCls            toInc  Dirset   
 toInc  mrCls         Dirset   mrCls         mrCls     
     |
106 | 97, 98, 105 | syl2anc 666 |
. . . . . . . . 9
   Moore  
  toInc  Dirset
  
  toInc  mrCls         Dirset   mrCls     
   mrCls     
     |
107 | 89, 106 | mpd 15 |
. . . . . . . 8
   Moore  
  toInc  Dirset
  
   mrCls     
   mrCls     
    |
108 | 69, 107 | eqeltrd 2528 |
. . . . . . 7
   Moore  
  toInc  Dirset
  
  mrCls     
    |
109 | | fvelimab 5919 |
. . . . . . . . 9
  mrCls    
     mrCls       
      mrCls        |
110 | 73, 83, 109 | syl2anc 666 |
. . . . . . . 8
  Moore     mrCls     
        mrCls        |
111 | 110 | adantlr 720 |
. . . . . . 7
   Moore  
  toInc  Dirset
  
   mrCls       
      mrCls        |
112 | 108, 111 | mpbid 214 |
. . . . . 6
   Moore  
  toInc  Dirset
  
       mrCls       |
113 | | eqcom 2457 |
. . . . . . 7
  mrCls      mrCls       |
114 | 113 | rexbii 2888 |
. . . . . 6
       mrCls           mrCls       |
115 | 112, 114 | sylibr 216 |
. . . . 5
   Moore  
  toInc  Dirset
  
       mrCls       |
116 | 10 | mrefg2 35543 |
. . . . . 6
 Moore 
 
     mrCls           mrCls        |
117 | 116 | ad2antrr 731 |
. . . . 5
   Moore  
  toInc  Dirset
  
        mrCls    
      mrCls        |
118 | 115, 117 | mpbird 236 |
. . . 4
   Moore  
  toInc  Dirset
  
       mrCls       |
119 | 118 | ralrimiva 2801 |
. . 3
  Moore  
  toInc  Dirset
   

 
   mrCls       |
120 | 10 | isnacs 35540 |
. . 3
 NoeACS   ACS   
 
   mrCls        |
121 | 62, 119, 120 | sylanbrc 669 |
. 2
  Moore  
  toInc  Dirset
  
NoeACS    |
122 | 54, 121 | impbii 191 |
1
 NoeACS   Moore     toInc  Dirset      |