Step | Hyp | Ref
| Expression |
1 | | cnfcom.1 |
. 2
   |
2 | | cnfcom.s |
. . . . . 6
 CNF   |
3 | | omelon 8182 |
. . . . . . 7
 |
4 | 3 | a1i 11 |
. . . . . 6
   |
5 | | cnfcom.a |
. . . . . 6
   |
6 | | cnfcom.g |
. . . . . 6
OrdIso  supp    |
7 | | cnfcom.f |
. . . . . . 7
   CNF      |
8 | 2, 4, 5 | cantnff1o 8232 |
. . . . . . . . 9
  CNF
         |
9 | | f1ocnv 5853 |
. . . . . . . . 9
  CNF       
  CNF          |
10 | | f1of 5841 |
. . . . . . . . 9
   CNF
      
  CNF          |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . 8
   CNF          |
12 | | cnfcom.b |
. . . . . . . 8
     |
13 | 11, 12 | ffvelrnd 6051 |
. . . . . . 7
    CNF       |
14 | 7, 13 | syl5eqel 2544 |
. . . . . 6
   |
15 | 2, 4, 5, 6, 14 | cantnfcl 8203 |
. . . . 5
  supp     |
16 | 15 | simprd 469 |
. . . 4
   |
17 | | elnn 6734 |
. . . 4
     |
18 | 1, 16, 17 | syl2anc 671 |
. . 3
   |
19 | | eleq1 2528 |
. . . . . 6
     |
20 | | suceq 5511 |
. . . . . . . 8

  |
21 | 20 | fveq2d 5896 |
. . . . . . 7
           |
22 | 20 | fveq2d 5896 |
. . . . . . 7
           |
23 | | fveq2 5892 |
. . . . . . . . 9
           |
24 | 23 | oveq2d 6336 |
. . . . . . . 8
               |
25 | 23 | fveq2d 5896 |
. . . . . . . 8
                   |
26 | 24, 25 | oveq12d 6338 |
. . . . . . 7
                                   |
27 | 21, 22, 26 | f1oeq123d 5838 |
. . . . . 6
                                                             |
28 | 19, 27 | imbi12d 326 |
. . . . 5
                                
  
                             |
29 | 28 | imbi2d 322 |
. . . 4
  
                              
                                   |
30 | | eleq1 2528 |
. . . . . 6


   |
31 | | suceq 5511 |
. . . . . . . 8

  |
32 | 31 | fveq2d 5896 |
. . . . . . 7

  
       |
33 | 31 | fveq2d 5896 |
. . . . . . 7

  
       |
34 | | fveq2 5892 |
. . . . . . . . 9

          |
35 | 34 | oveq2d 6336 |
. . . . . . . 8

              |
36 | 34 | fveq2d 5896 |
. . . . . . . 8

                  |
37 | 35, 36 | oveq12d 6338 |
. . . . . . 7

                                  |
38 | 32, 33, 37 | f1oeq123d 5838 |
. . . . . 6

         
                           
                      |
39 | 30, 38 | imbi12d 326 |
. . . . 5

                                                                |
40 | | eleq1 2528 |
. . . . . 6
     |
41 | | suceq 5511 |
. . . . . . . 8

  |
42 | 41 | fveq2d 5896 |
. . . . . . 7
           |
43 | 41 | fveq2d 5896 |
. . . . . . 7
           |
44 | | fveq2 5892 |
. . . . . . . . 9
           |
45 | 44 | oveq2d 6336 |
. . . . . . . 8
               |
46 | 44 | fveq2d 5896 |
. . . . . . . 8
                   |
47 | 45, 46 | oveq12d 6338 |
. . . . . . 7
                                   |
48 | 42, 43, 47 | f1oeq123d 5838 |
. . . . . 6
                                                             |
49 | 40, 48 | imbi12d 326 |
. . . . 5
                                
  
                             |
50 | | eleq1 2528 |
. . . . . 6
 
   |
51 | | suceq 5511 |
. . . . . . . 8
   |
52 | 51 | fveq2d 5896 |
. . . . . . 7
           |
53 | 51 | fveq2d 5896 |
. . . . . . 7
           |
54 | | fveq2 5892 |
. . . . . . . . 9
       
   |
55 | 54 | oveq2d 6336 |
. . . . . . . 8
               |
56 | 54 | fveq2d 5896 |
. . . . . . . 8
                   |
57 | 55, 56 | oveq12d 6338 |
. . . . . . 7
                                   |
58 | 52, 53, 57 | f1oeq123d 5838 |
. . . . . 6
                                                             |
59 | 50, 58 | imbi12d 326 |
. . . . 5
  
  
                                   
                       |
60 | 5 | adantr 471 |
. . . . . . 7
 

  |
61 | 12 | adantr 471 |
. . . . . . 7
 

    |
62 | | cnfcom.h |
. . . . . . 7
seq𝜔  

     |
63 | | cnfcom.t |
. . . . . . 7
seq𝜔  
    |
64 | | cnfcom.m |
. . . . . . 7
                 |
65 | | cnfcom.k |
. . . . . . 7
            |
66 | | simpr 467 |
. . . . . . 7
 

  |
67 | 3 | a1i 11 |
. . . . . . . 8
 

  |
68 | | suppssdm 6959 |
. . . . . . . . . . 11
 supp 
 |
69 | 2, 4, 5 | cantnfs 8202 |
. . . . . . . . . . . . . 14
       finSupp     |
70 | 14, 69 | mpbid 215 |
. . . . . . . . . . . . 13
      finSupp
   |
71 | 70 | simpld 465 |
. . . . . . . . . . . 12
       |
72 | | fdm 5760 |
. . . . . . . . . . . 12
       |
73 | 71, 72 | syl 17 |
. . . . . . . . . . 11
   |
74 | 68, 73 | syl5sseq 3492 |
. . . . . . . . . 10
  supp    |
75 | | onss 6649 |
. . . . . . . . . . 11
   |
76 | 5, 75 | syl 17 |
. . . . . . . . . 10

  |
77 | 74, 76 | sstrd 3454 |
. . . . . . . . 9
  supp    |
78 | 6 | oif 8076 |
. . . . . . . . . 10
     supp   |
79 | 78 | ffvelrni 6049 |
. . . . . . . . 9
      supp    |
80 | | ssel2 3439 |
. . . . . . . . 9
   supp       supp         |
81 | 77, 79, 80 | syl2an 484 |
. . . . . . . 8
 

      |
82 | | peano1 6744 |
. . . . . . . . 9
 |
83 | 82 | a1i 11 |
. . . . . . . 8
 

  |
84 | | oen0 7318 |
. . . . . . . 8
                 |
85 | 67, 81, 83, 84 | syl21anc 1275 |
. . . . . . 7
 

        |
86 | | 0ex 4551 |
. . . . . . . . 9
 |
87 | 63 | seqom0g 7204 |
. . . . . . . . 9

      |
88 | 86, 87 | ax-mp 5 |
. . . . . . . 8
     |
89 | | f1o0 5876 |
. . . . . . . . . 10
     |
90 | 62 | seqom0g 7204 |
. . . . . . . . . . 11

      |
91 | | f1oeq2 5833 |
. . . . . . . . . . 11
             
       |
92 | 86, 90, 91 | mp2b 10 |
. . . . . . . . . 10
        
      |
93 | 89, 92 | mpbir 214 |
. . . . . . . . 9
         |
94 | | f1oeq1 5832 |
. . . . . . . . 9
                 
           |
95 | 93, 94 | mpbiri 241 |
. . . . . . . 8
                   |
96 | 88, 95 | mp1i 13 |
. . . . . . 7
 

              |
97 | 2, 60, 61, 7, 6, 62, 63, 64, 65, 66, 85, 96 | cnfcomlem 8235 |
. . . . . 6
 

                              |
98 | 97 | ex 440 |
. . . . 5
 
                               |
99 | 6 | oicl 8075 |
. . . . . . . . . 10
 |
100 | | ordtr 5460 |
. . . . . . . . . 10

  |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . 9
 |
102 | | trsuc 5530 |
. . . . . . . . 9
 

  |
103 | 101, 102 | mpan 681 |
. . . . . . . 8
   |
104 | 103 | imim1i 60 |
. . . . . . 7
                              

                               |
105 | 5 | ad2antrr 737 |
. . . . . . . . . 10
    
                                |
106 | 12 | ad2antrr 737 |
. . . . . . . . . 10
    
                                  |
107 | | simprl 769 |
. . . . . . . . . 10
    
                             
  |
108 | 76 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
    
                                |
109 | 74 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    
                               supp    |
110 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
      supp    |
111 | 110 | ad2antrl 739 |
. . . . . . . . . . . . . . . 16
    
                                   supp    |
112 | 109, 111 | sseldd 3445 |
. . . . . . . . . . . . . . 15
    
                                    |
113 | 108, 112 | sseldd 3445 |
. . . . . . . . . . . . . 14
    
                                    |
114 | | eloni 5456 |
. . . . . . . . . . . . . 14
           |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . 13
    
                                    |
116 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
117 | 116 | sucid 5525 |
. . . . . . . . . . . . . 14
 |
118 | 5, 74 | ssexd 4566 |
. . . . . . . . . . . . . . . . . 18
  supp    |
119 | 15 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
  supp    |
120 | 6 | oiiso 8083 |
. . . . . . . . . . . . . . . . . 18
   supp 

supp      supp
    |
121 | 118, 119,
120 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17

   supp     |
122 | 121 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    
                                 supp     |
123 | 103 | ad2antrl 739 |
. . . . . . . . . . . . . . . 16
    
                                |
124 | | isorel 6247 |
. . . . . . . . . . . . . . . 16
 
   supp      
           |
125 | 122, 123,
107, 124 | syl12anc 1274 |
. . . . . . . . . . . . . . 15
    
                                          |
126 | 116 | sucex 6670 |
. . . . . . . . . . . . . . . 16
 |
127 | 126 | epelc 4769 |
. . . . . . . . . . . . . . 15

  |
128 | | fvex 5902 |
. . . . . . . . . . . . . . . 16
  
  |
129 | 128 | epelc 4769 |
. . . . . . . . . . . . . . 15
        
          |
130 | 125, 127,
129 | 3bitr3g 295 |
. . . . . . . . . . . . . 14
    
                                          |
131 | 117, 130 | mpbii 216 |
. . . . . . . . . . . . 13
    
                                        |
132 | | ordsucss 6677 |
. . . . . . . . . . . . 13
            
            |
133 | 115, 131,
132 | sylc 62 |
. . . . . . . . . . . 12
    
                                        |
134 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
      supp    |
135 | 123, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
    
                                   supp    |
136 | 109, 135 | sseldd 3445 |
. . . . . . . . . . . . . . 15
    
                                    |
137 | 108, 136 | sseldd 3445 |
. . . . . . . . . . . . . 14
    
                                    |
138 | | suceloni 6672 |
. . . . . . . . . . . . . 14
           |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . 13
    
                                    |
140 | 3 | a1i 11 |
. . . . . . . . . . . . 13
    
                                |
141 | 82 | a1i 11 |
. . . . . . . . . . . . 13
    
                                |
142 | | oewordi 7323 |
. . . . . . . . . . . . 13
         
 
                         |
143 | 139, 113,
140, 141, 142 | syl31anc 1279 |
. . . . . . . . . . . 12
    
                                  
         
         |
144 | 133, 143 | mpd 15 |
. . . . . . . . . . 11
    
                                            |
145 | 71 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
                                    |
146 | 145, 136 | ffvelrnd 6051 |
. . . . . . . . . . . . 13
    
                                        |
147 | | nnon 6730 |
. . . . . . . . . . . . . . 15
                   |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
    
                                        |
149 | | oecl 7270 |
. . . . . . . . . . . . . . 15
               |
150 | 140, 137,
149 | syl2anc 671 |
. . . . . . . . . . . . . 14
    
                                      |
151 | | oen0 7318 |
. . . . . . . . . . . . . . 15
        
        |
152 | 140, 137,
141, 151 | syl21anc 1275 |
. . . . . . . . . . . . . 14
    
                                      |
153 | | omord2 7299 |
. . . . . . . . . . . . . 14
                        
                                    |
154 | 148, 140,
150, 152, 153 | syl31anc 1279 |
. . . . . . . . . . . . 13
    
                                      
                           |
155 | 146, 154 | mpbid 215 |
. . . . . . . . . . . 12
    
                                                        |
156 | | oesuc 7260 |
. . . . . . . . . . . . 13
                       |
157 | 140, 137,
156 | syl2anc 671 |
. . . . . . . . . . . 12
    
                                              |
158 | 155, 157 | eleqtrrd 2543 |
. . . . . . . . . . 11
    
                                                      |
159 | 144, 158 | sseldd 3445 |
. . . . . . . . . 10
    
                                                      |
160 | | simprr 771 |
. . . . . . . . . 10
    
                                                            |
161 | 2, 105, 106, 7, 6, 62, 63, 64, 65, 107, 159, 160 | cnfcomlem 8235 |
. . . . . . . . 9
    
                                      
                     |
162 | 161 | exp32 614 |
. . . . . . . 8
 


                                                             |
163 | 162 | a2d 29 |
. . . . . . 7
 

 
                            

                                |
164 | 104, 163 | syl5 33 |
. . . . . 6
 

                              

                                |
165 | 164 | expcom 441 |
. . . . 5
                                

                                 |
166 | 39, 49, 59, 98, 165 | finds2 6753 |
. . . 4
  
  
                             |
167 | 29, 166 | vtoclga 3125 |
. . 3
  
  
                             |
168 | 18, 167 | mpcom 37 |
. 2
                                 |
169 | 1, 168 | mpd 15 |
1
                               |