Step | Hyp | Ref
| Expression |
1 | | iswomninn 14837 |
. 2
 
WOmni       DECID 
       |
2 | | simpr 110 |
. . . . . . . . . . . 12
                      |
3 | 2 | oveq2d 5893 |
. . . . . . . . . . 11
                          |
4 | | 1m0e1 9034 |
. . . . . . . . . . 11
   |
5 | 3, 4 | eqtrdi 2226 |
. . . . . . . . . 10
                        |
6 | | 1ex 7954 |
. . . . . . . . . . 11
 |
7 | 6 | prid2 3701 |
. . . . . . . . . 10
    |
8 | 5, 7 | eqeltrdi 2268 |
. . . . . . . . 9
                           |
9 | | simpr 110 |
. . . . . . . . . . . 12
                      |
10 | 9 | oveq2d 5893 |
. . . . . . . . . . 11
                          |
11 | | 1m1e0 8990 |
. . . . . . . . . . 11
   |
12 | 10, 11 | eqtrdi 2226 |
. . . . . . . . . 10
                        |
13 | | c0ex 7953 |
. . . . . . . . . . 11
 |
14 | 13 | prid1 3700 |
. . . . . . . . . 10
    |
15 | 12, 14 | eqeltrdi 2268 |
. . . . . . . . 9
                           |
16 | | elmapi 6672 |
. . . . . . . . . . . 12
               |
17 | 16 | ad2antlr 489 |
. . . . . . . . . . 11
  
                |
18 | | simpr 110 |
. . . . . . . . . . 11
  
         |
19 | 17, 18 | ffvelcdmd 5654 |
. . . . . . . . . 10
  
                |
20 | | elpri 3617 |
. . . . . . . . . 10
                    |
21 | 19, 20 | syl 14 |
. . . . . . . . 9
  
                   |
22 | 8, 15, 21 | mpjaodan 798 |
. . . . . . . 8
  
                  |
23 | 22 | fmpttd 5673 |
. . . . . . 7
 
                       |
24 | | 0nn0 9193 |
. . . . . . . . . 10
 |
25 | | 1nn0 9194 |
. . . . . . . . . 10
 |
26 | | prexg 4213 |
. . . . . . . . . 10
 
      |
27 | 24, 25, 26 | mp2an 426 |
. . . . . . . . 9
    |
28 | 27 | a1i 9 |
. . . . . . . 8
 
           |
29 | | simpl 109 |
. . . . . . . 8
 
        |
30 | 28, 29 | elmapd 6664 |
. . . . . . 7
 
                   

                 |
31 | 23, 30 | mpbird 167 |
. . . . . 6
 
                     |
32 | | fveq1 5516 |
. . . . . . . . . 10
                           |
33 | 32 | eqeq1d 2186 |
. . . . . . . . 9
                             |
34 | 33 | ralbidv 2477 |
. . . . . . . 8
               
               |
35 | 34 | dcbid 838 |
. . . . . . 7
         DECID 
    DECID

               |
36 | 35 | rspcv 2839 |
. . . . . 6
                     DECID 
    DECID 
               |
37 | 31, 36 | syl 14 |
. . . . 5
 
             DECID 
    DECID 
               |
38 | | eqid 2177 |
. . . . . . . . . . 11
                 |
39 | | fveq2 5517 |
. . . . . . . . . . . 12
           |
40 | 39 | oveq2d 5893 |
. . . . . . . . . . 11
               |
41 | | simpr 110 |
. . . . . . . . . . 11
  
         |
42 | 22 | ralrimiva 2550 |
. . . . . . . . . . . . 13
 
                  |
43 | 40 | eleq1d 2246 |
. . . . . . . . . . . . . 14
          
            |
44 | 43 | cbvralv 2705 |
. . . . . . . . . . . . 13
 
        

           |
45 | 42, 44 | sylib 122 |
. . . . . . . . . . . 12
 
                  |
46 | 45 | r19.21bi 2565 |
. . . . . . . . . . 11
  
                  |
47 | 38, 40, 41, 46 | fvmptd3 5611 |
. . . . . . . . . 10
  
                           |
48 | 47 | eqeq1d 2186 |
. . . . . . . . 9
  
                             |
49 | | 1cnd 7975 |
. . . . . . . . . 10
  
         |
50 | | 0z 9266 |
. . . . . . . . . . . . 13
 |
51 | | 1z 9281 |
. . . . . . . . . . . . 13
 |
52 | | prssi 3752 |
. . . . . . . . . . . . 13
 
   
  |
53 | 50, 51, 52 | mp2an 426 |
. . . . . . . . . . . 12
    |
54 | 16 | adantl 277 |
. . . . . . . . . . . . 13
 
               |
55 | 54 | ffvelcdmda 5653 |
. . . . . . . . . . . 12
  
                |
56 | 53, 55 | sselid 3155 |
. . . . . . . . . . 11
  
             |
57 | 56 | zcnd 9378 |
. . . . . . . . . 10
  
             |
58 | | subsub23 8164 |
. . . . . . . . . 10
     
                 |
59 | 49, 57, 49, 58 | syl3anc 1238 |
. . . . . . . . 9
  
                       |
60 | 48, 59 | bitrd 188 |
. . . . . . . 8
  
                             |
61 | 11 | eqeq1i 2185 |
. . . . . . . . 9
      
      |
62 | | eqcom 2179 |
. . . . . . . . 9
    
      |
63 | 61, 62 | bitri 184 |
. . . . . . . 8
      
      |
64 | 60, 63 | bitrdi 196 |
. . . . . . 7
  
                           |
65 | 64 | ralbidva 2473 |
. . . . . 6
 
       
           

       |
66 | 65 | dcbid 838 |
. . . . 5
 
      DECID              DECID 
       |
67 | 37, 66 | sylibd 149 |
. . . 4
 
             DECID 
    DECID 
       |
68 | 67 | ralrimdva 2557 |
. . 3
  
     DECID 
          DECID 
       |
69 | | simpr 110 |
. . . . . . . . . . . 12
                      |
70 | 69 | oveq2d 5893 |
. . . . . . . . . . 11
                          |
71 | 70, 4 | eqtrdi 2226 |
. . . . . . . . . 10
                        |
72 | 71, 7 | eqeltrdi 2268 |
. . . . . . . . 9
                           |
73 | | simpr 110 |
. . . . . . . . . . . 12
                      |
74 | 73 | oveq2d 5893 |
. . . . . . . . . . 11
                          |
75 | 74, 11 | eqtrdi 2226 |
. . . . . . . . . 10
                        |
76 | 75, 14 | eqeltrdi 2268 |
. . . . . . . . 9
                           |
77 | | elmapi 6672 |
. . . . . . . . . . . 12
               |
78 | 77 | adantl 277 |
. . . . . . . . . . 11
 
               |
79 | 78 | ffvelcdmda 5653 |
. . . . . . . . . 10
  
                |
80 | | elpri 3617 |
. . . . . . . . . 10
                    |
81 | 79, 80 | syl 14 |
. . . . . . . . 9
  
                   |
82 | 72, 76, 81 | mpjaodan 798 |
. . . . . . . 8
  
                  |
83 | 82 | fmpttd 5673 |
. . . . . . 7
 
                       |
84 | 27 | a1i 9 |
. . . . . . . 8
 
           |
85 | | simpl 109 |
. . . . . . . 8
 
        |
86 | 84, 85 | elmapd 6664 |
. . . . . . 7
 
                   

                 |
87 | 83, 86 | mpbird 167 |
. . . . . 6
 
                     |
88 | | fveq1 5516 |
. . . . . . . . . 10
                           |
89 | 88 | eqeq1d 2186 |
. . . . . . . . 9
                             |
90 | 89 | ralbidv 2477 |
. . . . . . . 8
               
               |
91 | 90 | dcbid 838 |
. . . . . . 7
         DECID 
    DECID

               |
92 | 91 | rspcv 2839 |
. . . . . 6
                     DECID 
    DECID 
               |
93 | 87, 92 | syl 14 |
. . . . 5
 
             DECID 
    DECID 
               |
94 | | eqid 2177 |
. . . . . . . . . . 11
                 |
95 | | fveq2 5517 |
. . . . . . . . . . . 12
           |
96 | 95 | oveq2d 5893 |
. . . . . . . . . . 11
               |
97 | | simpr 110 |
. . . . . . . . . . 11
  
         |
98 | 82 | ralrimiva 2550 |
. . . . . . . . . . . . 13
 
                  |
99 | 96 | eleq1d 2246 |
. . . . . . . . . . . . . 14
          
            |
100 | 99 | cbvralv 2705 |
. . . . . . . . . . . . 13
 
        

           |
101 | 98, 100 | sylib 122 |
. . . . . . . . . . . 12
 
                  |
102 | 101 | r19.21bi 2565 |
. . . . . . . . . . 11
  
                  |
103 | 94, 96, 97, 102 | fvmptd3 5611 |
. . . . . . . . . 10
  
                           |
104 | 103 | eqeq1d 2186 |
. . . . . . . . 9
  
                             |
105 | | 1cnd 7975 |
. . . . . . . . . 10
  
         |
106 | 78 | ffvelcdmda 5653 |
. . . . . . . . . . . 12
  
                |
107 | 53, 106 | sselid 3155 |
. . . . . . . . . . 11
  
             |
108 | 107 | zcnd 9378 |
. . . . . . . . . 10
  
             |
109 | | 0cnd 7952 |
. . . . . . . . . 10
  
         |
110 | | subsub23 8164 |
. . . . . . . . . 10
     
                 |
111 | 105, 108,
109, 110 | syl3anc 1238 |
. . . . . . . . 9
  
                       |
112 | 104, 111 | bitrd 188 |
. . . . . . . 8
  
                             |
113 | 4 | eqeq1i 2185 |
. . . . . . . . 9
      
      |
114 | | eqcom 2179 |
. . . . . . . . 9
    
      |
115 | 113, 114 | bitri 184 |
. . . . . . . 8
      
      |
116 | 112, 115 | bitrdi 196 |
. . . . . . 7
  
                           |
117 | 116 | ralbidva 2473 |
. . . . . 6
 
       
           

       |
118 | 117 | dcbid 838 |
. . . . 5
 
      DECID              DECID 
       |
119 | 93, 118 | sylibd 149 |
. . . 4
 
             DECID 
    DECID 
       |
120 | 119 | ralrimdva 2557 |
. . 3
  
     DECID 
          DECID 
       |
121 | 68, 120 | impbid 129 |
. 2
  
     DECID 
   
      DECID 
       |
122 | 1, 121 | bitrd 188 |
1
 
WOmni       DECID 
       |