Step | Hyp | Ref
| Expression |
1 | | ismkvmap 7145 |
. 2
 
Markov      
             |
2 | | nfv 1528 |
. . . . . . . . 9

 |
3 | | nfcv 2319 |
. . . . . . . . . 10
     |
4 | | nfra1 2508 |
. . . . . . . . . . . 12
  
     |
5 | 4 | nfn 1658 |
. . . . . . . . . . 11
       |
6 | | nfre1 2520 |
. . . . . . . . . . 11
  
     |
7 | 5, 6 | nfim 1572 |
. . . . . . . . . 10
   
           |
8 | 3, 7 | nfralxy 2515 |
. . . . . . . . 9
  
                |
9 | 2, 8 | nfan 1565 |
. . . . . . . 8
        
            |
10 | | nfv 1528 |
. . . . . . . 8

      |
11 | 9, 10 | nfan 1565 |
. . . . . . 7
         
   

             |
12 | | ismkvnnlem.g |
. . . . . . . . . . . 12
frec        |
13 | 12 | frechashgf1o 10401 |
. . . . . . . . . . 11
     |
14 | | 0nn0 9167 |
. . . . . . . . . . . . 13
 |
15 | | 1nn0 9168 |
. . . . . . . . . . . . 13
 |
16 | | prssi 3749 |
. . . . . . . . . . . . 13
 
   
  |
17 | 14, 15, 16 | mp2an 426 |
. . . . . . . . . . . 12
    |
18 | | elmapi 6663 |
. . . . . . . . . . . . . 14
               |
19 | 18 | ad2antlr 489 |
. . . . . . . . . . . . 13
         
   

                      |
20 | | simpr 110 |
. . . . . . . . . . . . 13
         
   

               |
21 | 19, 20 | ffvelcdmd 5647 |
. . . . . . . . . . . 12
         
   

                      |
22 | 17, 21 | sselid 3153 |
. . . . . . . . . . 11
         
   

                   |
23 | | f1ocnvfv2 5772 |
. . . . . . . . . . 11
                              |
24 | 13, 22, 23 | sylancr 414 |
. . . . . . . . . 10
         
   

                                |
25 | 24 | adantr 276 |
. . . . . . . . 9
     
               
      
  
                        |
26 | | fvco3 5582 |
. . . . . . . . . . . . . 14
        
                   |
27 | 19, 26 | sylancom 420 |
. . . . . . . . . . . . 13
         
   

                               |
28 | 27 | adantr 276 |
. . . . . . . . . . . 12
     
               
      
  
                       |
29 | | simpr 110 |
. . . . . . . . . . . 12
     
               
      
  
              |
30 | 28, 29 | eqtr3d 2212 |
. . . . . . . . . . 11
     
               
      
  
                |
31 | 30 | fveq2d 5514 |
. . . . . . . . . 10
     
               
      
  
                        |
32 | | df-1o 6410 |
. . . . . . . . . . . 12
 |
33 | 32 | fveq2i 5513 |
. . . . . . . . . . 11
         |
34 | | 0zd 9241 |
. . . . . . . . . . . . 13
  |
35 | | peano1 4589 |
. . . . . . . . . . . . . 14
 |
36 | 35 | a1i 9 |
. . . . . . . . . . . . 13
  |
37 | 34, 12, 36 | frec2uzsucd 10374 |
. . . . . . . . . . . 12
            |
38 | 37 | mptru 1362 |
. . . . . . . . . . 11
  
        |
39 | 34, 12 | frec2uz0d 10372 |
. . . . . . . . . . . . . 14
      |
40 | 39 | mptru 1362 |
. . . . . . . . . . . . 13
     |
41 | 40 | oveq1i 5878 |
. . . . . . . . . . . 12
         |
42 | | 0p1e1 9009 |
. . . . . . . . . . . 12
   |
43 | 41, 42 | eqtri 2198 |
. . . . . . . . . . 11
       |
44 | 33, 38, 43 | 3eqtri 2202 |
. . . . . . . . . 10
     |
45 | 31, 44 | eqtrdi 2226 |
. . . . . . . . 9
     
               
      
  
                    |
46 | 25, 45 | eqtr3d 2212 |
. . . . . . . 8
     
               
      
  
           |
47 | 46 | ex 115 |
. . . . . . 7
         
   

                            |
48 | 11, 47 | ralimdaa 2543 |
. . . . . 6
        
                
 
               |
49 | 48 | con3d 631 |
. . . . 5
        
                
                 |
50 | | fveq1 5509 |
. . . . . . . . . 10
                 |
51 | 50 | eqeq1d 2186 |
. . . . . . . . 9
        
  
       |
52 | 51 | ralbidv 2477 |
. . . . . . . 8
     
   

  
       |
53 | 52 | notbid 667 |
. . . . . . 7
         

  
       |
54 | 50 | eqeq1d 2186 |
. . . . . . . 8
        
  
       |
55 | 54 | rexbidv 2478 |
. . . . . . 7
     
   

  
       |
56 | 53, 55 | imbi12d 234 |
. . . . . 6
      
         
                     |
57 | | simplr 528 |
. . . . . 6
        
                
     
   

       |
58 | 12 | 012of 14367 |
. . . . . . . 8
 
            |
59 | 18 | adantl 277 |
. . . . . . . 8
        
                
         |
60 | | fco2 5377 |
. . . . . . . 8
                                |
61 | 58, 59, 60 | sylancr 414 |
. . . . . . 7
        
                
 
       |
62 | | 2onn 6515 |
. . . . . . . . 9
 |
63 | 62 | a1i 9 |
. . . . . . . 8
        
                
  |
64 | | simpll 527 |
. . . . . . . 8
        
                
  |
65 | 63, 64 | elmapd 6655 |
. . . . . . 7
        
                
  
  
 
        |
66 | 61, 65 | mpbird 167 |
. . . . . 6
        
                
 
     |
67 | 56, 57, 66 | rspcdva 2846 |
. . . . 5
        
                
                    |
68 | 24 | adantr 276 |
. . . . . . . 8
     
               
      
  
                        |
69 | 27 | eqeq1d 2186 |
. . . . . . . . . . 11
         
   

                    
            |
70 | 69 | biimpa 296 |
. . . . . . . . . 10
     
               
      
  
                |
71 | 70 | fveq2d 5514 |
. . . . . . . . 9
     
               
      
  
                        |
72 | 71, 40 | eqtrdi 2226 |
. . . . . . . 8
     
               
      
  
                    |
73 | 68, 72 | eqtr3d 2212 |
. . . . . . 7
     
               
      
  
           |
74 | 73 | exp31 364 |
. . . . . 6
        
                

                |
75 | 11, 74 | reximdai 2575 |
. . . . 5
        
                
 
       
       |
76 | 49, 67, 75 | 3syld 57 |
. . . 4
        
                
      
       |
77 | 76 | ralrimiva 2550 |
. . 3
                           
            |
78 | | nfcv 2319 |
. . . . . . . . . 10
        |
79 | | nfra1 2508 |
. . . . . . . . . . . 12
  
     |
80 | 79 | nfn 1658 |
. . . . . . . . . . 11
       |
81 | | nfre1 2520 |
. . . . . . . . . . 11
  
     |
82 | 80, 81 | nfim 1572 |
. . . . . . . . . 10
   
           |
83 | 78, 82 | nfralxy 2515 |
. . . . . . . . 9
  
       
           |
84 | 2, 83 | nfan 1565 |
. . . . . . . 8
           
            |
85 | | nfv 1528 |
. . . . . . . 8

   |
86 | 84, 85 | nfan 1565 |
. . . . . . 7
            
    
          |
87 | | elmapi 6663 |
. . . . . . . . . . . . . 14
         |
88 | 87 | ad2antlr 489 |
. . . . . . . . . . . . 13
            
    
                |
89 | | omelon 4604 |
. . . . . . . . . . . . . . . 16
 |
90 | 89 | onelssi 4425 |
. . . . . . . . . . . . . . 15
   |
91 | 62, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
 |
92 | 91 | a1i 9 |
. . . . . . . . . . . . 13
            
    
            |
93 | 88, 92 | fssd 5373 |
. . . . . . . . . . . 12
            
    
                |
94 | | simpr 110 |
. . . . . . . . . . . 12
            
    
            |
95 | 93, 94 | ffvelcdmd 5647 |
. . . . . . . . . . 11
            
    
                |
96 | | f1ocnvfv1 5771 |
. . . . . . . . . . 11
                              |
97 | 13, 95, 96 | sylancr 414 |
. . . . . . . . . 10
            
    
                             |
98 | 97 | adantr 276 |
. . . . . . . . 9
     
                                                 |
99 | | fvco3 5582 |
. . . . . . . . . . . . . 14
     
                 |
100 | 88, 99 | sylancom 420 |
. . . . . . . . . . . . 13
            
    
                          |
101 | 100 | eqeq1d 2186 |
. . . . . . . . . . . 12
            
    
                            |
102 | 101 | biimpa 296 |
. . . . . . . . . . 11
     
                                        |
103 | 102 | fveq2d 5514 |
. . . . . . . . . 10
     
                                                  |
104 | | 1onn 6514 |
. . . . . . . . . . . 12
 |
105 | | f1ocnvfv 5773 |
. . . . . . . . . . . 12
      
             |
106 | 13, 104, 105 | mp2an 426 |
. . . . . . . . . . 11
            |
107 | 44, 106 | ax-mp 5 |
. . . . . . . . . 10
      |
108 | 103, 107 | eqtrdi 2226 |
. . . . . . . . 9
     
                                             |
109 | 98, 108 | eqtr3d 2212 |
. . . . . . . 8
     
                                    |
110 | 109 | ex 115 |
. . . . . . 7
            
    
                        |
111 | 86, 110 | ralimdaa 2543 |
. . . . . 6
           
               
      
       |
112 | 111 | con3d 631 |
. . . . 5
           
                              |
113 | | fveq1 5509 |
. . . . . . . . . 10
               |
114 | 113 | eqeq1d 2186 |
. . . . . . . . 9
                 |
115 | 114 | ralbidv 2477 |
. . . . . . . 8
    
    
         |
116 | 115 | notbid 667 |
. . . . . . 7
                   |
117 | 113 | eqeq1d 2186 |
. . . . . . . 8
                 |
118 | 117 | rexbidv 2478 |
. . . . . . 7
    
    
         |
119 | 116, 118 | imbi12d 234 |
. . . . . 6
     
           
 
               |
120 | | simplr 528 |
. . . . . 6
           
                      
    
       |
121 | 12 | 2o01f 14368 |
. . . . . . . 8
          |
122 | 87 | adantl 277 |
. . . . . . . 8
           
                    |
123 | | fco2 5377 |
. . . . . . . 8
                           |
124 | 121, 122,
123 | sylancr 414 |
. . . . . . 7
           
              
          |
125 | | prexg 4207 |
. . . . . . . . . 10
 
      |
126 | 14, 15, 125 | mp2an 426 |
. . . . . . . . 9
    |
127 | 126 | a1i 9 |
. . . . . . . 8
           
                   |
128 | | simpll 527 |
. . . . . . . 8
           
                |
129 | 127, 128 | elmapd 6655 |
. . . . . . 7
           
                     
            |
130 | 124, 129 | mpbird 167 |
. . . . . 6
           
              
        |
131 | 119, 120,
130 | rspcdva 2846 |
. . . . 5
           
                      
         |
132 | 97 | adantr 276 |
. . . . . . . 8
     
                                                 |
133 | 100 | eqeq1d 2186 |
. . . . . . . . . . 11
            
    
                            |
134 | 133 | biimpa 296 |
. . . . . . . . . 10
     
                                        |
135 | 134 | fveq2d 5514 |
. . . . . . . . 9
     
                                                  |
136 | | f1ocnvfv 5773 |
. . . . . . . . . . 11
                    |
137 | 13, 35, 136 | mp2an 426 |
. . . . . . . . . 10
    
       |
138 | 40, 137 | ax-mp 5 |
. . . . . . . . 9
      |
139 | 135, 138 | eqtrdi 2226 |
. . . . . . . 8
     
                                             |
140 | 132, 139 | eqtr3d 2212 |
. . . . . . 7
     
                                    |
141 | 140 | exp31 364 |
. . . . . 6
           
                              |
142 | 86, 141 | reximdai 2575 |
. . . . 5
           
               
      
       |
143 | 112, 131,
142 | 3syld 57 |
. . . 4
           
                            |
144 | 143 | ralrimiva 2550 |
. . 3
                     
     
   

       |
145 | 77, 144 | impbida 596 |
. 2
  
              
        
    
        |
146 | 1, 145 | bitrd 188 |
1
 
Markov         
             |