Step | Hyp | Ref
| Expression |
1 | | simp3 990 |
. 2
            
       
 
   |
2 | | fvelrnb 5849 |
. . . . . 6
          |
3 | | fvelrnb 5849 |
. . . . . 6
          |
4 | 2, 3 | anbi12d 710 |
. . . . 5
                   |
5 | 4 | 3ad2ant1 1009 |
. . . 4
            
       
 
                   |
6 | | reeanv 2994 |
. . . . 5
  
         
 
   
        |
7 | | nnord 6595 |
. . . . . . . . . . 11
   |
8 | | nnord 6595 |
. . . . . . . . . . 11
   |
9 | | ordtri2or2 4924 |
. . . . . . . . . . 11
   
   |
10 | 7, 8, 9 | syl2an 477 |
. . . . . . . . . 10
 
 
   |
11 | 10 | adantl 466 |
. . . . . . . . 9
                       
 
  
   |
12 | | vex 3081 |
. . . . . . . . . . 11
 |
13 | | vex 3081 |
. . . . . . . . . . 11
 |
14 | | eleq1 2526 |
. . . . . . . . . . . . . 14
 
   |
15 | | eleq1 2526 |
. . . . . . . . . . . . . 14
 
   |
16 | 14, 15 | bi2anan9 868 |
. . . . . . . . . . . . 13
 
  
 
    |
17 | 16 | anbi2d 703 |
. . . . . . . . . . . 12
 
    
         
       
 
 
    
         
       
 
 
     |
18 | | sseq12 3488 |
. . . . . . . . . . . . 13
 
     |
19 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
           |
20 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
           |
21 | 19, 20 | breqan12d 4416 |
. . . . . . . . . . . . . 14
 
                         |
22 | 19, 20 | eqeqan12d 2477 |
. . . . . . . . . . . . . 14
 
                     |
23 | 21, 22 | orbi12d 709 |
. . . . . . . . . . . . 13
 
                     
                       |
24 | 18, 23 | imbi12d 320 |
. . . . . . . . . . . 12
 
                       

                        |
25 | 17, 24 | imbi12d 320 |
. . . . . . . . . . 11
 
               
       
 
 
 

                                   
       
 
 
 

                         |
26 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . 18
           |
27 | 26 | breq2d 4413 |
. . . . . . . . . . . . . . . . 17
           
             |
28 | 26 | eqeq2d 2468 |
. . . . . . . . . . . . . . . . 17
         
           |
29 | 27, 28 | orbi12d 709 |
. . . . . . . . . . . . . . . 16
                                             |
30 | 29 | imbi2d 316 |
. . . . . . . . . . . . . . 15
                        
                     
 

         
       
 
                         |
31 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . 18
           |
32 | 31 | breq2d 4413 |
. . . . . . . . . . . . . . . . 17
           
             |
33 | 31 | eqeq2d 2468 |
. . . . . . . . . . . . . . . . 17
         
           |
34 | 32, 33 | orbi12d 709 |
. . . . . . . . . . . . . . . 16
                                             |
35 | 34 | imbi2d 316 |
. . . . . . . . . . . . . . 15
                        
                     
 

         
       
 
                         |
36 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . 18
       
   |
37 | 36 | breq2d 4413 |
. . . . . . . . . . . . . . . . 17
                    
    |
38 | 36 | eqeq2d 2468 |
. . . . . . . . . . . . . . . . 17
                
    |
39 | 37, 38 | orbi12d 709 |
. . . . . . . . . . . . . . . 16
                     
                       |
40 | 39 | imbi2d 316 |
. . . . . . . . . . . . . . 15
    
         
       
 
                        
         
       
 
          
       
      |
41 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . 18
           |
42 | 41 | breq2d 4413 |
. . . . . . . . . . . . . . . . 17
           
             |
43 | 41 | eqeq2d 2468 |
. . . . . . . . . . . . . . . . 17
         
           |
44 | 42, 43 | orbi12d 709 |
. . . . . . . . . . . . . . . 16
                                             |
45 | 44 | imbi2d 316 |
. . . . . . . . . . . . . . 15
                        
                     
 

         
       
 
                         |
46 | | eqid 2454 |
. . . . . . . . . . . . . . . . 17
         |
47 | 46 | olci 391 |
. . . . . . . . . . . . . . . 16
                     |
48 | 47 | a1ii 27 |
. . . . . . . . . . . . . . 15
                       
                        |
49 | | simplll 757 |
. . . . . . . . . . . . . . . . . . 19
   
  

         
       
 
    |
50 | | simpr2 995 |
. . . . . . . . . . . . . . . . . . 19
   
  

         
       
 
  
                      |
51 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
52 | | suceq 4893 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
53 | 52 | fveq2d 5804 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
54 | 51, 53 | breq12d 4414 |
. . . . . . . . . . . . . . . . . . . . 21
          
              |
55 | 51, 53 | eqeq12d 2476 |
. . . . . . . . . . . . . . . . . . . . 21
        
            |
56 | 54, 55 | orbi12d 709 |
. . . . . . . . . . . . . . . . . . . 20
                     
                       |
57 | 56 | rspcva 3177 |
. . . . . . . . . . . . . . . . . . 19
            
       
            
       
    |
58 | 49, 50, 57 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
   
  

         
       
 
                        |
59 | | simprr 756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  
    |
60 | | simprl 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  
    |
61 | | simpllr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  
    |
62 | | fnfvelrn 5950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       |
63 | 60, 61, 62 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  
        |
64 | | simplll 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  
    |
65 | | fnfvelrn 5950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       |
66 | 60, 64, 65 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  
        |
67 | | peano2 6607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
68 | 67 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
  
 
  |
69 | | fnfvelrn 5950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       |
70 | 60, 68, 69 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  
        |
71 | | potr 4762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                     |
72 | 59, 63, 66, 70, 71 | syl13anc 1221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
  
                                 
    |
73 | 72 | imp 429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
            
                    
   |
74 | 73 | ancom2s 800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
                                     |
75 | 74 | orcd 392 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                               |
76 | 75 | expr 615 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                                               |
77 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  
              |
78 | 77 | biimprcd 225 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                            
    |
79 | | orc 385 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                    
       
    |
80 | 78, 79 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           |
81 | 80 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                                             |
82 | 76, 81 | jaod 380 |
. . . . . . . . . . . . . . . . . . . . 21
       
                                 
                       |
83 | 82 | ex 434 |
. . . . . . . . . . . . . . . . . . . 20
   
  
                                 
                        |
84 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
             |
85 | | eqeq2 2469 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 
           |
86 | 84, 85 | orbi12d 709 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                     |
87 | 86 | biimpd 207 |
. . . . . . . . . . . . . . . . . . . . 21
                             
                       |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   
  
                               
                        |
89 | 83, 88 | jaod 380 |
. . . . . . . . . . . . . . . . . . 19
   
  
                                                     
       
      |
90 | 89 | 3adantr2 1148 |
. . . . . . . . . . . . . . . . . 18
   
  

         
       
 
                                                     
       
      |
91 | 58, 90 | mpd 15 |
. . . . . . . . . . . . . . . . 17
   
  

         
       
 
                                
       
     |
92 | 91 | ex 434 |
. . . . . . . . . . . . . . . 16
   
   
         
       
 
                     
                        |
93 | 92 | a2d 26 |
. . . . . . . . . . . . . . 15
   
              
       
 
                     
 

         
       
 
          
       
      |
94 | 30, 35, 40, 45, 48, 93 | findsg 6614 |
. . . . . . . . . . . . . 14
   
   
         
       
 
                        |
95 | 94 | ancom1s 803 |
. . . . . . . . . . . . 13
   
   
         
       
 
                        |
96 | 95 | impcom 430 |
. . . . . . . . . . . 12
                       
                            |
97 | 96 | expr 615 |
. . . . . . . . . . 11
                       
 
  
                       |
98 | 12, 13, 25, 97 | vtocl2 3131 |
. . . . . . . . . 10
                       
 
  
                       |
99 | | eleq1 2526 |
. . . . . . . . . . . . . . 15
 
   |
100 | | eleq1 2526 |
. . . . . . . . . . . . . . 15
 
   |
101 | 99, 100 | bi2anan9 868 |
. . . . . . . . . . . . . 14
 
  
 
    |
102 | 101 | anbi2d 703 |
. . . . . . . . . . . . 13
 
    
         
       
 
 
    
         
       
 
 
     |
103 | | sseq12 3488 |
. . . . . . . . . . . . . 14
 
     |
104 | | fveq2 5800 |
. . . . . . . . . . . . . . . 16
           |
105 | | fveq2 5800 |
. . . . . . . . . . . . . . . 16
           |
106 | 104, 105 | breqan12d 4416 |
. . . . . . . . . . . . . . 15
 
                         |
107 | 104, 105 | eqeqan12d 2477 |
. . . . . . . . . . . . . . 15
 
                     |
108 | 106, 107 | orbi12d 709 |
. . . . . . . . . . . . . 14
 
                     
                       |
109 | 103, 108 | imbi12d 320 |
. . . . . . . . . . . . 13
 
                       

                        |
110 | 102, 109 | imbi12d 320 |
. . . . . . . . . . . 12
 
               
       
 
 
 

                                   
       
 
 
 

                         |
111 | 13, 12, 110, 97 | vtocl2 3131 |
. . . . . . . . . . 11
                       
 
  
                       |
112 | 111 | ancom2s 800 |
. . . . . . . . . 10
                       
 
  
                       |
113 | 98, 112 | orim12d 834 |
. . . . . . . . 9
                       
 
   
                                              |
114 | 11, 113 | mpd 15 |
. . . . . . . 8
                       
 
                                              |
115 | | 3mix1 1157 |
. . . . . . . . . 10
                                           |
116 | | 3mix2 1158 |
. . . . . . . . . 10
                                         |
117 | 115, 116 | jaoi 379 |
. . . . . . . . 9
                                                     |
118 | | 3mix3 1159 |
. . . . . . . . . 10
                                           |
119 | 116 | eqcoms 2466 |
. . . . . . . . . 10
                                         |
120 | 118, 119 | jaoi 379 |
. . . . . . . . 9
                                                     |
121 | 117, 120 | jaoi 379 |
. . . . . . . 8
                                                                           |
122 | 114, 121 | syl 16 |
. . . . . . 7
                       
 
                                  |
123 | | breq12 4406 |
. . . . . . . 8
                           |
124 | | eqeq12 2473 |
. . . . . . . 8
                       |
125 | | breq12 4406 |
. . . . . . . . 9
                           |
126 | 125 | ancoms 453 |
. . . . . . . 8
                           |
127 | 123, 124,
126 | 3orbi123d 1289 |
. . . . . . 7
                                         
  
      |
128 | 122, 127 | syl5ibcom 220 |
. . . . . 6
                       
 
            
  
      |
129 | 128 | rexlimdvva 2954 |
. . . . 5
            
       
 
  
                    |
130 | 6, 129 | syl5bir 218 |
. . . 4
            
       
 
             
  
      |
131 | 5, 130 | sylbid 215 |
. . 3
            
       
 
   
  
      |
132 | 131 | ralrimivv 2913 |
. 2
            
       
 
       
     |
133 | | df-so 4751 |
. 2

 
 
          |
134 | 1, 132, 133 | sylanbrc 664 |
1
            
       
 
   |