Step | Hyp | Ref
| Expression |
1 | | ensym 7643 |
. 2

  |
2 | | bren 7603 |
. . . 4

       |
3 | | simpll 765 |
. . . . . . . . . . . . . . 15
           |
4 | | f1of 5836 |
. . . . . . . . . . . . . . . . 17
    
      |
5 | 4 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
           |
6 | 5 | ffvelrnda 6044 |
. . . . . . . . . . . . . . 15
               |
7 | 3, 6 | sseldd 3444 |
. . . . . . . . . . . . . 14
               |
8 | 7 | leidd 10207 |
. . . . . . . . . . . . 13
                   |
9 | | df-br 4416 |
. . . . . . . . . . . . 13
        
            |
10 | 8, 9 | sylib 201 |
. . . . . . . . . . . 12
                     |
11 | | opelxpi 4884 |
. . . . . . . . . . . . 13
                          |
12 | 7, 7, 11 | syl2anc 671 |
. . . . . . . . . . . 12
                        |
13 | 10, 12 | elind 3629 |
. . . . . . . . . . 11
                   
     |
14 | | df-ov 6317 |
. . . . . . . . . . . . 13
                        |
15 | | opex 4677 |
. . . . . . . . . . . . . 14
            |
16 | | fvi 5944 |
. . . . . . . . . . . . . 14
           
                          |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
            
            |
18 | 14, 17 | eqtri 2483 |
. . . . . . . . . . . 12
                      |
19 | 18 | mpteq2i 4499 |
. . . . . . . . . . 11
                          |
20 | 13, 19 | fmptd 6068 |
. . . . . . . . . 10
 
                          |
21 | | nnex 10642 |
. . . . . . . . . . . . 13
 |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
 
       |
23 | 7 | recnd 9694 |
. . . . . . . . . . . 12
               |
24 | 5 | feqmptd 5940 |
. . . . . . . . . . . 12
 
             |
25 | 22, 23, 23, 24, 24 | offval2 6574 |
. . . . . . . . . . 11
 
                      |
26 | 25 | feq1d 5735 |
. . . . . . . . . 10
 
             
 
                
     |
27 | 20, 26 | mpbird 240 |
. . . . . . . . 9
 
           
     |
28 | | f1ofo 5843 |
. . . . . . . . . . . . . . . 16
    
      |
29 | 28 | adantl 472 |
. . . . . . . . . . . . . . 15
 
           |
30 | | forn 5818 |
. . . . . . . . . . . . . . 15
    
  |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
 
    
  |
32 | 31 | eleq2d 2524 |
. . . . . . . . . . . . 13
 
         |
33 | | f1ofn 5837 |
. . . . . . . . . . . . . . 15
    
  |
34 | 33 | adantl 472 |
. . . . . . . . . . . . . 14
 
       |
35 | | fvelrnb 5934 |
. . . . . . . . . . . . . 14
          |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
 
              |
37 | 32, 36 | bitr3d 263 |
. . . . . . . . . . . 12
 
     
        |
38 | 25, 19 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . 20
 
                       |
39 | 38 | fveq1d 5889 |
. . . . . . . . . . . . . . . . . . 19
 
                               |
40 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
41 | 40 | fvmpt2 5979 |
. . . . . . . . . . . . . . . . . . . 20
                                            |
42 | 15, 41 | mpan2 682 |
. . . . . . . . . . . . . . . . . . 19
                               |
43 | 39, 42 | sylan9eq 2515 |
. . . . . . . . . . . . . . . . . 18
                             |
44 | 43 | fveq2d 5891 |
. . . . . . . . . . . . . . . . 17
                                     |
45 | | fvex 5897 |
. . . . . . . . . . . . . . . . . 18
     |
46 | 45, 45 | op1st 6827 |
. . . . . . . . . . . . . . . . 17
              
     |
47 | 44, 46 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
                          |
48 | 47, 8 | eqbrtrd 4436 |
. . . . . . . . . . . . . . 15
                   
      |
49 | 43 | fveq2d 5891 |
. . . . . . . . . . . . . . . . 17
                                     |
50 | 45, 45 | op2nd 6828 |
. . . . . . . . . . . . . . . . 17
              
     |
51 | 49, 50 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
                          |
52 | 8, 51 | breqtrrd 4442 |
. . . . . . . . . . . . . . 15
                          |
53 | 48, 52 | jca 539 |
. . . . . . . . . . . . . 14
                        
                  |
54 | | breq2 4419 |
. . . . . . . . . . . . . . 15
                                   |
55 | | breq1 4418 |
. . . . . . . . . . . . . . 15
         
          
              |
56 | 54, 55 | anbi12d 722 |
. . . . . . . . . . . . . 14
                     
               
           
               |
57 | 53, 56 | syl5ibcom 228 |
. . . . . . . . . . . . 13
                         
               |
58 | 57 | reximdva 2873 |
. . . . . . . . . . . 12
 
      
    
           
               |
59 | 37, 58 | sylbid 223 |
. . . . . . . . . . 11
 
      
           
               |
60 | 59 | ralrimiv 2811 |
. . . . . . . . . 10
 
     
                           |
61 | | ovolficc 22469 |
. . . . . . . . . . 11
 
      
           

           
               |
62 | 27, 61 | syldan 477 |
. . . . . . . . . 10
 
             
           
               |
63 | 60, 62 | mpbird 240 |
. . . . . . . . 9
 
     
       |
64 | | eqid 2461 |
. . . . . . . . . 10
   
 
      
      |
65 | 64 | ovollb2 22490 |
. . . . . . . . 9
         
  
     
          
 
    
  |
66 | 27, 63, 65 | syl2anc 671 |
. . . . . . . 8
 
               
         |
67 | | opelxpi 4884 |
. . . . . . . . . . . . . . . . . 18
                          |
68 | 23, 23, 67 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                        |
69 | | absf 13448 |
. . . . . . . . . . . . . . . . . . . 20
     |
70 | | subf 9902 |
. . . . . . . . . . . . . . . . . . . 20
      |
71 | | fco 5761 |
. . . . . . . . . . . . . . . . . . . 20
            
        |
72 | 69, 70, 71 | mp2an 683 |
. . . . . . . . . . . . . . . . . . 19

       |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
              |
74 | 73 | feqmptd 5940 |
. . . . . . . . . . . . . . . . 17
 
                 |
75 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . 18
             
                     |
76 | | df-ov 6317 |
. . . . . . . . . . . . . . . . . 18
                              |
77 | 75, 76 | syl6eqr 2513 |
. . . . . . . . . . . . . . . . 17
             
                  |
78 | 68, 38, 74, 77 | fmptco 6079 |
. . . . . . . . . . . . . . . 16
 
      
                     |
79 | | cnmet 21840 |
. . . . . . . . . . . . . . . . . 18

     |
80 | | met0 21406 |
. . . . . . . . . . . . . . . . . 18
  
                        |
81 | 79, 23, 80 | sylancr 674 |
. . . . . . . . . . . . . . . . 17
                        |
82 | 81 | mpteq2dva 4502 |
. . . . . . . . . . . . . . . 16
 
                        |
83 | 78, 82 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
 
      
        |
84 | | fconstmpt 4896 |
. . . . . . . . . . . . . . 15
       |
85 | 83, 84 | syl6eqr 2513 |
. . . . . . . . . . . . . 14
 
      
          |
86 | 85 | seqeq3d 12252 |
. . . . . . . . . . . . 13
 
        
              |
87 | | 1z 10995 |
. . . . . . . . . . . . . 14
 |
88 | | nnuz 11222 |
. . . . . . . . . . . . . . 15
     |
89 | 88 | ser0f 12297 |
. . . . . . . . . . . . . 14
              |
90 | 87, 89 | ax-mp 5 |
. . . . . . . . . . . . 13
            |
91 | 86, 90 | syl6eq 2511 |
. . . . . . . . . . . 12
 
        
           |
92 | 91 | rneqd 5080 |
. . . . . . . . . . 11
 
        
           |
93 | | 1nn 10647 |
. . . . . . . . . . . 12
 |
94 | | ne0i 3748 |
. . . . . . . . . . . 12
   |
95 | | rnxp 5285 |
. . . . . . . . . . . 12

        |
96 | 93, 94, 95 | mp2b 10 |
. . . . . . . . . . 11
       |
97 | 92, 96 | syl6eq 2511 |
. . . . . . . . . 10
 
        
         |
98 | 97 | supeq1d 7985 |
. . . . . . . . 9
 
                          |
99 | | xrltso 11468 |
. . . . . . . . . 10
 |
100 | | 0xr 9712 |
. . . . . . . . . 10
 |
101 | | supsn 8013 |
. . . . . . . . . 10
          |
102 | 99, 100, 101 | mp2an 683 |
. . . . . . . . 9
       |
103 | 98, 102 | syl6eq 2511 |
. . . . . . . 8
 
                    |
104 | 66, 103 | breqtrd 4440 |
. . . . . . 7
 
            |
105 | | ovolge0 22482 |
. . . . . . . 8

       |
106 | 105 | adantr 471 |
. . . . . . 7
 
            |
107 | | ovolcl 22479 |
. . . . . . . . 9

       |
108 | 107 | adantr 471 |
. . . . . . . 8
 
            |
109 | | xrletri3 11479 |
. . . . . . . 8
                   
         |
110 | 108, 100,
109 | sylancl 673 |
. . . . . . 7
 
                
         |
111 | 104, 106,
110 | mpbir2and 938 |
. . . . . 6
 
            |
112 | 111 | ex 440 |
. . . . 5

    
        |
113 | 112 | exlimdv 1789 |
. . . 4

              |
114 | 2, 113 | syl5bi 225 |
. . 3

         |
115 | 114 | imp 435 |
. 2
 
        |
116 | 1, 115 | sylan2 481 |
1
 
        |