Step | Hyp | Ref
| Expression |
1 | | f1oi 5339 |
. . . . . . . . . . 11
      |
2 | | f1of 5301 |
. . . . . . . . . . 11

    
       |
3 | 1, 2 | mp1i 10 |
. . . . . . . . . 10
       ⊔          |
4 | | fconst6g 5257 |
. . . . . . . . . . 11
           |
5 | 4 | adantr 272 |
. . . . . . . . . 10
       ⊔             |
6 | 3, 5 | casef 6888 |
. . . . . . . . 9
       ⊔   case
          ⊔      |
7 | | ffun 5211 |
. . . . . . . . 9
case           ⊔    case          |
8 | 6, 7 | syl 14 |
. . . . . . . 8
       ⊔   case          |
9 | | vex 2644 |
. . . . . . . . 9
 |
10 | 9 | a1i 9 |
. . . . . . . 8
       ⊔     |
11 | | cofunexg 5940 |
. . . . . . . 8
  case       
 case           |
12 | 8, 10, 11 | syl2anc 406 |
. . . . . . 7
       ⊔   case           |
13 | | fof 5281 |
. . . . . . . . . 10
      ⊔ 
     ⊔    |
14 | 13 | adantl 273 |
. . . . . . . . 9
       ⊔        ⊔    |
15 | | fco 5224 |
. . . . . . . . 9
 case           ⊔         ⊔  
case               |
16 | 6, 14, 15 | syl2anc 406 |
. . . . . . . 8
       ⊔   case               |
17 | | simplr 500 |
. . . . . . . . . . 11
        ⊔  
      ⊔    |
18 | | djulcl 6851 |
. . . . . . . . . . . 12
 inl   ⊔    |
19 | 18 | adantl 273 |
. . . . . . . . . . 11
        ⊔  
 inl   ⊔
   |
20 | | foelrn 5586 |
. . . . . . . . . . 11
       ⊔  inl   ⊔   
inl        |
21 | 17, 19, 20 | syl2anc 406 |
. . . . . . . . . 10
        ⊔  
  inl        |
22 | | fofn 5283 |
. . . . . . . . . . . . . . . 16
      ⊔ 
  |
23 | 22 | ad4antlr 482 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
  |
24 | | simplr 500 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
  |
25 | | fvco2 5422 |
. . . . . . . . . . . . . . 15
 
  case
           case                 |
26 | 23, 24, 25 | syl2anc 406 |
. . . . . . . . . . . . . 14
          ⊔     inl      
 case            case                 |
27 | | simpr 109 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
inl        |
28 | 27 | fveq2d 5357 |
. . . . . . . . . . . . . 14
          ⊔     inl      
case          inl   case                 |
29 | | fnresi 5176 |
. . . . . . . . . . . . . . . 16
  |
30 | 29 | a1i 9 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
   |
31 | | vex 2644 |
. . . . . . . . . . . . . . . . 17
 |
32 | 31 | fconst6 5258 |
. . . . . . . . . . . . . . . 16
         |
33 | | ffun 5211 |
. . . . . . . . . . . . . . . 16
        
      |
34 | 32, 33 | mp1i 10 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
      |
35 | | simpllr 504 |
. . . . . . . . . . . . . . 15
          ⊔     inl      
  |
36 | 30, 34, 35 | caseinl 6891 |
. . . . . . . . . . . . . 14
          ⊔     inl      
case          inl          |
37 | 26, 28, 36 | 3eqtr2d 2138 |
. . . . . . . . . . . . 13
          ⊔     inl      
 case                   |
38 | | fvresi 5545 |
. . . . . . . . . . . . . 14
        |
39 | 35, 38 | syl 14 |
. . . . . . . . . . . . 13
          ⊔     inl      
       |
40 | 37, 39 | eqtr2d 2133 |
. . . . . . . . . . . 12
          ⊔     inl      
 case              |
41 | 40 | ex 114 |
. . . . . . . . . . 11
         ⊔      inl       case               |
42 | 41 | reximdva 2493 |
. . . . . . . . . 10
        ⊔  
   inl      
 case               |
43 | 21, 42 | mpd 13 |
. . . . . . . . 9
        ⊔  
 
 case              |
44 | 43 | ralrimiva 2464 |
. . . . . . . 8
       ⊔   
  case              |
45 | | dffo3 5499 |
. . . . . . . 8
 case            
 case              
 case               |
46 | 16, 44, 45 | sylanbrc 411 |
. . . . . . 7
       ⊔   case               |
47 | | foeq1 5277 |
. . . . . . . 8
 case
            
case                |
48 | 47 | spcegv 2729 |
. . . . . . 7
 case          case                     |
49 | 12, 46, 48 | sylc 62 |
. . . . . 6
       ⊔          |
50 | 49 | ex 114 |
. . . . 5
       ⊔          |
51 | 50 | exlimiv 1545 |
. . . 4
        ⊔
         |
52 | 51 | exlimdv 1758 |
. . 3
         ⊔ 
        |
53 | | foeq1 5277 |
. . . 4
             |
54 | 53 | cbvexv 1855 |
. . 3
             |
55 | 52, 54 | syl6ibr 161 |
. 2
         ⊔ 
        |
56 | | ctmlemr 6908 |
. 2
        
     ⊔     |
57 | 55, 56 | impbid 128 |
1
         ⊔ 
        |