Proof of Theorem oemapvali
Step | Hyp | Ref
| Expression |
1 | | oemapvali.r |
. . 3
     |
2 | | cantnfs.s |
. . . 4
 CNF   |
3 | | cantnfs.a |
. . . 4
   |
4 | | cantnfs.b |
. . . 4
   |
5 | | oemapval.t |
. . . 4
   

        


            |
6 | | oemapval.f |
. . . 4
   |
7 | | oemapval.g |
. . . 4
   |
8 | 2, 3, 4, 5, 6, 7 | oemapval 8206 |
. . 3
    
          
             |
9 | 1, 8 | mpbid 215 |
. 2
            
            |
10 | | ssrab2 3500 |
. . . 4
           |
11 | | oemapvali.x |
. . . . 5
            |
12 | 4 | adantr 472 |
. . . . . . . 8
 

                      
  |
13 | | onss 6636 |
. . . . . . . 8
   |
14 | 12, 13 | syl 17 |
. . . . . . 7
 

                         |
15 | 10, 14 | syl5ss 3429 |
. . . . . 6
 

                                
  |
16 | 2, 3, 4 | cantnfs 8189 |
. . . . . . . . . 10
       finSupp     |
17 | 7, 16 | mpbid 215 |
. . . . . . . . 9
      finSupp
   |
18 | 17 | simprd 470 |
. . . . . . . 8
 finSupp   |
19 | 18 | adantr 472 |
. . . . . . 7
 

                       finSupp   |
20 | 4 | 3ad2ant1 1051 |
. . . . . . . . . 10
 
        
  |
21 | | simp2 1031 |
. . . . . . . . . 10
 
        
  |
22 | 17 | simpld 466 |
. . . . . . . . . . . 12
       |
23 | | ffn 5739 |
. . . . . . . . . . . 12
    
  |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
   |
25 | 24 | 3ad2ant1 1051 |
. . . . . . . . . 10
 
        
  |
26 | | ne0i 3728 |
. . . . . . . . . . 11
               |
27 | 26 | 3ad2ant3 1053 |
. . . . . . . . . 10
 
        
      |
28 | | fvn0elsupp 6949 |
. . . . . . . . . 10
            supp    |
29 | 20, 21, 25, 27, 28 | syl22anc 1293 |
. . . . . . . . 9
 
        

supp    |
30 | 29 | rabssdv 3495 |
. . . . . . . 8
          
 supp    |
31 | 30 | adantr 472 |
. . . . . . 7
 

                                
 supp    |
32 | | fsuppimp 7907 |
. . . . . . . 8
 finSupp  
supp     |
33 | | ssfi 7810 |
. . . . . . . . . 10
   supp 

          supp               |
34 | 33 | ex 441 |
. . . . . . . . 9
  supp              supp               |
35 | 34 | adantl 473 |
. . . . . . . 8
   supp              
supp               |
36 | 32, 35 | syl 17 |
. . . . . . 7
 finSupp             supp               |
37 | 19, 31, 36 | sylc 61 |
. . . . . 6
 

                                   |
38 | | simprl 772 |
. . . . . . . 8
 

                         |
39 | | simprrl 782 |
. . . . . . . 8
 

                                 |
40 | | fveq2 5879 |
. . . . . . . . . 10
           |
41 | | fveq2 5879 |
. . . . . . . . . 10
           |
42 | 40, 41 | eleq12d 2543 |
. . . . . . . . 9
         
           |
43 | 42 | elrab 3184 |
. . . . . . . 8
          

           |
44 | 38, 39, 43 | sylanbrc 677 |
. . . . . . 7
 

                                   |
45 | | ne0i 3728 |
. . . . . . 7
                       |
46 | 44, 45 | syl 17 |
. . . . . 6
 

                                   |
47 | | ordunifi 7839 |
. . . . . 6
           
                                            |
48 | 15, 37, 46, 47 | syl3anc 1292 |
. . . . 5
 

                                              |
49 | 11, 48 | syl5eqel 2553 |
. . . 4
 

                      

           |
50 | 10, 49 | sseldi 3416 |
. . 3
 

                      
  |
51 | | fveq2 5879 |
. . . . . . 7
           |
52 | | fveq2 5879 |
. . . . . . 7
           |
53 | 51, 52 | eleq12d 2543 |
. . . . . 6
         
           |
54 | | fveq2 5879 |
. . . . . . . 8
           |
55 | | fveq2 5879 |
. . . . . . . 8
           |
56 | 54, 55 | eleq12d 2543 |
. . . . . . 7
         
           |
57 | 56 | cbvrabv 3030 |
. . . . . 6
          
          |
58 | 53, 57 | elrab2 3186 |
. . . . 5
          

           |
59 | 49, 58 | sylib 201 |
. . . 4
 

                                   |
60 | 59 | simprd 470 |
. . 3
 

                                 |
61 | | simprrr 783 |
. . . 4
 

                       
            |
62 | 3 | adantr 472 |
. . . . . . . . . . 11
 

                      
  |
63 | 22 | adantr 472 |
. . . . . . . . . . . 12
 

                             |
64 | 63, 50 | ffvelrnd 6038 |
. . . . . . . . . . 11
 

                             |
65 | | onelon 5455 |
. . . . . . . . . . 11
             |
66 | 62, 64, 65 | syl2anc 673 |
. . . . . . . . . 10
 

                             |
67 | | eloni 5440 |
. . . . . . . . . 10
           |
68 | | ordirr 5448 |
. . . . . . . . . 10
    
          |
69 | 66, 67, 68 | 3syl 18 |
. . . . . . . . 9
 

                                 |
70 | | nelneq 2573 |
. . . . . . . . 9
                  
          |
71 | 60, 69, 70 | syl2anc 673 |
. . . . . . . 8
 

                                 |
72 | | eleq2 2538 |
. . . . . . . . . . 11
 
   |
73 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
74 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
75 | 73, 74 | eqeq12d 2486 |
. . . . . . . . . . 11
         
           |
76 | 72, 75 | imbi12d 327 |
. . . . . . . . . 10
                         |
77 | 76 | rspccv 3133 |
. . . . . . . . 9
 
          

            |
78 | 61, 50, 77 | sylc 61 |
. . . . . . . 8
 

                                   |
79 | 71, 78 | mtod 182 |
. . . . . . 7
 

                      
  |
80 | | ssexg 4542 |
. . . . . . . . . . 11
           
             |
81 | 10, 12, 80 | sylancr 676 |
. . . . . . . . . 10
 

                                   |
82 | | ssonuni 6632 |
. . . . . . . . . 10
                     
              |
83 | 81, 15, 82 | sylc 61 |
. . . . . . . . 9
 

                                    |
84 | 11, 83 | syl5eqel 2553 |
. . . . . . . 8
 

                      
  |
85 | | onelon 5455 |
. . . . . . . . 9
 
   |
86 | 12, 38, 85 | syl2anc 673 |
. . . . . . . 8
 

                         |
87 | | ontri1 5464 |
. . . . . . . 8
 
     |
88 | 84, 86, 87 | syl2anc 673 |
. . . . . . 7
 

                           |
89 | 79, 88 | mpbird 240 |
. . . . . 6
 

                         |
90 | | elssuni 4219 |
. . . . . . . 8
                        |
91 | 90, 11 | syl6sseqr 3465 |
. . . . . . 7
             |
92 | 44, 91 | syl 17 |
. . . . . 6
 

                      
  |
93 | 89, 92 | eqssd 3435 |
. . . . 5
 

                      
  |
94 | | eleq1 2537 |
. . . . . . 7
 
   |
95 | 94 | imbi1d 324 |
. . . . . 6
                         |
96 | 95 | ralbidv 2829 |
. . . . 5
  

         
             |
97 | 93, 96 | syl 17 |
. . . 4
 

                         
                       |
98 | 61, 97 | mpbird 240 |
. . 3
 

                       

           |
99 | 50, 60, 98 | 3jca 1210 |
. 2
 

                                              |
100 | 9, 99 | rexlimddv 2875 |
1
                        |