Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
 CNF   |
2 | | cantnfs.a |
. . 3
   |
3 | | cantnfs.b |
. . 3
   |
4 | | oemapval.t |
. . 3
   

        


            |
5 | 1, 2, 3, 4 | oemapso 8213 |
. 2
   |
6 | | oecl 7265 |
. . . . 5
 
     |
7 | 2, 3, 6 | syl2anc 671 |
. . . 4
     |
8 | | eloni 5452 |
. . . 4
   
   |
9 | 7, 8 | syl 17 |
. . 3
     |
10 | | ordwe 5455 |
. . 3
  

   |
11 | | weso 4844 |
. . 3
      |
12 | | sopo 4791 |
. . 3
      |
13 | 9, 10, 11, 12 | 4syl 19 |
. 2
     |
14 | 1, 2, 3 | cantnff 8205 |
. . 3
  CNF          |
15 | | frn 5758 |
. . . . 5
  CNF        
CNF      |
16 | 14, 15 | syl 17 |
. . . 4
  CNF 
    |
17 | | onss 6644 |
. . . . . . . 8
       |
18 | 7, 17 | syl 17 |
. . . . . . 7
  
  |
19 | 18 | sseld 3443 |
. . . . . 6
       |
20 | | eleq1 2528 |
. . . . . . . . . 10
   

    |
21 | | eleq1 2528 |
. . . . . . . . . 10
   CNF 
 CNF     |
22 | 20, 21 | imbi12d 326 |
. . . . . . . . 9
     
CNF     
 CNF      |
23 | 22 | imbi2d 322 |
. . . . . . . 8
  
    CNF   
    
CNF       |
24 | | r19.21v 2805 |
. . . . . . . . 9
 
   
 CNF   
     
CNF      |
25 | | ordelss 5458 |
. . . . . . . . . . . . . . . . . . 19
           |
26 | 9, 25 | sylan 478 |
. . . . . . . . . . . . . . . . . 18
 

 

   |
27 | 26 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
           |
28 | | pm5.5 342 |
. . . . . . . . . . . . . . . . 17
       
CNF   
CNF     |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
           
CNF   
CNF     |
30 | 29 | ralbidva 2836 |
. . . . . . . . . . . . . . 15
 

 
 
    CNF  

 CNF     |
31 | | dfss3 3434 |
. . . . . . . . . . . . . . 15

 CNF    CNF    |
32 | 30, 31 | syl6bbr 271 |
. . . . . . . . . . . . . 14
 

 
 
    CNF  
 CNF     |
33 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16

  CNF 

CNF     |
34 | 2 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
 
  
 CNF      |
35 | 34 | adantr 471 |
. . . . . . . . . . . . . . . . 17
       CNF    
  |
36 | 3 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
 
  
 CNF      |
37 | 36 | adantr 471 |
. . . . . . . . . . . . . . . . 17
       CNF    
  |
38 | | simplrl 775 |
. . . . . . . . . . . . . . . . 17
       CNF         |
39 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
       CNF    
 CNF    |
40 | 7 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 CNF        |
41 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 CNF        |
42 | | onelon 5467 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
43 | 40, 41, 42 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
 
  
 CNF      |
44 | | on0eln0 5497 |
. . . . . . . . . . . . . . . . . . 19
 
   |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
  
 CNF    
   |
46 | 45 | biimpar 492 |
. . . . . . . . . . . . . . . . 17
       CNF       |
47 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
             |
48 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
        
                               
                        |
49 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
       
                  
                    
                         |
50 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
       
                  
                    
                         |
51 | 1, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50 | cantnflem4 8223 |
. . . . . . . . . . . . . . . 16
       CNF      CNF    |
52 | | fczsupp0 6971 |
. . . . . . . . . . . . . . . . . . . . 21
     supp   |
53 | 52 | eqcomi 2471 |
. . . . . . . . . . . . . . . . . . . 20
     supp   |
54 | | oieq2 8054 |
. . . . . . . . . . . . . . . . . . . 20
      supp 
OrdIso  OrdIso      supp     |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
OrdIso  OrdIso      supp    |
56 | | ne0i 3749 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
57 | | ne0i 3749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
58 | 57 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
 CNF        |
59 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  
   |
60 | 59 | neeq1d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

        |
61 | 58, 60 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  
 CNF    
     |
62 | 61 | necon2d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
 CNF      
   |
63 | | on0eln0 5497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
64 | | oe0m1 7249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
65 | 63, 64 | bitr3d 263 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
66 | 36, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
 CNF          |
67 | | on0eln0 5497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
68 | 34, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
 CNF    
   |
69 | 62, 66, 68 | 3imtr4d 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
 CNF    
   |
70 | 56, 69 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
 CNF        |
71 | 70 | imp 435 |
. . . . . . . . . . . . . . . . . . . . 21
       CNF    
  |
72 | | fconstmpt 4897 |
. . . . . . . . . . . . . . . . . . . . 21
       |
73 | 71, 72 | fmptd 6069 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 CNF              |
74 | | 0ex 4549 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
76 | 3, 75 | fczfsuppd 7927 |
. . . . . . . . . . . . . . . . . . . . 21
     finSupp
  |
77 | 76 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 CNF        finSupp   |
78 | 1, 2, 3 | cantnfs 8197 |
. . . . . . . . . . . . . . . . . . . . 21
               
   finSupp     |
79 | 78 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 CNF                      finSupp     |
80 | 73, 77, 79 | mpbir2and 938 |
. . . . . . . . . . . . . . . . . . 19
 
  
 CNF          |
81 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔      OrdIso             OrdIso
          seq𝜔      OrdIso             OrdIso            |
82 | 1, 34, 36, 55, 80, 81 | cantnfval 8199 |
. . . . . . . . . . . . . . . . . 18
 
  
 CNF      CNF         seq𝜔      OrdIso             OrdIso
            OrdIso     |
83 | | we0 4848 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
84 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . . . . 23
OrdIso  OrdIso   |
85 | 84 | oien 8079 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 OrdIso    |
86 | 74, 83, 85 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . 21
OrdIso   |
87 | | en0 7658 |
. . . . . . . . . . . . . . . . . . . . 21
 OrdIso
 OrdIso
   |
88 | 86, 87 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . 20
OrdIso   |
89 | 88 | fveq2i 5891 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔      OrdIso             OrdIso             OrdIso   seq𝜔      OrdIso             OrdIso
              |
90 | 81 | seqom0g 7199 |
. . . . . . . . . . . . . . . . . . . 20

seq𝜔      OrdIso             OrdIso
               |
91 | 74, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔      OrdIso             OrdIso               |
92 | 89, 91 | eqtri 2484 |
. . . . . . . . . . . . . . . . . 18
seq𝜔      OrdIso             OrdIso             OrdIso    |
93 | 82, 92 | syl6eq 2512 |
. . . . . . . . . . . . . . . . 17
 
  
 CNF      CNF           |
94 | 14 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
  
 CNF     CNF      
   |
95 | | ffn 5751 |
. . . . . . . . . . . . . . . . . . 19
  CNF         CNF    |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
  
 CNF     CNF    |
97 | | fnfvelrn 6042 |
. . . . . . . . . . . . . . . . . 18
   CNF         CNF          CNF    |
98 | 96, 80, 97 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
 
  
 CNF      CNF          CNF    |
99 | 93, 98 | eqeltrrd 2541 |
. . . . . . . . . . . . . . . 16
 
  
 CNF    
CNF    |
100 | 33, 51, 99 | pm2.61ne 2721 |
. . . . . . . . . . . . . . 15
 
  
 CNF     CNF    |
101 | 100 | expr 624 |
. . . . . . . . . . . . . 14
 

 
  CNF 
 CNF     |
102 | 32, 101 | sylbid 223 |
. . . . . . . . . . . . 13
 

 
 
    CNF    CNF     |
103 | 102 | ex 440 |
. . . . . . . . . . . 12
     
  
 CNF  
 CNF      |
104 | 103 | com23 81 |
. . . . . . . . . . 11
     
 CNF  
  
 CNF      |
105 | 104 | a2i 14 |
. . . . . . . . . 10
      
CNF       
 CNF      |
106 | 105 | a1i 11 |
. . . . . . . . 9
  

  
 CNF       
 CNF       |
107 | 24, 106 | syl5bi 225 |
. . . . . . . 8
  

    CNF    
    CNF       |
108 | 23, 107 | tfis2 6710 |
. . . . . . 7
    
 CNF      |
109 | 108 | com3l 84 |
. . . . . 6
    
 CNF      |
110 | 19, 109 | mpdd 41 |
. . . . 5
    
CNF     |
111 | 110 | ssrdv 3450 |
. . . 4
  
 CNF    |
112 | 16, 111 | eqssd 3461 |
. . 3
  CNF      |
113 | | dffo2 5820 |
. . 3
  CNF       
  CNF      
  CNF       |
114 | 14, 112, 113 | sylanbrc 675 |
. 2
  CNF          |
115 | 2 | adantr 471 |
. . . . . 6
 
 
    
  |
116 | 3 | adantr 471 |
. . . . . 6
 
 
    
  |
117 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
118 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
119 | 117, 118 | eleq12d 2534 |
. . . . . . . . . . 11
         
           |
120 | | eleq1 2528 |
. . . . . . . . . . . . 13
 
   |
121 | 120 | imbi1d 323 |
. . . . . . . . . . . 12
                         |
122 | 121 | ralbidv 2839 |
. . . . . . . . . . 11
  
          
             |
123 | 119, 122 | anbi12d 722 |
. . . . . . . . . 10
            
         
        


             |
124 | 123 | cbvrexv 3032 |
. . . . . . . . 9
                                  
            |
125 | | fveq1 5887 |
. . . . . . . . . . . 12
           |
126 | | fveq1 5887 |
. . . . . . . . . . . 12
           |
127 | | eleq12 2530 |
. . . . . . . . . . . 12
                                       |
128 | 125, 126,
127 | syl2an 484 |
. . . . . . . . . . 11
 
                     |
129 | | fveq1 5887 |
. . . . . . . . . . . . . 14
           |
130 | | fveq1 5887 |
. . . . . . . . . . . . . 14
           |
131 | 129, 130 | eqeqan12d 2478 |
. . . . . . . . . . . . 13
 
                     |
132 | 131 | imbi2d 322 |
. . . . . . . . . . . 12
 
  
         
            |
133 | 132 | ralbidv 2839 |
. . . . . . . . . . 11
 
   
                       |
134 | 128, 133 | anbi12d 722 |
. . . . . . . . . 10
 
          


         
        


             |
135 | 134 | rexbidv 2913 |
. . . . . . . . 9
 
           


         

        


             |
136 | 124, 135 | syl5bb 265 |
. . . . . . . 8
 
           


         

        


             |
137 | 136 | cbvopabv 4486 |
. . . . . . 7
    
                                     
            |
138 | 4, 137 | eqtri 2484 |
. . . . . 6
   

        


            |
139 | | simprll 777 |
. . . . . 6
 
 
    
  |
140 | | simprlr 778 |
. . . . . 6
 
 
    
  |
141 | | simprr 771 |
. . . . . 6
 
 
    
    |
142 | | eqid 2462 |
. . . . . 6
                       |
143 | | eqid 2462 |
. . . . . 6
OrdIso  supp   OrdIso  supp    |
144 | | eqid 2462 |
. . . . . 6
seq𝜔      OrdIso  supp          OrdIso  supp            seq𝜔      OrdIso  supp          OrdIso
 supp             |
145 | 1, 115, 116, 138, 139, 140, 141, 142, 143, 144 | cantnflem1 8220 |
. . . . 5
 
 
    
  CNF       CNF       |
146 | | fvex 5898 |
. . . . . 6
  CNF      |
147 | 146 | epelc 4766 |
. . . . 5
   CNF       CNF       CNF       CNF       |
148 | 145, 147 | sylibr 217 |
. . . 4
 
 
    
  CNF       CNF       |
149 | 148 | expr 624 |
. . 3
 

       CNF       CNF        |
150 | 149 | ralrimivva 2821 |
. 2
  
     CNF       CNF        |
151 | | soisoi 6244 |
. 2
        CNF       


     CNF       CNF         CNF    
     |
152 | 5, 13, 114, 150, 151 | syl22anc 1277 |
1
  CNF    
     |