Step | Hyp | Ref
| Expression |
1 | | suceq 4284 |
. . . . 5

  |
2 | 1 | eleq1d 2183 |
. . . 4
 
   |
3 | | tfrcllemsucaccv.u |
. . . . 5
 
 
  |
4 | 3 | ralrimiva 2479 |
. . . 4
     |
5 | | tfrcllemsucaccv.zy |
. . . . 5
   |
6 | | tfrcllemsucaccv.yx |
. . . . 5
   |
7 | | elunii 3707 |
. . . . 5
 
    |
8 | 5, 6, 7 | syl2anc 406 |
. . . 4
    |
9 | 2, 4, 8 | rspcdva 2765 |
. . 3
   |
10 | | tfrcl.f |
. . . 4
recs   |
11 | | tfrcl.g |
. . . 4
   |
12 | | tfrcl.x |
. . . 4
   |
13 | | tfrcl.ex |
. . . 4
 
           |
14 | | tfrcllemsucfn.1 |
. . . 4
 
                   |
15 | 5, 6 | jca 302 |
. . . . 5
 
   |
16 | | ordtr1 4270 |
. . . . 5

 
    |
17 | 12, 15, 16 | sylc 62 |
. . . 4
   |
18 | | tfrcllemsucaccv.gfn |
. . . 4
       |
19 | | tfrcllemsucaccv.gacc |
. . . 4
   |
20 | 10, 11, 12, 13, 14, 17, 18, 19 | tfrcllemsucfn 6204 |
. . 3
                  |
21 | | vex 2660 |
. . . . . 6
 |
22 | 21 | elsuc 4288 |
. . . . 5


   |
23 | | vex 2660 |
. . . . . . . . . . 11
 |
24 | | feq1 5213 |
. . . . . . . . . . . . 13
     
       |
25 | | fveq1 5374 |
. . . . . . . . . . . . . . 15
           |
26 | | reseq1 4771 |
. . . . . . . . . . . . . . . 16
       |
27 | 26 | fveq2d 5379 |
. . . . . . . . . . . . . . 15
               |
28 | 25, 27 | eqeq12d 2129 |
. . . . . . . . . . . . . 14
           
             |
29 | 28 | ralbidv 2411 |
. . . . . . . . . . . . 13
  
         

             |
30 | 24, 29 | anbi12d 462 |
. . . . . . . . . . . 12
       
                
              |
31 | 30 | rexbidv 2412 |
. . . . . . . . . . 11
  
     
           
     
              |
32 | 23, 31, 14 | elab2 2801 |
. . . . . . . . . 10


                   |
33 | 19, 32 | sylib 121 |
. . . . . . . . 9
       
             |
34 | | simprrr 512 |
. . . . . . . . . 10
 

                  

            |
35 | | simprrl 511 |
. . . . . . . . . . . . 13
 

                  
      |
36 | | ffn 5230 |
. . . . . . . . . . . . 13
       |
37 | 35, 36 | syl 14 |
. . . . . . . . . . . 12
 

                  
  |
38 | 18 | adantr 272 |
. . . . . . . . . . . . 13
 

                  
      |
39 | | ffn 5230 |
. . . . . . . . . . . . 13
       |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . 12
 

                  
  |
41 | | fndmu 5182 |
. . . . . . . . . . . 12
 
   |
42 | 37, 40, 41 | syl2anc 406 |
. . . . . . . . . . 11
 

                  
  |
43 | 42 | raleqdv 2606 |
. . . . . . . . . 10
 

                  
 
         

             |
44 | 34, 43 | mpbid 146 |
. . . . . . . . 9
 

                  

            |
45 | 33, 44 | rexlimddv 2528 |
. . . . . . . 8
              |
46 | 45 | r19.21bi 2494 |
. . . . . . 7
 
             |
47 | | ordelon 4265 |
. . . . . . . . . . . . 13
     |
48 | 12, 17, 47 | syl2anc 406 |
. . . . . . . . . . . 12
   |
49 | | onelon 4266 |
. . . . . . . . . . . 12
 
   |
50 | 48, 49 | sylan 279 |
. . . . . . . . . . 11
 
   |
51 | | eloni 4257 |
. . . . . . . . . . 11
   |
52 | | ordirr 4417 |
. . . . . . . . . . 11

  |
53 | 50, 51, 52 | 3syl 17 |
. . . . . . . . . 10
 

  |
54 | | elequ2 1674 |
. . . . . . . . . . . 12
 
   |
55 | 54 | biimpcd 158 |
. . . . . . . . . . 11
     |
56 | 55 | adantl 273 |
. . . . . . . . . 10
 
     |
57 | 53, 56 | mtod 635 |
. . . . . . . . 9
 

  |
58 | 57 | neqned 2289 |
. . . . . . . 8
 
   |
59 | | fvunsng 5568 |
. . . . . . . 8
                        |
60 | 21, 58, 59 | sylancr 408 |
. . . . . . 7
 
                      |
61 | | eloni 4257 |
. . . . . . . . . . . 12
   |
62 | 48, 61 | syl 14 |
. . . . . . . . . . 11
   |
63 | | ordelss 4261 |
. . . . . . . . . . 11
     |
64 | 62, 63 | sylan 279 |
. . . . . . . . . 10
 
   |
65 | | resabs1 4806 |
. . . . . . . . . 10
                               |
66 | 64, 65 | syl 14 |
. . . . . . . . 9
 
                               |
67 | 18, 39 | syl 14 |
. . . . . . . . . . . 12
   |
68 | | ordirr 4417 |
. . . . . . . . . . . . 13

  |
69 | 62, 68 | syl 14 |
. . . . . . . . . . . 12
   |
70 | | fsnunres 5576 |
. . . . . . . . . . . 12
 

               |
71 | 67, 69, 70 | syl2anc 406 |
. . . . . . . . . . 11
                |
72 | 71 | reseq1d 4776 |
. . . . . . . . . 10
                    |
73 | 72 | adantr 272 |
. . . . . . . . 9
 
                    |
74 | 66, 73 | eqtr3d 2149 |
. . . . . . . 8
 
                  |
75 | 74 | fveq2d 5379 |
. . . . . . 7
 
                          |
76 | 46, 60, 75 | 3eqtr4d 2157 |
. . . . . 6
 
                                   |
77 | | feq2 5214 |
. . . . . . . . . . . . 13
     
       |
78 | 77 | imbi1d 230 |
. . . . . . . . . . . 12
      
                  |
79 | 78 | albidv 1778 |
. . . . . . . . . . 11
             
      
        |
80 | 13 | 3expia 1166 |
. . . . . . . . . . . . 13
 
             |
81 | 80 | alrimiv 1828 |
. . . . . . . . . . . 12
 
       
       |
82 | 81 | ralrimiva 2479 |
. . . . . . . . . . 11
                |
83 | 79, 82, 17 | rspcdva 2765 |
. . . . . . . . . 10
               |
84 | | feq1 5213 |
. . . . . . . . . . . 12
             |
85 | | fveq2 5375 |
. . . . . . . . . . . . 13
           |
86 | 85 | eleq1d 2183 |
. . . . . . . . . . . 12
     
       |
87 | 84, 86 | imbi12d 233 |
. . . . . . . . . . 11
      
                  |
88 | 87 | spv 1814 |
. . . . . . . . . 10
                         |
89 | 83, 18, 88 | sylc 62 |
. . . . . . . . 9
       |
90 | | fndm 5180 |
. . . . . . . . . . 11

  |
91 | 67, 90 | syl 14 |
. . . . . . . . . 10
   |
92 | 69, 91 | neleqtrrd 2213 |
. . . . . . . . 9
   |
93 | | fsnunfv 5575 |
. . . . . . . . 9
     
                      |
94 | 5, 89, 92, 93 | syl3anc 1199 |
. . . . . . . 8
                      |
95 | 94 | adantr 272 |
. . . . . . 7
 
                      |
96 | | simpr 109 |
. . . . . . . 8
 
   |
97 | 96 | fveq2d 5379 |
. . . . . . 7
 
                                 |
98 | | reseq2 4772 |
. . . . . . . . 9
                             |
99 | 98, 71 | sylan9eqr 2169 |
. . . . . . . 8
 
                |
100 | 99 | fveq2d 5379 |
. . . . . . 7
 
                        |
101 | 95, 97, 100 | 3eqtr4d 2157 |
. . . . . 6
 
                                   |
102 | 76, 101 | jaodan 769 |
. . . . 5
 

                                    |
103 | 22, 102 | sylan2b 283 |
. . . 4
 
                                   |
104 | 103 | ralrimiva 2479 |
. . 3
                                     |
105 | | feq2 5214 |
. . . . . 6
                                   |
106 | | raleq 2600 |
. . . . . 6
                                  
                                     |
107 | 105, 106 | anbi12d 462 |
. . . . 5
                                                                                                          |
108 | 107 | rspcev 2760 |
. . . 4
                                                                       
                                   |
109 | | feq2 5214 |
. . . . . 6
                                   |
110 | | raleq 2600 |
. . . . . 6
  
                               

                                   |
111 | 109, 110 | anbi12d 462 |
. . . . 5
                  
                                
                                                     |
112 | 111 | cbvrexv 2629 |
. . . 4
                  
                                

                                                    |
113 | 108, 112 | sylib 121 |
. . 3
                                                                       
                                   |
114 | 9, 20, 104, 113 | syl12anc 1197 |
. 2
                  
                                   |
115 | | vex 2660 |
. . . . . 6
 |
116 | | opexg 4110 |
. . . . . 6
                |
117 | 115, 89, 116 | sylancr 408 |
. . . . 5
          |
118 | | snexg 4068 |
. . . . 5
       
           |
119 | 117, 118 | syl 14 |
. . . 4
            |
120 | | unexg 4324 |
. . . 4
          
              |
121 | 23, 119, 120 | sylancr 408 |
. . 3
              |
122 | | feq1 5213 |
. . . . . 6
                
                  |
123 | | fveq1 5374 |
. . . . . . . 8
                                 |
124 | | reseq1 4771 |
. . . . . . . . 9
                             |
125 | 124 | fveq2d 5379 |
. . . . . . . 8
                                     |
126 | 123, 125 | eqeq12d 2129 |
. . . . . . 7
                      
                                   |
127 | 126 | ralbidv 2411 |
. . . . . 6
             
         

                                   |
128 | 122, 127 | anbi12d 462 |
. . . . 5
                  
                           
                                    |
129 | 128 | rexbidv 2412 |
. . . 4
             
     
           
                
                                    |
130 | 129, 14 | elab2g 2800 |
. . 3
                                         
                                    |
131 | 121, 130 | syl 14 |
. 2
                              
                                    |
132 | 114, 131 | mpbird 166 |
1
              |