Step | Hyp | Ref
| Expression |
1 | | simpr 467 |
. . 3
    
[ ]   
    FinII   FinII |
2 | | simpll1 1053 |
. . . 4
    
[ ]   
    FinII    |
3 | | ssel2 3439 |
. . . . . . . . . 10
 


   |
4 | 3 | elpwid 3973 |
. . . . . . . . 9
 


  |
5 | 4 | ssdifd 3581 |
. . . . . . . 8
 


      |
6 | | sseq1 3465 |
. . . . . . . 8
   
 
       |
7 | 5, 6 | syl5ibrcom 230 |
. . . . . . 7
 


        |
8 | 7 | rexlimdva 2891 |
. . . . . 6
   
       |
9 | | vex 3060 |
. . . . . . 7
 |
10 | | eqid 2462 |
. . . . . . . 8
         |
11 | 10 | elrnmpt 5100 |
. . . . . . 7
      
     |
12 | 9, 11 | ax-mp 5 |
. . . . . 6
     
    |
13 | | selpw 3970 |
. . . . . 6
   

   |
14 | 8, 12, 13 | 3imtr4g 278 |
. . . . 5
      
      |
15 | 14 | ssrdv 3450 |
. . . 4
       
   |
16 | 2, 15 | syl 17 |
. . 3
    
[ ]   
    FinII

        |
17 | | simplrr 776 |
. . . 4
    
[ ]   
    FinII   |
18 | | difid 3847 |
. . . . . . 7
   |
19 | 18 | eqcomi 2471 |
. . . . . 6
   |
20 | | difeq1 3556 |
. . . . . . . 8
 
     |
21 | 20 | eqeq2d 2472 |
. . . . . . 7
   
     |
22 | 21 | rspcev 3162 |
. . . . . 6
     
    |
23 | 19, 22 | mpan2 682 |
. . . . 5
 
    |
24 | | 0ex 4549 |
. . . . . 6
 |
25 | 10 | elrnmpt 5100 |
. . . . . 6

    

     |
26 | 24, 25 | ax-mp 5 |
. . . . 5
    

    |
27 | 23, 26 | sylibr 217 |
. . . 4
       |
28 | | ne0i 3749 |
. . . 4
           |
29 | 17, 27, 28 | 3syl 18 |
. . 3
    
[ ]   
    FinII

     |
30 | | simpll2 1054 |
. . . 4
    
[ ]   
    FinII [ ]   |
31 | | vex 3060 |
. . . . . . . 8
 |
32 | 10 | elrnmpt 5100 |
. . . . . . . 8
      
     |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
     
    |
34 | | difeq1 3556 |
. . . . . . . . . 10
 
     |
35 | 34 | eqeq2d 2472 |
. . . . . . . . 9
   
     |
36 | 35 | cbvrexv 3032 |
. . . . . . . 8
   

    |
37 | | sorpssi 6604 |
. . . . . . . . . . . . . . . 16
 [ ] 
 
    |
38 | | ssdif 3580 |
. . . . . . . . . . . . . . . . 17
 
     |
39 | | ssdif 3580 |
. . . . . . . . . . . . . . . . 17
 
     |
40 | 38, 39 | orim12i 523 |
. . . . . . . . . . . . . . . 16
 
    
  
     |
41 | 37, 40 | syl 17 |
. . . . . . . . . . . . . . 15
 [ ] 
 
 
          |
42 | | sseq2 3466 |
. . . . . . . . . . . . . . . 16
     
  
    |
43 | | sseq1 3465 |
. . . . . . . . . . . . . . . 16
   
 
  
    |
44 | 42, 43 | orbi12d 721 |
. . . . . . . . . . . . . . 15
      
      
  
      |
45 | 41, 44 | syl5ibrcom 230 |
. . . . . . . . . . . . . 14
 [ ] 
 
     
      |
46 | 45 | expr 624 |
. . . . . . . . . . . . 13
 [ ]        
       |
47 | 46 | rexlimdv 2889 |
. . . . . . . . . . . 12
 [ ]   
    
      |
48 | 12, 47 | syl5bi 225 |
. . . . . . . . . . 11
 [ ]      
 
       |
49 | 48 | ralrimiv 2812 |
. . . . . . . . . 10
 [ ]          
     |
50 | | sseq1 3465 |
. . . . . . . . . . . 12
   
     |
51 | | sseq2 3466 |
. . . . . . . . . . . 12
   
     |
52 | 50, 51 | orbi12d 721 |
. . . . . . . . . . 11
    
   
      |
53 | 52 | ralbidv 2839 |
. . . . . . . . . 10
    
      
        
      |
54 | 49, 53 | syl5ibrcom 230 |
. . . . . . . . 9
 [ ]     
          |
55 | 54 | rexlimdva 2891 |
. . . . . . . 8
[ ]
          
    |
56 | 36, 55 | syl5bi 225 |
. . . . . . 7
[ ]
          
    |
57 | 33, 56 | syl5bi 225 |
. . . . . 6
[ ]
                |
58 | 57 | ralrimiv 2812 |
. . . . 5
[ ]
      
     
   |
59 | | sorpss 6603 |
. . . . 5
[ ]    
      
     
   |
60 | 58, 59 | sylibr 217 |
. . . 4
[ ]
[ ]       |
61 | 30, 60 | syl 17 |
. . 3
    
[ ]   
    FinII [ ]       |
62 | | fin2i 8751 |
. . 3
     FinII      
       [ ]                  |
63 | 1, 16, 29, 61, 62 | syl22anc 1277 |
. 2
    
[ ]   
    FinII            |
64 | | simpll3 1055 |
. . 3
    
[ ]   
    FinII
   |
65 | | difeq1 3556 |
. . . . . . 7
 
     |
66 | 65 | cbvmptv 4509 |
. . . . . 6
         |
67 | 66 | elrnmpt 5100 |
. . . . 5
                   

          |
68 | 67 | ibi 249 |
. . . 4
          
         |
69 | | eqid 2462 |
. . . . . . . . . . . . . . . 16
     |
70 | | difeq1 3556 |
. . . . . . . . . . . . . . . . . 18
 
     |
71 | 70 | eqeq2d 2472 |
. . . . . . . . . . . . . . . . 17
     
       |
72 | 71 | rspcev 3162 |
. . . . . . . . . . . . . . . 16
  
    

     |
73 | 69, 72 | mpan2 682 |
. . . . . . . . . . . . . . 15
 
      |
74 | 73 | adantl 472 |
. . . . . . . . . . . . . 14
          
  
     |
75 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
76 | | difexg 4565 |
. . . . . . . . . . . . . . 15
 
   |
77 | 10 | elrnmpt 5100 |
. . . . . . . . . . . . . . 15
           
      |
78 | 75, 76, 77 | mp2b 10 |
. . . . . . . . . . . . . 14
       

     |
79 | 74, 78 | sylibr 217 |
. . . . . . . . . . . . 13
          
         |
80 | | elssuni 4241 |
. . . . . . . . . . . . 13
                |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
          
  
       |
82 | | simplr 767 |
. . . . . . . . . . . 12
          
          |
83 | 81, 82 | sseqtrd 3480 |
. . . . . . . . . . 11
          
  
    |
84 | 83 | adantll 725 |
. . . . . . . . . 10
     
 [ ]  

  
 FinII            
     |
85 | | unss2 3617 |
. . . . . . . . . . 11
     
   

    |
86 | | uncom 3590 |
. . . . . . . . . . . . . . 15
         |
87 | | undif1 3854 |
. . . . . . . . . . . . . . 15
       |
88 | 86, 87 | eqtri 2484 |
. . . . . . . . . . . . . 14
       |
89 | 88 | a1i 11 |
. . . . . . . . . . . . 13
     
 [ ]  

  
 FinII            
       |
90 | 64 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
     
 [ ]  

  
 FinII               |
91 | 17 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
     
 [ ]  

  
 FinII              |
92 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
     
 [ ]  

  
 FinII                     |
93 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
94 | | difeq1 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     |
95 | 94 | eqeq2d 2472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
       |
96 | 95 | rspcev 3162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
    

     |
97 | 93, 96 | mpan2 682 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
      |
98 | | difexg 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
99 | 10 | elrnmpt 5100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
      |
100 | 31, 98, 99 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       

     |
101 | 97, 100 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
102 | 101 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
       |
103 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       |
104 | | ssdif0 3835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    |
105 | 104 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
106 | 105 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
   |
107 | 103, 106 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
108 | | uni0c 4238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
       |
109 | 107, 108 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                      |
110 | | eqeq1 2466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
     |
111 | 110 | rspcva 3160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
   |
112 | 102, 109,
111 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
   |
113 | | ssdif0 3835 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
114 | 112, 113 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
115 | 114 | ralrimiva 2814 |
. . . . . . . . . . . . . . . . . . . . 21
            
  |
116 | | unissb 4243 |
. . . . . . . . . . . . . . . . . . . . 21
 

  |
117 | 115, 116 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . 20
            
  |
118 | | elssuni 4241 |
. . . . . . . . . . . . . . . . . . . . 21
    |
119 | 118 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
               |
120 | 117, 119 | eqssd 3461 |
. . . . . . . . . . . . . . . . . . 19
            
  |
121 | | simpll 765 |
. . . . . . . . . . . . . . . . . . 19
           
  |
122 | 120, 121 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . 18
            
  |
123 | 122 | ex 440 |
. . . . . . . . . . . . . . . . 17
          
    |
124 | 91, 92, 123 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
     
 [ ]  

  
 FinII            
    |
125 | 90, 124 | mtod 182 |
. . . . . . . . . . . . . . 15
     
 [ ]  

  
 FinII              |
126 | 30 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
     
 [ ]  

  
 FinII            [ ]   |
127 | | simplrl 775 |
. . . . . . . . . . . . . . . 16
     
 [ ]  

  
 FinII              |
128 | | sorpssi 6604 |
. . . . . . . . . . . . . . . 16
 [ ] 
 
    |
129 | 126, 127,
91, 128 | syl12anc 1274 |
. . . . . . . . . . . . . . 15
     
 [ ]  

  
 FinII            
   |
130 | | orel1 388 |
. . . . . . . . . . . . . . 15

 
    |
131 | 125, 129,
130 | sylc 62 |
. . . . . . . . . . . . . 14
     
 [ ]  

  
 FinII              |
132 | | undif 3860 |
. . . . . . . . . . . . . 14

      |
133 | 131, 132 | sylib 201 |
. . . . . . . . . . . . 13
     
 [ ]  

  
 FinII            
     |
134 | 89, 133 | sseq12d 3473 |
. . . . . . . . . . . 12
     
 [ ]  

  
 FinII              
 
   
     |
135 | | ssun1 3609 |
. . . . . . . . . . . . 13

  |
136 | | sstr 3452 |
. . . . . . . . . . . . 13
 
       |
137 | 135, 136 | mpan 681 |
. . . . . . . . . . . 12
     |
138 | 134, 137 | syl6bi 236 |
. . . . . . . . . . 11
     
 [ ]  

  
 FinII              
 
       |
139 | 85, 138 | syl5 33 |
. . . . . . . . . 10
     
 [ ]  

  
 FinII              
     |
140 | 84, 139 | mpd 15 |
. . . . . . . . 9
     
 [ ]  

  
 FinII              |
141 | 140 | ralrimiva 2814 |
. . . . . . . 8
      [ ]   
    FinII           
  |
142 | | unissb 4243 |
. . . . . . . 8
 

  |
143 | 141, 142 | sylibr 217 |
. . . . . . 7
      [ ]   
    FinII              |
144 | | elssuni 4241 |
. . . . . . . 8
    |
145 | 144 | ad2antrl 739 |
. . . . . . 7
      [ ]   
    FinII              |
146 | 143, 145 | eqssd 3461 |
. . . . . 6
      [ ]   
    FinII              |
147 | | simprl 769 |
. . . . . 6
      [ ]   
    FinII             |
148 | 146, 147 | eqeltrd 2540 |
. . . . 5
      [ ]   
    FinII              |
149 | 148 | rexlimdvaa 2892 |
. . . 4
    
[ ]   
    FinII  
       
   |
150 | 68, 149 | syl5 33 |
. . 3
    
[ ]   
    FinII               |
151 | 64, 150 | mtod 182 |
. 2
    
[ ]   
    FinII
           |
152 | 63, 151 | pm2.65da 584 |
1
    [ ]
  
 
  FinII |