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 15535 |
. . 3

  |
6 | | mreexmrid.6 |
. . . 4
   |
7 | 6 | snssd 4116 |
. . 3
     |
8 | 5, 7 | unssd 3609 |
. 2
       |
9 | 3 | 3ad2ant1 1028 |
. . . . . . . . . 10
 
            
Moore    |
10 | 9 | elfvexd 5891 |
. . . . . . . . 9
 
            
  |
11 | | mreexmrid.4 |
. . . . . . . . . 10
    
                         |
12 | 11 | 3ad2ant1 1028 |
. . . . . . . . 9
 
            
  
                          |
13 | 4 | 3ad2ant1 1028 |
. . . . . . . . . . 11
 
            
  |
14 | 2, 9, 13 | mrissd 15535 |
. . . . . . . . . 10
 
            
  |
15 | 14 | ssdifssd 3570 |
. . . . . . . . 9
 
            
      |
16 | 6 | 3ad2ant1 1028 |
. . . . . . . . 9
 
            
  |
17 | | simp3 1009 |
. . . . . . . . . 10
 
            
              |
18 | | difundir 3695 |
. . . . . . . . . . . 12
                     |
19 | | simp2 1008 |
. . . . . . . . . . . . . . . 16
 
            
  |
20 | 3, 1, 5 | mrcssidd 15524 |
. . . . . . . . . . . . . . . . . 18

      |
21 | | mreexmrid.7 |
. . . . . . . . . . . . . . . . . 18
       |
22 | 20, 21 | ssneldd 3434 |
. . . . . . . . . . . . . . . . 17
   |
23 | 22 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . 16
 
            
  |
24 | | nelneq 2552 |
. . . . . . . . . . . . . . . 16
 

  |
25 | 19, 23, 24 | syl2anc 666 |
. . . . . . . . . . . . . . 15
 
            
  |
26 | | elsni 3992 |
. . . . . . . . . . . . . . 15
     |
27 | 25, 26 | nsyl 125 |
. . . . . . . . . . . . . 14
 
            
    |
28 | | difsnb 4113 |
. . . . . . . . . . . . . 14
             |
29 | 27, 28 | sylib 200 |
. . . . . . . . . . . . 13
 
            
  
       |
30 | 29 | uneq2d 3587 |
. . . . . . . . . . . 12
 
            
                      |
31 | 18, 30 | syl5eq 2496 |
. . . . . . . . . . 11
 
            
 
                |
32 | 31 | fveq2d 5867 |
. . . . . . . . . 10
 
            
                          |
33 | 17, 32 | eleqtrd 2530 |
. . . . . . . . 9
 
            
              |
34 | 1, 2, 9, 13, 19 | ismri2dad 15536 |
. . . . . . . . 9
 
            
          |
35 | 10, 12, 15, 16, 33, 34 | mreexd 15541 |
. . . . . . . 8
 
            
              |
36 | 21 | 3ad2ant1 1028 |
. . . . . . . . 9
 
            
      |
37 | | undif1 3841 |
. . . . . . . . . . 11
             |
38 | 19 | snssd 4116 |
. . . . . . . . . . . 12
 
            
    |
39 | | ssequn2 3606 |
. . . . . . . . . . . 12
         |
40 | 38, 39 | sylib 200 |
. . . . . . . . . . 11
 
            
      |
41 | 37, 40 | syl5eq 2496 |
. . . . . . . . . 10
 
            
          |
42 | 41 | fveq2d 5867 |
. . . . . . . . 9
 
            
                  |
43 | 36, 42 | neleqtrrd 2550 |
. . . . . . . 8
 
            
              |
44 | 35, 43 | pm2.65i 177 |
. . . . . . 7

    
         |
45 | | df-3an 986 |
. . . . . . 7
 
                               |
46 | 44, 45 | mtbi 300 |
. . . . . 6
 
               |
47 | 46 | imnani 425 |
. . . . 5
 

              |
48 | 47 | adantlr 720 |
. . . 4
       
               |
49 | 26 | adantl 468 |
. . . . . 6
       
     |
50 | 21 | ad2antrr 731 |
. . . . . 6
       
  
      |
51 | 49, 50 | eqneltrd 2547 |
. . . . 5
       
  
      |
52 | 49 | sneqd 3979 |
. . . . . . . . 9
       
    
    |
53 | 52 | difeq2d 3550 |
. . . . . . . 8
       
                     |
54 | | difun2 3846 |
. . . . . . . 8
             |
55 | 53, 54 | syl6eq 2500 |
. . . . . . 7
       
                 |
56 | | difsnb 4113 |
. . . . . . . . 9

      |
57 | 22, 56 | sylib 200 |
. . . . . . . 8
       |
58 | 57 | ad2antrr 731 |
. . . . . . 7
       
         |
59 | 55, 58 | eqtrd 2484 |
. . . . . 6
       
             |
60 | 59 | fveq2d 5867 |
. . . . 5
       
       
             |
61 | 51, 60 | neleqtrrd 2550 |
. . . 4
       
  
              |
62 | | simpr 463 |
. . . . 5
 

   
      |
63 | | elun 3573 |
. . . . 5
    

     |
64 | 62, 63 | sylib 200 |
. . . 4
 

    
     |
65 | 48, 61, 64 | mpjaodan 794 |
. . 3
 

   
    
         |
66 | 65 | ralrimiva 2801 |
. 2
                    |
67 | 1, 2, 3, 8, 66 | ismri2dd 15533 |
1
       |