Proof of Theorem fin23lem11
Step | Hyp | Ref
| Expression |
1 | | difeq2 3513 |
. . . . 5
       |
2 | 1 | eleq1d 2514 |
. . . 4
   
     |
3 | 2 | elrab 3164 |
. . 3
     
       |
4 | | simp2r 1036 |
. . . . 5
 
     
  
        |
5 | | difss 3528 |
. . . . . . . . . 10
   |
6 | | ssun1 3565 |
. . . . . . . . . . . . 13

  |
7 | | undif1 3810 |
. . . . . . . . . . . . 13
       |
8 | 6, 7 | sseqtr4i 3433 |
. . . . . . . . . . . 12
     |
9 | | simpl2r 1063 |
. . . . . . . . . . . . 13
         
           |
10 | | simpl2l 1062 |
. . . . . . . . . . . . 13
         
          |
11 | | unexg 6580 |
. . . . . . . . . . . . 13
   
 
      |
12 | 9, 10, 11 | syl2anc 671 |
. . . . . . . . . . . 12
         
             |
13 | | ssexg 4521 |
. . . . . . . . . . . 12
 
        
  |
14 | 8, 12, 13 | sylancr 674 |
. . . . . . . . . . 11
         
         |
15 | | elpw2g 4539 |
. . . . . . . . . . 11
          |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
         
                |
17 | 5, 16 | mpbiri 241 |
. . . . . . . . 9
         
            |
18 | | simpl1 1012 |
. . . . . . . . . . . . 13
         
          |
19 | | simpr 467 |
. . . . . . . . . . . . 13
         
         |
20 | 18, 19 | sseldd 3401 |
. . . . . . . . . . . 12
         
          |
21 | 20 | elpwid 3929 |
. . . . . . . . . . 11
         
         |
22 | | dfss4 3645 |
. . . . . . . . . . 11

      |
23 | 21, 22 | sylib 201 |
. . . . . . . . . 10
         
             |
24 | 23, 19 | eqeltrd 2530 |
. . . . . . . . 9
         
             |
25 | | difeq2 3513 |
. . . . . . . . . . 11
           |
26 | 25 | eleq1d 2514 |
. . . . . . . . . 10
     
       |
27 | 26 | elrab 3164 |
. . . . . . . . 9
       
           |
28 | 17, 24, 27 | sylanbrc 675 |
. . . . . . . 8
         
          
     |
29 | | simpl3 1014 |
. . . . . . . 8
         
         
     |
30 | | fin23lem11.2 |
. . . . . . . . . 10
       |
31 | 30 | notbid 300 |
. . . . . . . . 9
   
   |
32 | 31 | rspcva 3116 |
. . . . . . . 8
                  |
33 | 28, 29, 32 | syl2anc 671 |
. . . . . . 7
         
         |
34 | | simplrl 775 |
. . . . . . . . . . 11
         
    |
35 | 34 | elpwid 3929 |
. . . . . . . . . 10
         

  |
36 | | ssel2 3395 |
. . . . . . . . . . . 12
 


   |
37 | 36 | adantlr 726 |
. . . . . . . . . . 11
         
    |
38 | 37 | elpwid 3929 |
. . . . . . . . . 10
         

  |
39 | | fin23lem11.3 |
. . . . . . . . . 10
 
 
   |
40 | 35, 38, 39 | syl2anc 671 |
. . . . . . . . 9
         
 
   |
41 | 40 | notbid 300 |
. . . . . . . 8
         
 
   |
42 | 41 | 3adantl3 1167 |
. . . . . . 7
         
       
   |
43 | 33, 42 | mpbird 240 |
. . . . . 6
         
         |
44 | 43 | ralrimiva 2790 |
. . . . 5
 
     
  
    
  |
45 | | fin23lem11.1 |
. . . . . . . 8
       |
46 | 45 | notbid 300 |
. . . . . . 7
   
   |
47 | 46 | ralbidv 2810 |
. . . . . 6
    
    |
48 | 47 | rspcev 3118 |
. . . . 5
     


  |
49 | 4, 44, 48 | syl2anc 671 |
. . . 4
 
     
  
    

  |
50 | 49 | 3exp 1209 |
. . 3
       
 
      
    |
51 | 3, 50 | syl5bi 225 |
. 2
           
  


    |
52 | 51 | rexlimdv 2851 |
1
   
      
    


   |