Step | Hyp | Ref
| Expression |
1 | | ovex 6336 |
. . . . . 6
 supp 
 |
2 | | cantnflem1.o |
. . . . . . 7
OrdIso  supp    |
3 | 2 | oion 8069 |
. . . . . 6
  supp    |
4 | 1, 3 | mp1i 13 |
. . . . 5
   |
5 | | uniexg 6607 |
. . . . 5
 
  |
6 | | sucidg 5508 |
. . . . 5
  
   |
7 | 4, 5, 6 | 3syl 18 |
. . . 4
     |
8 | | cantnfs.s |
. . . . . . . . . 10
 CNF   |
9 | | cantnfs.a |
. . . . . . . . . 10
   |
10 | | cantnfs.b |
. . . . . . . . . 10
   |
11 | | oemapval.t |
. . . . . . . . . 10
   

        


            |
12 | | oemapval.f |
. . . . . . . . . 10
   |
13 | | oemapval.g |
. . . . . . . . . 10
   |
14 | | oemapvali.r |
. . . . . . . . . 10
     |
15 | | oemapvali.x |
. . . . . . . . . 10
            |
16 | 8, 9, 10, 11, 12, 13, 14, 15 | cantnflem1a 8208 |
. . . . . . . . 9
  supp    |
17 | | n0i 3727 |
. . . . . . . . 9
  supp   supp    |
18 | 16, 17 | syl 17 |
. . . . . . . 8
  supp    |
19 | | suppssdm 6946 |
. . . . . . . . . . . 12
 supp 
 |
20 | 8, 9, 10 | cantnfs 8189 |
. . . . . . . . . . . . . . 15
       finSupp     |
21 | 13, 20 | mpbid 215 |
. . . . . . . . . . . . . 14
      finSupp
   |
22 | 21 | simpld 466 |
. . . . . . . . . . . . 13
       |
23 | | fdm 5745 |
. . . . . . . . . . . . 13
       |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
   |
25 | 19, 24 | syl5sseq 3466 |
. . . . . . . . . . 11
  supp    |
26 | 10, 25 | ssexd 4543 |
. . . . . . . . . 10
  supp    |
27 | 8, 9, 10, 2, 13 | cantnfcl 8190 |
. . . . . . . . . . 11
  supp     |
28 | 27 | simpld 466 |
. . . . . . . . . 10
  supp    |
29 | 2 | oien 8071 |
. . . . . . . . . 10
   supp 

supp  

supp    |
30 | 26, 28, 29 | syl2anc 673 |
. . . . . . . . 9
  supp    |
31 | | breq1 4398 |
. . . . . . . . . 10
   supp 
 supp     |
32 | | ensymb 7635 |
. . . . . . . . . . 11
  supp 
 supp    |
33 | | en0 7650 |
. . . . . . . . . . 11
  supp 
 supp    |
34 | 32, 33 | bitri 257 |
. . . . . . . . . 10
  supp 
 supp    |
35 | 31, 34 | syl6bb 269 |
. . . . . . . . 9
   supp 
 supp     |
36 | 30, 35 | syl5ibcom 228 |
. . . . . . . 8
   supp     |
37 | 18, 36 | mtod 182 |
. . . . . . 7
   |
38 | 27 | simprd 470 |
. . . . . . . 8
   |
39 | | nnlim 6724 |
. . . . . . . 8
   |
40 | 38, 39 | syl 17 |
. . . . . . 7
   |
41 | | ioran 498 |
. . . . . . 7
   
   |
42 | 37, 40, 41 | sylanbrc 677 |
. . . . . 6
     |
43 | 2 | oicl 8062 |
. . . . . . 7
 |
44 | | unizlim 5546 |
. . . . . . 7

  
    |
45 | 43, 44 | mp1i 13 |
. . . . . 6
  

    |
46 | 42, 45 | mtbird 308 |
. . . . 5
 
  |
47 | | orduniorsuc 6676 |
. . . . . . 7

      |
48 | 43, 47 | mp1i 13 |
. . . . . 6
  
    |
49 | 48 | ord 384 |
. . . . 5
       |
50 | 46, 49 | mpd 15 |
. . . 4
    |
51 | 7, 50 | eleqtrrd 2552 |
. . 3
    |
52 | 2 | oiiso 8070 |
. . . . . . . 8
   supp 

supp      supp
    |
53 | 26, 28, 52 | syl2anc 673 |
. . . . . . 7

   supp     |
54 | | isof1o 6234 |
. . . . . . 7

   supp        supp    |
55 | 53, 54 | syl 17 |
. . . . . 6
      supp    |
56 | | f1ocnv 5840 |
. . . . . 6
      supp 
    supp      |
57 | | f1of 5828 |
. . . . . 6
     supp        supp      |
58 | 55, 56, 57 | 3syl 18 |
. . . . 5
     supp   
  |
59 | 58, 16 | ffvelrnd 6038 |
. . . 4
        |
60 | | elssuni 4219 |
. . . 4
              |
61 | 59, 60 | syl 17 |
. . 3
         |
62 | 50, 38 | eqeltrrd 2550 |
. . . . 5
    |
63 | | peano2b 6727 |
. . . . 5
 
   |
64 | 62, 63 | sylibr 217 |
. . . 4
    |
65 | | eleq1 2537 |
. . . . . . . 8
       |
66 | | sseq2 3440 |
. . . . . . . 8
                 |
67 | 65, 66 | anbi12d 725 |
. . . . . . 7
   
     
            |
68 | | fveq2 5879 |
. . . . . . . . . . . 12
             |
69 | 68 | sseq2d 3446 |
. . . . . . . . . . 11
               |
70 | 69 | ifbid 3894 |
. . . . . . . . . 10
              
 
              |
71 | 70 | mpteq2dv 4483 |
. . . . . . . . 9
                                   |
72 | 71 | fveq2d 5883 |
. . . . . . . 8
    CNF    
 
               CNF                       |
73 | | suceq 5495 |
. . . . . . . . 9
     |
74 | 73 | fveq2d 5883 |
. . . . . . . 8
             |
75 | 72, 74 | eleq12d 2543 |
. . . . . . 7
     CNF                       
  CNF                             |
76 | 67, 75 | imbi12d 327 |
. . . . . 6
             CNF    
 
                 
         
  CNF                              |
77 | 76 | imbi2d 323 |
. . . . 5
           
  CNF                          
  
         CNF                               |
78 | | eleq1 2537 |
. . . . . . . 8


   |
79 | | sseq2 3440 |
. . . . . . . 8

     
        |
80 | 78, 79 | anbi12d 725 |
. . . . . . 7

                  |
81 | | fveq2 5879 |
. . . . . . . . . . . 12

          |
82 | 81 | sseq2d 3446 |
. . . . . . . . . . 11

    
       |
83 | 82 | ifbid 3894 |
. . . . . . . . . 10

 
                          |
84 | 83 | mpteq2dv 4483 |
. . . . . . . . 9

  
                             |
85 | 84 | fveq2d 5883 |
. . . . . . . 8

  CNF    
                 CNF    
 
               |
86 | | suceq 5495 |
. . . . . . . . 9

  |
87 | 86 | fveq2d 5883 |
. . . . . . . 8

  
       |
88 | 85, 87 | eleq12d 2543 |
. . . . . . 7

   CNF                       
  CNF                      
    |
89 | 80, 88 | imbi12d 327 |
. . . . . 6

        
  CNF                        
 
        CNF                            |
90 | | eleq1 2537 |
. . . . . . . 8
     |
91 | | sseq2 3440 |
. . . . . . . 8
               |
92 | 90, 91 | anbi12d 725 |
. . . . . . 7
         
         |
93 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
94 | 93 | sseq2d 3446 |
. . . . . . . . . . 11
 
   
       |
95 | 94 | ifbid 3894 |
. . . . . . . . . 10
  
                          |
96 | 95 | mpteq2dv 4483 |
. . . . . . . . 9
                                 |
97 | 96 | fveq2d 5883 |
. . . . . . . 8
   CNF                      CNF                      |
98 | | suceq 5495 |
. . . . . . . . 9

  |
99 | 98 | fveq2d 5883 |
. . . . . . . 8
           |
100 | 97, 99 | eleq12d 2543 |
. . . . . . 7
    CNF    
 
                
  CNF                           |
101 | 92, 100 | imbi12d 327 |
. . . . . 6
   
        CNF    
 
                 
       
  CNF                            |
102 | | eleq1 2537 |
. . . . . . . 8
     |
103 | | sseq2 3440 |
. . . . . . . 8
           
   |
104 | 102, 103 | anbi12d 725 |
. . . . . . 7
  
     

    
    |
105 | | fveq2 5879 |
. . . . . . . . . . . 12
       
   |
106 | 105 | sseq2d 3446 |
. . . . . . . . . . 11
             |
107 | 106 | ifbid 3894 |
. . . . . . . . . 10
             
 
             |
108 | 107 | mpteq2dv 4483 |
. . . . . . . . 9
                                 |
109 | 108 | fveq2d 5883 |
. . . . . . . 8
   CNF    
 
               CNF                      |
110 | | suceq 5495 |
. . . . . . . . 9

  |
111 | 110 | fveq2d 5883 |
. . . . . . . 8
           |
112 | 109, 111 | eleq12d 2543 |
. . . . . . 7
    CNF                       
  CNF                           |
113 | 104, 112 | imbi12d 327 |
. . . . . 6
            CNF    
 
                 
          CNF                            |
114 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . 13
       supp   supp              |
115 | 55, 16, 114 | syl2anc 673 |
. . . . . . . . . . . 12
            |
116 | 115 | sseq2d 3446 |
. . . . . . . . . . 11
          
   |
117 | 116 | ifbid 3894 |
. . . . . . . . . 10
                  
 
         |
118 | 117 | mpteq2dv 4483 |
. . . . . . . . 9
                                  |
119 | 118 | fveq2d 5883 |
. . . . . . . 8
   CNF    
 
                    CNF    
  
          |
120 | | cantnflem1.h |
. . . . . . . . 9
seq𝜔  
                      |
121 | 8, 9, 10, 11, 12, 13, 14, 15, 2, 120 | cantnflem1d 8211 |
. . . . . . . 8
   CNF    
 
           
        |
122 | 119, 121 | eqeltrd 2549 |
. . . . . . 7
   CNF    
 
                    
        |
123 | | ss0 3768 |
. . . . . . . . . . . . . 14
     
       |
124 | 123 | fveq2d 5883 |
. . . . . . . . . . . . 13
     
               |
125 | 124 | sseq2d 3446 |
. . . . . . . . . . . 12
     
         
       |
126 | 125 | ifbid 3894 |
. . . . . . . . . . 11
     
 
                               |
127 | 126 | mpteq2dv 4483 |
. . . . . . . . . 10
     

 
                                  |
128 | 127 | fveq2d 5883 |
. . . . . . . . 9
     
  CNF                           CNF    
 
               |
129 | | suceq 5495 |
. . . . . . . . . . 11
     
       |
130 | 123, 129 | syl 17 |
. . . . . . . . . 10
     
       |
131 | 130 | fveq2d 5883 |
. . . . . . . . 9
     
               |
132 | 128, 131 | eleq12d 2543 |
. . . . . . . 8
     
   CNF                                    CNF                      
    |
133 | 132 | adantl 473 |
. . . . . . 7
 
         CNF    
 
                    
        CNF                      
    |
134 | 122, 133 | syl5ibcom 228 |
. . . . . 6
           CNF    
 
                    |
135 | | ordelon 5454 |
. . . . . . . . . . . . 13
 
             |
136 | 43, 59, 135 | sylancr 676 |
. . . . . . . . . . . 12
        |
137 | 136 | adantr 472 |
. . . . . . . . . . 11
 
        |
138 | 43 | a1i 11 |
. . . . . . . . . . . 12

  |
139 | | ordelon 5454 |
. . . . . . . . . . . 12
 

  |
140 | 138, 139 | sylan 479 |
. . . . . . . . . . 11
 
   |
141 | | onsseleq 5471 |
. . . . . . . . . . 11
             
               |
142 | 137, 140,
141 | syl2anc 673 |
. . . . . . . . . 10
 
            
         |
143 | | sucelon 6663 |
. . . . . . . . . . . . . . 15

  |
144 | 140, 143 | sylibr 217 |
. . . . . . . . . . . . . 14
 

  |
145 | | eloni 5440 |
. . . . . . . . . . . . . 14
   |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . 13
 
   |
147 | | ordsssuc 5516 |
. . . . . . . . . . . . 13
                      |
148 | 137, 146,
147 | syl2anc 673 |
. . . . . . . . . . . 12
 
               |
149 | | ordtr 5444 |
. . . . . . . . . . . . . . . . 17

  |
150 | 43, 149 | mp1i 13 |
. . . . . . . . . . . . . . . 16
 

      
  |
151 | | simprl 772 |
. . . . . . . . . . . . . . . 16
 

      
  |
152 | | trsuc 5514 |
. . . . . . . . . . . . . . . 16
  
  |
153 | 150, 151,
152 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 

         |
154 | | simprr 774 |
. . . . . . . . . . . . . . 15
 

              |
155 | 153, 154 | jca 541 |
. . . . . . . . . . . . . 14
 

       
        |
156 | 9 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

         |
157 | 10 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

         |
158 | | oecl 7257 |
. . . . . . . . . . . . . . . . . . 19
 
     |
159 | 156, 157,
158 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 

           |
160 | 8, 156, 157 | cantnff 8197 |
. . . . . . . . . . . . . . . . . . 19
 

        CNF          |
161 | 8, 9, 10 | cantnfs 8189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       finSupp     |
162 | 12, 161 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      finSupp
   |
163 | 162 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
164 | 163 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
165 | 8, 9, 10, 11, 12, 13, 14, 15 | oemapvali 8207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                        |
166 | 165 | simp1d 1042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
167 | 22, 166 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
168 | | ne0i 3728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
170 | | on0eln0 5485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
171 | 9, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
172 | 169, 171 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
173 | 172 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
174 | 164, 173 | ifcld 3915 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
             |
175 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                            |
176 | 174, 175 | fmptd 6061 |
. . . . . . . . . . . . . . . . . . . . 21
                      |
177 | | mptexg 6151 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
178 | 10, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
179 | | funmpt 5625 |
. . . . . . . . . . . . . . . . . . . . . . 23
                |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
181 | 162 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . 22
 finSupp   |
182 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 supp 
 supp   |
183 | | eqimss2 3471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  supp   supp   supp   supp    |
184 | 182, 183 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  supp  
supp    |
185 | | 0ex 4528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
187 | 163, 184,
10, 186 | suppssr 6965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

 supp          |
188 | 187 | ifeq1d 3890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

 supp                            |
189 | | ifid 3909 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      
 |
190 | 188, 189 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

 supp                   |
191 | 190, 10 | suppss2 6968 |
. . . . . . . . . . . . . . . . . . . . . 22
                 supp  
supp    |
192 | | fsuppsssupp 7917 |
. . . . . . . . . . . . . . . . . . . . . 22
                 
  
              finSupp                 supp
 
supp   

 
            finSupp   |
193 | 178, 180,
181, 191, 192 | syl22anc 1293 |
. . . . . . . . . . . . . . . . . . . . 21
               
finSupp   |
194 | 8, 9, 10 | cantnfs 8189 |
. . . . . . . . . . . . . . . . . . . . 21
                    
                              
finSupp     |
195 | 176, 193,
194 | mpbir2and 936 |
. . . . . . . . . . . . . . . . . . . 20
                  |
196 | 195 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

                        |
197 | 160, 196 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . 18
 

         CNF                        |
198 | | onelon 5455 |
. . . . . . . . . . . . . . . . . 18
      CNF    
 
                  CNF    
 
               |
199 | 159, 197,
198 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 

         CNF                      |
200 | 38 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 

      
  |
201 | | elnn 6721 |
. . . . . . . . . . . . . . . . . . 19
  
  |
202 | 151, 200,
201 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 

      
  |
203 | 120 | cantnfvalf 8188 |
. . . . . . . . . . . . . . . . . . 19
     |
204 | 203 | ffvelrni 6036 |
. . . . . . . . . . . . . . . . . 18
       |
205 | 202, 204 | syl 17 |
. . . . . . . . . . . . . . . . 17
 

             |
206 | 25 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 

        supp    |
207 | 2 | oif 8063 |
. . . . . . . . . . . . . . . . . . . . . . 23
     supp   |
208 | 207 | ffvelrni 6036 |
. . . . . . . . . . . . . . . . . . . . . 22
      supp    |
209 | 151, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 

            supp    |
210 | 206, 209 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . 20
 

             |
211 | | onelon 5455 |
. . . . . . . . . . . . . . . . . . . 20
             |
212 | 157, 210,
211 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 

             |
213 | | oecl 7257 |
. . . . . . . . . . . . . . . . . . 19
               |
214 | 156, 212,
213 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 

               |
215 | 163 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 

             |
216 | 215, 210 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . 19
 

                 |
217 | | onelon 5455 |
. . . . . . . . . . . . . . . . . . 19
       
             |
218 | 156, 216,
217 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 

                 |
219 | | omcl 7256 |
. . . . . . . . . . . . . . . . . 18
             
                     |
220 | 214, 218,
219 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 

                         |
221 | | oaord 7266 |
. . . . . . . . . . . . . . . . 17
    CNF    
 
                                     CNF                       
                   CNF                          
                   |
222 | 199, 205,
220, 221 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
 

          CNF    
                  
                   CNF                          
                   |
223 | | ifeq1 3876 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
 
                      |
224 | | ifid 3909 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        |
225 | 223, 224 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
             |
226 | | ifeq1 3876 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                  
                 |
227 | | ifid 3909 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
 |
228 | 226, 227 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                  
  |
229 | 225, 228 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . . 21
    
             
                  
   |
230 | | onss 6636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
231 | 10, 230 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
232 | 231 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
233 | 232 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              |
234 | 212 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                  |
235 | | onsseleq 5471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                         |
236 | 233, 234,
235 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
   
             |
237 | 236 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  
   
             |
238 | 233 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                    |
239 | 207 | ffvelrni 6036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      supp    |
240 | 153, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

            supp    |
241 | 206, 240 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

             |
242 | | onelon 5455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             |
243 | 157, 241,
242 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

             |
244 | 243 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                        |
245 | | onsssuc 5517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   |
246 | 238, 244,
245 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
   
       |
247 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
248 | 247 | sucid 5509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
249 | 53 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

          supp
    |
250 | | isorel 6235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   supp   
  
           |
251 | 249, 153,
151, 250 | syl12anc 1290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

       
           |
252 | 247 | sucex 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 |
253 | 252 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
254 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
  |
255 | 254 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        
          |
256 | 251, 253,
255 | 3bitr3g 295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

       
           |
257 | 248, 256 | mpbii 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

                 |
258 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
259 | 212, 258 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

      
      |
260 | | ordelsuc 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                               |
261 | 243, 259,
260 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

               
           |
262 | 257, 261 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

      
          |
263 | 262 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                            |
264 | 263 | sseld 3417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         
    |
265 | 246, 264 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                  
           |
266 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                              |
267 | 249 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                           supp     |
268 | 267, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                             supp    |
269 | 8, 9, 10, 11, 12, 13, 14, 15, 2 | cantnflem1c 8210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                       
 supp    |
270 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       supp   supp              |
271 | 268, 269,
270 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                   |
272 | 266, 271 | eleqtrrd 2552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                       |
273 | 153 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                       
  |
274 | 268, 56, 57 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                            supp   
  |
275 | 274, 269 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                               |
276 | | isorel 6235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   supp   
                             |
277 | 267, 273,
275, 276 | syl12anc 1290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                              |
278 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      |
279 | 278 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
       |
280 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          |
281 | 280 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                             |
282 | 277, 279,
281 | 3bitr3g 295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                              |
283 | 272, 282 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       
       |
284 | | ordelon 5454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
             |
285 | 43, 275, 284 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                               |
286 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
287 | 285, 286 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                               |
288 | | ordelsuc 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
     
        |
289 | 283, 287,
288 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                             
        |
290 | 283, 289 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                       
       |
291 | 151 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                          |
292 | 43, 291, 139 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                          |
293 | | ontri1 5464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
             
        |
294 | 292, 285,
293 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                        
             |
295 | 290, 294 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                               |
296 | | isorel 6235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   supp                
                |
297 | 267, 275,
291, 296 | syl12anc 1290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                         
    |
298 | 252 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       |
299 | 254 | epelc 4752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
            
   |
300 | 297, 298,
299 | 3bitr3g 295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         
    |
301 | 271 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                    
        |
302 | 300, 301 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                
    |
303 | 295, 302 | mtbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                       
      |
304 | 303 | expr 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                      
       |
305 | 304 | con2d 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     
        |
306 | | ontri1 5464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   |
307 | 238, 244,
306 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
   
       |
308 | 305, 307 | sylibrd 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     

       |
309 | 265, 308 | impbid 195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  
   
       |
310 | 309 | orbi1d 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       
                  |
311 | 237, 310 | bitr4d 264 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
   
             |
312 | | orcom 394 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        
            |
313 | 311, 312 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . . . 22
                  
   
             |
314 | 313 | ifbid 3894 |
. . . . . . . . . . . . . . . . . . . . 21
                   
  
       
                     |
315 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . 21
              |
316 | 229, 314,
315 | pm2.61ne 2728 |
. . . . . . . . . . . . . . . . . . . 20
             
  
       
                     |
317 | 316 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . . 19
 

                                             |
318 | 317 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
 

         CNF                      CNF    
                       |
319 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
320 | 319, 185 | ifex 3940 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
            |
321 | 320 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

                      |
322 | 321 | ralrimivw 2810 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

                    
  |
323 | 175 | fnmpt 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
                            |
324 | 322, 323 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

                        |
325 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

         |
326 | | suppvalfn 6940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
                 supp      
                  |
327 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
328 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
329 | | nffvmpt1 5887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                      |
330 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
331 | 329, 330 | nfne 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      |
332 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      |
333 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                         |
334 | 333 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    
                      |
335 | 327, 328,
331, 332, 334 | cbvrab 3029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     
   
                 |
336 | 326, 335 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
                 supp      
                  |
337 | 324, 157,
325, 336 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
 

          
            supp      
                  |
338 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

                                       |
339 | 320 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
             |
340 | 338, 339 | fvmpt2d 5974 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                
             |
341 | 340 | neeq1d 2702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                               
 
              |
342 | 339 | biantrurd 516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                            
                            |
343 | | dif1o 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
 
  
          
 
              |
344 | 342, 343 | syl6bbr 271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                      
     |
345 | 341, 344 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               
 
                |
346 | 345 | rabbidva 3021 |
. . . . . . . . . . . . . . . . . . . . . 22
 

                            
            
     |
347 | 337, 346 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . 21
 

          
            supp               
     |
348 | 320, 343 | mpbiran 932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
 
 
             |
349 | | ifeq1 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 
                      |
350 | 349, 189 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
             |
351 | 350 | necon3i 2675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
      |
352 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

     
             |
353 | 352 | necon1ai 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
      |
354 | 351, 353 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
            |
355 | 265 | expimpd 614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                              |
356 | 354, 355 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                         
       |
357 | 348, 356 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         
         |
358 | 357 | 3impia 1228 |
. . . . . . . . . . . . . . . . . . . . . 22
          
 
             
      |
359 | 358 | rabssdv 3495 |
. . . . . . . . . . . . . . . . . . . . 21
 

         
             
      |
360 | 347, 359 | eqsstrd 3452 |
. . . . . . . . . . . . . . . . . . . 20
 

          
            supp        |
361 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
        |
362 | | sseq1 3439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
       |
363 | 361, 362 | orbi12d 724 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         |
364 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
365 | 363, 364 | ifbieq1d 3895 |
. . . . . . . . . . . . . . . . . . . . . 22
                                         |
366 | 365 | cbvmptv 4488 |
. . . . . . . . . . . . . . . . . . . . 21
                                           |
367 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
368 | 367 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
              
    |
369 | 368 | ifeq1da 3902 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                             
                         |
370 | 362, 364 | ifbieq1d 3895 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
                          |
371 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
372 | 371, 185 | ifex 3940 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
            |
373 | 370, 175,
372 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     
             |
374 | 373 | ifeq2d 3891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                             |
375 | | ifor 3919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  
                           |
376 | 374, 375 | syl6eqr 2523 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                      |
377 | 369, 376 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                          |
378 | 377 | mpteq2ia 4478 |
. . . . . . . . . . . . . . . . . . . . 21
     
                                                      |
379 | 366, 378 | eqtr4i 2496 |
. . . . . . . . . . . . . . . . . . . 20
                                                            |
380 | 8, 156, 157, 196, 210, 216, 360, 379 | cantnfp1 8204 |
. . . . . . . . . . . . . . . . . . 19
 

                               CNF    
                                        CNF                        |
381 | 380 | simprd 470 |
. . . . . . . . . . . . . . . . . 18
 
|