Step | Hyp | Ref
| Expression |
1 | | simplll 767 |
. . . . . . . . . . . 12
    FinII  

FinII |
2 | | ssrab2 3513 |
. . . . . . . . . . . . . . . . . . 19

    |
3 | | sstr 3439 |
. . . . . . . . . . . . . . . . . . 19
       
     |
4 | 2, 3 | mpan 675 |
. . . . . . . . . . . . . . . . . 18
 
     |
5 | | elpw2g 4565 |
. . . . . . . . . . . . . . . . . . 19
 FinII  
   
       |
6 | 5 | biimpar 488 |
. . . . . . . . . . . . . . . . . 18
 
FinII

    
      |
7 | 4, 6 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
 
FinII


      |
8 | 7 | ralrimivw 2802 |
. . . . . . . . . . . . . . . 16
 
FinII



      |
9 | | vex 3047 |
. . . . . . . . . . . . . . . . . . 19
 |
10 | 9 | rabex 4553 |
. . . . . . . . . . . . . . . . . 18

    |
11 | 10 | rgenw 2748 |
. . . . . . . . . . . . . . . . 17


    |
12 | | eqid 2450 |
. . . . . . . . . . . . . . . . . 18
 
           |
13 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . 18
               |
14 | 12, 13 | ralrnmpt 6029 |
. . . . . . . . . . . . . . . . 17
 
     
         
       |
15 | 11, 14 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 
 
              |
16 | 8, 15 | sylibr 216 |
. . . . . . . . . . . . . . 15
 
FinII

           |
17 | | dfss3 3421 |
. . . . . . . . . . . . . . 15
      
            |
18 | 16, 17 | sylibr 216 |
. . . . . . . . . . . . . 14
 
FinII

 
       |
19 | 18 | adantlr 720 |
. . . . . . . . . . . . 13
   FinII        
   |
20 | 19 | adantr 467 |
. . . . . . . . . . . 12
    FinII  

 
       |
21 | 10, 12 | dmmpti 5705 |
. . . . . . . . . . . . . . . 16
       |
22 | 21 | neeq1i 2687 |
. . . . . . . . . . . . . . 15
      
  |
23 | | dm0rn0 5050 |
. . . . . . . . . . . . . . . 16
      
 
      |
24 | 23 | necon3bii 2675 |
. . . . . . . . . . . . . . 15
      
 
      |
25 | 22, 24 | bitr3i 255 |
. . . . . . . . . . . . . 14
         |
26 | 25 | biimpi 198 |
. . . . . . . . . . . . 13

 
      |
27 | 26 | adantl 468 |
. . . . . . . . . . . 12
    FinII  

 
      |
28 | | soss 4772 |
. . . . . . . . . . . . . . . 16
 
   |
29 | 28 | impcom 432 |
. . . . . . . . . . . . . . 15
  
  |
30 | | porpss 6572 |
. . . . . . . . . . . . . . . . 17
[ ]        |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
 [ ]         |
32 | | solin 4777 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
          |
33 | | fin2solem 31924 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     
   [ ]        |
34 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
     |
35 | 34 | rabbidv 3035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   
     |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
   
          |
37 | | fin2solem 31924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
     
   [ ]        |
38 | 37 | ancom2s 810 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     
   [ ]        |
39 | 33, 36, 38 | 3orim123d 1346 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
        
     [ ]                 [ ] 
       |
40 | 32, 39 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
  
   
   [ ]                 [ ] 
      |
41 | 40 | ralrimivva 2808 |
. . . . . . . . . . . . . . . . . . . . 21
 

     [ ]                 [ ] 
      |
42 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      [ ]    

   [ ] 
      |
43 | | eqeq1 2454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  

   
      |
44 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
   [ ]
    [ ]        |
45 | 42, 43, 44 | 3orbi123d 1337 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       [ ] 
  

       [ ] 
     [ ]                 [ ] 
       |
46 | 45 | ralbidv 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
      

[ ] 
  

       [ ] 

     [ ]                 [ ] 
       |
47 | 12, 46 | ralrnmpt 6029 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
         [ ]             [ ]   
     [ ]                 [ ] 
       |
48 | 11, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
      
[ ] 
  

       [ ] 


     [ ]                 [ ] 
      |
49 | 41, 48 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . 20
         
 [ ]             [ ]    |
50 | 49 | r19.21bi 2756 |
. . . . . . . . . . . . . . . . . . 19
 
 
    

 [ ]             [ ]    |
51 | 9 | rabex 4553 |
. . . . . . . . . . . . . . . . . . . . 21

    |
52 | 51 | rgenw 2748 |
. . . . . . . . . . . . . . . . . . . 20


    |
53 | 35 | cbvmptv 4494 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
54 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . 22
      [ ]
[ ] 
      |
55 | | eqeq2 2461 |
. . . . . . . . . . . . . . . . . . . . . 22
     

      |
56 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . 22
      [ ]

   [ ]    |
57 | 54, 55, 56 | 3orbi123d 1337 |
. . . . . . . . . . . . . . . . . . . . 21
       [ ]
[ ]   [ ] 
  

       [ ]     |
58 | 53, 57 | ralrnmpt 6029 |
. . . . . . . . . . . . . . . . . . . 20
 
     
        [ ]
[ ]   
[ ] 
  

       [ ]     |
59 | 52, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 
 
      [ ]
[ ]  

[ ] 
  

       [ ]    |
60 | 50, 59 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
 
 
    
         [ ]
[ ]    |
61 | 60 | r19.21bi 2756 |
. . . . . . . . . . . . . . . . 17
  
               [ ]
[ ]    |
62 | 61 | anasss 652 |
. . . . . . . . . . . . . . . 16
  
             
 [ ] [ ]    |
63 | 31, 62 | issod 4784 |
. . . . . . . . . . . . . . 15
 [ ]         |
64 | 29, 63 | syl 17 |
. . . . . . . . . . . . . 14
   [ ]


      |
65 | 64 | adantll 719 |
. . . . . . . . . . . . 13
   FinII   [ ]         |
66 | 65 | adantr 467 |
. . . . . . . . . . . 12
    FinII  

[ ]         |
67 | | fin2i2 8745 |
. . . . . . . . . . . 12
   FinII      
 
       [ ]                        |
68 | 1, 20, 27, 66, 67 | syl22anc 1268 |
. . . . . . . . . . 11
    FinII  

               |
69 | 53, 51 | elrnmpti 5084 |
. . . . . . . . . . 11
                            |
70 | 68, 69 | sylib 200 |
. . . . . . . . . 10
    FinII  


       
     |
71 | | ssel2 3426 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
72 | | sonr 4775 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
73 | 71, 72 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
  
 
    |
74 | 73 | anassrs 653 |
. . . . . . . . . . . . . . . . . 18
  
 
    |
75 | 74 | adantlr 720 |
. . . . . . . . . . . . . . . . 17
    
      |
76 | 75 | adantr 467 |
. . . . . . . . . . . . . . . 16
               
   
    |
77 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
78 | 77 | elrab 3195 |
. . . . . . . . . . . . . . . . . . . 20
    

     |
79 | 78 | simplbi2 630 |
. . . . . . . . . . . . . . . . . . 19
    
      |
80 | 79 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . 18
  

       
      
       |
81 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
82 | 81 | elint2 4240 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
         |
83 | | eleq2 2517 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
84 | 12, 83 | ralrnmpt 6029 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
       

      |
85 | 11, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
    

      |
86 | 82, 85 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . 21
   
    

     |
87 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
     |
88 | 87 | rabbidv 3035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   
     |
89 | 88 | eleq2d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
  
       |
90 | 89 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

          |
91 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
     |
92 | 91 | elrab 3195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

     |
93 | 92 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
94 | 90, 93 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . 22
  

        |
95 | 94 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
            |
96 | 86, 95 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . 20
 
        
     |
97 | | eleq2 2517 |
. . . . . . . . . . . . . . . . . . . . 21
        
                  |
98 | 97 | imbi1d 319 |
. . . . . . . . . . . . . . . . . . . 20
        
           
  
           |
99 | 96, 98 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . 19
 
         
    
         |
100 | 99 | imp 431 |
. . . . . . . . . . . . . . . . . 18
  

       
              |
101 | 80, 100 | syld 45 |
. . . . . . . . . . . . . . . . 17
  

       
      
     |
102 | 101 | adantlll 723 |
. . . . . . . . . . . . . . . 16
               
      
     |
103 | 76, 102 | mtod 181 |
. . . . . . . . . . . . . . 15
               
   
    |
104 | 103 | ex 436 |
. . . . . . . . . . . . . 14
    
             
     |
105 | 104 | ralrimdva 2805 |
. . . . . . . . . . . . 13
  
 
        
         |
106 | 105 | reximdva 2861 |
. . . . . . . . . . . 12
            
    
     |
107 | 106 | adantll 719 |
. . . . . . . . . . 11
   FinII    
            
     |
108 | 107 | adantr 467 |
. . . . . . . . . 10
    FinII  

 
       
    
     |
109 | 70, 108 | mpd 15 |
. . . . . . . . 9
    FinII  



    |
110 | 109 | expl 623 |
. . . . . . . 8
 
FinII
  
 

     |
111 | 110 | alrimiv 1772 |
. . . . . . 7
 
FinII
      

     |
112 | | df-fr 4792 |
. . . . . . 7

     

     |
113 | 111, 112 | sylibr 216 |
. . . . . 6
 
FinII
   |
114 | | simpr 463 |
. . . . . 6
 
FinII
   |
115 | | df-we 4794 |
. . . . . 6


   |
116 | 113, 114,
115 | sylanbrc 669 |
. . . . 5
 
FinII
   |
117 | | weinxp 4901 |
. . . . 5

      |
118 | 116, 117 | sylib 200 |
. . . 4
 
FinII
       |
119 | | sqxpexg 6593 |
. . . . . 6
 FinII     |
120 | | incom 3624 |
. . . . . . 7
         |
121 | | inex1g 4545 |
. . . . . . 7
     
   |
122 | 120, 121 | syl5eqel 2532 |
. . . . . 6
         |
123 | | weeq1 4821 |
. . . . . . 7
  
  
       |
124 | 123 | spcegv 3134 |
. . . . . 6
              |
125 | 119, 122,
124 | 3syl 18 |
. . . . 5
 FinII     
    |
126 | 125 | imp 431 |
. . . 4
 
FinII
    
   |
127 | 118, 126 | syldan 473 |
. . 3
 
FinII
    |
128 | | ween 8463 |
. . 3

   |
129 | 127, 128 | sylibr 216 |
. 2
 
FinII
   |
130 | | fin23 8816 |
. . . . 5
 FinII FinIII |
131 | | fin34 8817 |
. . . . 5
 FinIII FinIV |
132 | | fin45 8819 |
. . . . 5
 FinIV FinV |
133 | 130, 131,
132 | 3syl 18 |
. . . 4
 FinII FinV |
134 | | fin56 8820 |
. . . 4
 FinV FinVI |
135 | | fin67 8822 |
. . . 4
 FinVI FinVII |
136 | 133, 134,
135 | 3syl 18 |
. . 3
 FinII FinVII |
137 | | fin71num 8824 |
. . . 4
 
FinVII    |
138 | 137 | biimpac 489 |
. . 3
 
FinVII
   |
139 | 136, 138 | sylan 474 |
. 2
 
FinII
   |
140 | 129, 139 | syldan 473 |
1
 
FinII
   |