Proof of Theorem mreexexlem2d
Step | Hyp | Ref
| Expression |
1 | | mreexexlem2d.7 |
. . . . . . . 8

        |
2 | 1 | adantr 472 |
. . . . . . 7
 
    
         
    |
3 | | mreexexlem2d.1 |
. . . . . . . . . 10
 Moore    |
4 | 3 | adantr 472 |
. . . . . . . . 9
 
    
      Moore    |
5 | | mreexexlem2d.2 |
. . . . . . . . 9
mrCls   |
6 | | simpr 468 |
. . . . . . . . . 10
 
    
           
      |
7 | | ssun2 3589 |
. . . . . . . . . . . . 13
       |
8 | | difundir 3687 |
. . . . . . . . . . . . . 14
                 |
9 | | mreexexlem2d.9 |
. . . . . . . . . . . . . . . . 17
   |
10 | | incom 3616 |
. . . . . . . . . . . . . . . . . 18
     |
11 | | mreexexlem2d.5 |
. . . . . . . . . . . . . . . . . . 19

    |
12 | | ssdifin0 3840 |
. . . . . . . . . . . . . . . . . . 19
       |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
14 | 10, 13 | syl5eqr 2519 |
. . . . . . . . . . . . . . . . 17
     |
15 | | minel 3824 |
. . . . . . . . . . . . . . . . 17
  
 
  |
16 | 9, 14, 15 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
   |
17 | | difsnb 4105 |
. . . . . . . . . . . . . . . 16

      |
18 | 16, 17 | sylib 201 |
. . . . . . . . . . . . . . 15
       |
19 | 18 | uneq2d 3579 |
. . . . . . . . . . . . . 14
                   |
20 | 8, 19 | syl5eq 2517 |
. . . . . . . . . . . . 13
               |
21 | 7, 20 | syl5sseqr 3467 |
. . . . . . . . . . . 12

 
      |
22 | | mreexexlem2d.3 |
. . . . . . . . . . . . . . 15
mrInd   |
23 | | mreexexlem2d.8 |
. . . . . . . . . . . . . . 15
     |
24 | 22, 3, 23 | mrissd 15620 |
. . . . . . . . . . . . . 14
  
  |
25 | 24 | ssdifssd 3560 |
. . . . . . . . . . . . 13
         |
26 | 3, 5, 25 | mrcssidd 15609 |
. . . . . . . . . . . 12
           
       |
27 | 21, 26 | sstrd 3428 |
. . . . . . . . . . 11

            |
28 | 27 | adantr 472 |
. . . . . . . . . 10
 
    
           
      |
29 | 6, 28 | unssd 3601 |
. . . . . . . . 9
 
    
      
      
      |
30 | 4, 5 | mrcssvd 15607 |
. . . . . . . . 9
 
    
          
    
  |
31 | 4, 5, 29, 30 | mrcssd 15608 |
. . . . . . . 8
 
    
                            |
32 | 25 | adantr 472 |
. . . . . . . . 9
 
    
        
     |
33 | 4, 5, 32 | mrcidmd 15610 |
. . . . . . . 8
 
    
                                |
34 | 31, 33 | sseqtrd 3454 |
. . . . . . 7
 
    
                        |
35 | 2, 34 | sstrd 3428 |
. . . . . 6
 
    
           
      |
36 | 9 | adantr 472 |
. . . . . 6
 
    
        |
37 | 35, 36 | sseldd 3419 |
. . . . 5
 
    
           
      |
38 | 23 | adantr 472 |
. . . . . 6
 
    
      
   |
39 | | ssun1 3588 |
. . . . . . 7

  |
40 | 39, 36 | sseldi 3416 |
. . . . . 6
 
    
          |
41 | 5, 22, 4, 38, 40 | ismri2dad 15621 |
. . . . 5
 
    
     
            |
42 | 37, 41 | pm2.65da 586 |
. . . 4
     
       |
43 | | nss 3476 |
. . . 4

         
                |
44 | 42, 43 | sylib 201 |
. . 3
   
             |
45 | | simprl 772 |
. . . . . 6
 

     
     
  |
46 | | ssun1 3588 |
. . . . . . . . . 10
   
       |
47 | 46, 20 | syl5sseqr 3467 |
. . . . . . . . 9
       
     |
48 | 47, 26 | sstrd 3428 |
. . . . . . . 8
         
       |
49 | 48 | adantr 472 |
. . . . . . 7
 

     
     
                |
50 | | simprr 774 |
. . . . . . 7
 

     
     
     
      |
51 | 49, 50 | ssneldd 3421 |
. . . . . 6
 

     
     
      |
52 | | unass 3582 |
. . . . . . 7
               
     |
53 | 3 | adantr 472 |
. . . . . . . 8
 

     
     
Moore    |
54 | | mreexexlem2d.4 |
. . . . . . . . 9
    
                         |
55 | 54 | adantr 472 |
. . . . . . . 8
 

     
     
  
                          |
56 | 23 | adantr 472 |
. . . . . . . . 9
 

     
     
    |
57 | | difss 3549 |
. . . . . . . . . 10
   
 |
58 | | unss1 3594 |
. . . . . . . . . 10
           
   |
59 | 57, 58 | mp1i 13 |
. . . . . . . . 9
 

     
     
          |
60 | 53, 5, 22, 56, 59 | mrissmrid 15625 |
. . . . . . . 8
 

     
     
        |
61 | | mreexexlem2d.6 |
. . . . . . . . . . 11

    |
62 | 61 | adantr 472 |
. . . . . . . . . 10
 

     
     
    |
63 | 62 | difss2d 3552 |
. . . . . . . . 9
 

     
     
  |
64 | 63, 45 | sseldd 3419 |
. . . . . . . 8
 

     
     
  |
65 | 20 | adantr 472 |
. . . . . . . . . 10
 

     
     
 
            |
66 | 65 | fveq2d 5883 |
. . . . . . . . 9
 

     
     
                      |
67 | 50, 66 | neleqtrd 2570 |
. . . . . . . 8
 

     
     
            |
68 | 53, 5, 22, 55, 60, 64, 67 | mreexmrid 15627 |
. . . . . . 7
 

     
     
            |
69 | 52, 68 | syl5eqelr 2554 |
. . . . . 6
 

     
     
            |
70 | 45, 51, 69 | jca32 544 |
. . . . 5
 

     
     


   
              |
71 | 70 | ex 441 |
. . . 4
        
          
               |
72 | 71 | eximdv 1772 |
. . 3
    
    
                   
         |
73 | 44, 72 | mpd 15 |
. 2
    
   
              |
74 | | df-rex 2762 |
. 2
            
    
             
        |
75 | 73, 74 | sylibr 217 |
1
  

        
       |