Step | Hyp | Ref
| Expression |
1 | | nfv 1528 |
. . . . . . 7

Markov |
2 | | nfra1 2508 |
. . . . . . 7
  
DECID  |
3 | 1, 2 | nfan 1565 |
. . . . . 6
   Markov 
DECID
  |
4 | | simpr 110 |
. . . . . . . . 9
   Markov 
DECID

   |
5 | | 0lt2o 6435 |
. . . . . . . . . . . 12
 |
6 | 5 | a1i 9 |
. . . . . . . . . . 11
   DECID

  |
7 | | 1lt2o 6436 |
. . . . . . . . . . . 12
 |
8 | 7 | a1i 9 |
. . . . . . . . . . 11
   DECID
   |
9 | | rsp 2524 |
. . . . . . . . . . . 12
 
DECID
 DECID    |
10 | 9 | imp 124 |
. . . . . . . . . . 11
   DECID
 DECID   |
11 | 6, 8, 10 | ifcldcd 3569 |
. . . . . . . . . 10
   DECID
        |
12 | 11 | adantll 476 |
. . . . . . . . 9
   Markov 
DECID

        |
13 | | eqid 2177 |
. . . . . . . . . 10
               |
14 | 13 | fvmpt2 5594 |
. . . . . . . . 9
                          |
15 | 4, 12, 14 | syl2anc 411 |
. . . . . . . 8
   Markov 
DECID

                   |
16 | 15 | eqeq1d 2186 |
. . . . . . 7
   Markov 
DECID

            
  
 
   |
17 | | 1n0 6426 |
. . . . . . . . . 10
 |
18 | 17 | nesymi 2393 |
. . . . . . . . 9
 |
19 | | iftrue 3539 |
. . . . . . . . . 10
        |
20 | 19 | eqeq1d 2186 |
. . . . . . . . 9
      
   |
21 | 18, 20 | mtbiri 675 |
. . . . . . . 8
        |
22 | 21 | con2i 627 |
. . . . . . 7
        |
23 | 16, 22 | syl6bi 163 |
. . . . . 6
   Markov 
DECID

                |
24 | 3, 23 | ralimdaa 2543 |
. . . . 5
  Markov

DECID   
           
   |
25 | 24 | con3d 631 |
. . . 4
  Markov

DECID   

              |
26 | 25 | 3impia 1200 |
. . 3
  Markov

DECID 


             |
27 | | mptexg 5736 |
. . . . 5
 Markov          |
28 | 27 | 3ad2ant1 1018 |
. . . 4
  Markov

DECID 


        |
29 | | ismkv 7144 |
. . . . . 6
 Markov  Markov                        |
30 | 29 | ibi 176 |
. . . . 5
 Markov                       |
31 | 30 | 3ad2ant1 1018 |
. . . 4
  Markov

DECID 

        
   

        |
32 | | nfra1 2508 |
. . . . . . 7
  
 |
33 | 32 | nfn 1658 |
. . . . . 6
   |
34 | 1, 2, 33 | nf3an 1566 |
. . . . 5
   Markov 
DECID
   |
35 | 11 | 3ad2antl2 1160 |
. . . . 5
   Markov 
DECID
       
  |
36 | 34, 35, 13 | fmptdf 5668 |
. . . 4
  Markov

DECID 


            |
37 | | feq1 5343 |
. . . . . 6
       
    

             |
38 | | nfmpt1 4093 |
. . . . . . . . . 10
          |
39 | 38 | nfeq2 2331 |
. . . . . . . . 9


       |
40 | | fveq1 5509 |
. . . . . . . . . 10
       
                 |
41 | 40 | eqeq1d 2186 |
. . . . . . . . 9
       
    
              |
42 | 39, 41 | ralbid 2475 |
. . . . . . . 8
       
 
   
               |
43 | 42 | notbid 667 |
. . . . . . 7
       
     

              |
44 | 40 | eqeq1d 2186 |
. . . . . . . 8
       
                   |
45 | 39, 44 | rexbid 2476 |
. . . . . . 7
       
 
                   |
46 | 43, 45 | imbi12d 234 |
. . . . . 6
       
            
            

               |
47 | 37, 46 | imbi12d 234 |
. . . . 5
       
                                                             |
48 | 47 | spcgv 2824 |
. . . 4
                 
   

                                                |
49 | 28, 31, 36, 48 | syl3c 63 |
. . 3
  Markov

DECID 

            

              |
50 | 26, 49 | mpd 13 |
. 2
  Markov

DECID 


             |
51 | | simpr 110 |
. . . . . 6
   Markov 
DECID
     |
52 | 51, 35, 14 | syl2anc 411 |
. . . . 5
   Markov 
DECID
                     |
53 | 52 | eqeq1d 2186 |
. . . 4
   Markov 
DECID
              
        |
54 | 9 | 3ad2ant2 1019 |
. . . . . . 7
  Markov

DECID 


DECID    |
55 | 54 | imp 124 |
. . . . . 6
   Markov 
DECID
  
DECID   |
56 | 17 | neii 2349 |
. . . . . . . . 9
 |
57 | | simpr 110 |
. . . . . . . . . . 11
    Markov  DECID    
  |
58 | 57 | iffalsed 3544 |
. . . . . . . . . 10
    Markov  DECID    
  
 
  |
59 | 58 | eqeq1d 2186 |
. . . . . . . . 9
    Markov  DECID    
     
   |
60 | 56, 59 | mtbiri 675 |
. . . . . . . 8
    Markov  DECID    
    
  |
61 | 60 | ex 115 |
. . . . . . 7
   Markov 
DECID
   
    
   |
62 | 61 | con2d 624 |
. . . . . 6
   Markov 
DECID
            |
63 | | notnotrdc 843 |
. . . . . 6
DECID     |
64 | 55, 62, 63 | sylsyld 58 |
. . . . 5
   Markov 
DECID
            |
65 | 64, 19 | impbid1 142 |
. . . 4
   Markov 
DECID
            |
66 | 53, 65 | bitrd 188 |
. . 3
   Markov 
DECID
              
   |
67 | 34, 66 | rexbida 2472 |
. 2
  Markov

DECID 

 
               |
68 | 50, 67 | mpbid 147 |
1
  Markov

DECID 


  |