Step | Hyp | Ref
| Expression |
1 | | breldm 4912 |
. . . . . . . . . 10
     |
2 | 1 | adantl 452 |
. . . . . . . . 9
       |
3 | | fnfrec.1 |
. . . . . . . . . . 11
FRec     |
4 | | fnfrec.2 |
. . . . . . . . . . 11
 Funs  |
5 | | fnfrec.3 |
. . . . . . . . . . 11
   |
6 | | fnfrec.4 |
. . . . . . . . . . 11
   |
7 | 3, 4, 5, 6 | dmfrec 6317 |
. . . . . . . . . 10
 Nn  |
8 | 7 | adantr 451 |
. . . . . . . . 9
     Nn  |
9 | 2, 8 | eleqtrd 2429 |
. . . . . . . 8
     Nn  |
10 | 9 | adantrr 697 |
. . . . . . 7
        
Nn  |
11 | 3 | frecexg 6313 |
. . . . . . . . . . . 12
 Funs
  |
12 | | fnfreclem1 6318 |
. . . . . . . . . . . 12
 
               |
13 | 4, 11, 12 | 3syl 18 |
. . . . . . . . . . 11
            
 
  |
14 | | breq1 4643 |
. . . . . . . . . . . . . 14
 0c    0c    |
15 | | breq1 4643 |
. . . . . . . . . . . . . 14
 0c    0c    |
16 | 14, 15 | anbi12d 691 |
. . . . . . . . . . . . 13
 0c        0c 0c     |
17 | 16 | imbi1d 308 |
. . . . . . . . . . . 12
 0c           0c
0c 
    |
18 | 17 | 2albidv 1627 |
. . . . . . . . . . 11
 0c                   0c 0c      |
19 | | breq1 4643 |
. . . . . . . . . . . . . 14
         |
20 | | breq1 4643 |
. . . . . . . . . . . . . 14
         |
21 | 19, 20 | anbi12d 691 |
. . . . . . . . . . . . 13
                 |
22 | 21 | imbi1d 308 |
. . . . . . . . . . . 12
                     |
23 | 22 | 2albidv 1627 |
. . . . . . . . . . 11
                             |
24 | | breq1 4643 |
. . . . . . . . . . . . . . 15
  1c    
1c     |
25 | | breq1 4643 |
. . . . . . . . . . . . . . 15
  1c    
1c     |
26 | 24, 25 | anbi12d 691 |
. . . . . . . . . . . . . 14
  1c         
1c  
1c      |
27 | 26 | imbi1d 308 |
. . . . . . . . . . . . 13
  1c            
1c  
1c       |
28 | 27 | 2albidv 1627 |
. . . . . . . . . . . 12
  1c                    
1c  
1c       |
29 | | breq2 4644 |
. . . . . . . . . . . . . . 15
  
1c   1c     |
30 | | breq2 4644 |
. . . . . . . . . . . . . . 15
  
1c   1c     |
31 | 29, 30 | bi2anan9 843 |
. . . . . . . . . . . . . 14
 
    1c   1c     1c 
 1c      |
32 | | eqeq12 2365 |
. . . . . . . . . . . . . 14
 
     |
33 | 31, 32 | imbi12d 311 |
. . . . . . . . . . . . 13
 
    
1c  
1c       1c   1c       |
34 | 33 | cbval2v 2006 |
. . . . . . . . . . . 12
       
1c  
1c           1c 
 1c      |
35 | 28, 34 | syl6bb 252 |
. . . . . . . . . . 11
  1c                    
1c  
1c       |
36 | | breq1 4643 |
. . . . . . . . . . . . . 14
         |
37 | | breq1 4643 |
. . . . . . . . . . . . . 14
         |
38 | 36, 37 | anbi12d 691 |
. . . . . . . . . . . . 13
                 |
39 | 38 | imbi1d 308 |
. . . . . . . . . . . 12
                     |
40 | 39 | 2albidv 1627 |
. . . . . . . . . . 11
                             |
41 | 3, 4, 5, 6 | fnfreclem2 6319 |
. . . . . . . . . . . . . . . 16
 0c    |
42 | 41 | imp 418 |
. . . . . . . . . . . . . . 15
  0c 
  |
43 | 42 | adantrr 697 |
. . . . . . . . . . . . . 14
  0c
0c     |
44 | 3, 4, 5, 6 | fnfreclem2 6319 |
. . . . . . . . . . . . . . . 16
 0c    |
45 | 44 | imp 418 |
. . . . . . . . . . . . . . 15
  0c 
  |
46 | 45 | adantrl 696 |
. . . . . . . . . . . . . 14
  0c
0c     |
47 | 43, 46 | eqtr4d 2388 |
. . . . . . . . . . . . 13
  0c
0c     |
48 | 47 | ex 423 |
. . . . . . . . . . . 12
  0c
0c 
   |
49 | 48 | alrimivv 1632 |
. . . . . . . . . . 11
      0c
0c 
   |
50 | 4 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   Funs  |
51 | 5 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c     |
52 | 6 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c     |
53 | | simplr 731 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   Nn  |
54 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   
1c    |
55 | 3, 50, 51, 52, 53, 54 | fnfreclem3 6320 |
. . . . . . . . . . . . . . . . . . 19
   Nn 
1c             |
56 | 55 | adantlrr 701 |
. . . . . . . . . . . . . . . . . 18
   
Nn                1c             |
57 | 56 | ex 423 |
. . . . . . . . . . . . . . . . 17
   Nn           
  
 
1c             |
58 | 4 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   Funs  |
59 | 5 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c     |
60 | 6 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c     |
61 | | simplr 731 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   Nn  |
62 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . 20
   Nn 
1c   
1c    |
63 | 3, 58, 59, 60, 61, 62 | fnfreclem3 6320 |
. . . . . . . . . . . . . . . . . . 19
   Nn 
1c             |
64 | 63 | adantlrr 701 |
. . . . . . . . . . . . . . . . . 18
   
Nn                1c             |
65 | 64 | ex 423 |
. . . . . . . . . . . . . . . . 17
   Nn           
  
 
1c             |
66 | 57, 65 | anim12d 546 |
. . . . . . . . . . . . . . . 16
   Nn           
  
  
1c  
1c                        |
67 | | eeanv 1913 |
. . . . . . . . . . . . . . . 16
                                       |
68 | 66, 67 | syl6ibr 218 |
. . . . . . . . . . . . . . 15
   Nn           
  
  
1c  
1c                        |
69 | | 19.29 1596 |
. . . . . . . . . . . . . . . . . . 19
                                                                 |
70 | | 19.29 1596 |
. . . . . . . . . . . . . . . . . . . 20
                                                         |
71 | 70 | eximi 1576 |
. . . . . . . . . . . . . . . . . . 19
                                          
                  |
72 | 69, 71 | syl 15 |
. . . . . . . . . . . . . . . . . 18
                                                               |
73 | | pm3.35 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
  |
74 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
75 | 74 | anbi1d 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 |
76 | 75 | biimpa 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
77 | | elfunsi 5832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 Funs   |
78 | | funbrfv 5357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
79 | 4, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
   |
80 | | funbrfv 5357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
81 | 4, 77, 80 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
   |
82 | 79, 81 | anim12d 546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     |
83 | | eqtr2 2371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
    
  |
84 | 76, 82, 83 | syl56 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
   |
85 | 84 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
86 | 73, 85 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               
             |
87 | 86 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                             |
88 | 87 | com34 77 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
89 | 88 | imp3a 420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
90 | 89 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
91 | 90 | an4s 799 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
92 | 91 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . 21
                             |
93 | 92 | imp3a 420 |
. . . . . . . . . . . . . . . . . . . 20
         
                   |
94 | 93 | exlimdvv 1637 |
. . . . . . . . . . . . . . . . . . 19
                                 |
95 | 94 | adantr 451 |
. . . . . . . . . . . . . . . . . 18
  Nn                                 |
96 | 72, 95 | syl5 28 |
. . . . . . . . . . . . . . . . 17
  Nn                                     |
97 | 96 | exp3a 425 |
. . . . . . . . . . . . . . . 16
  Nn            
                   
    |
98 | 97 | impr 602 |
. . . . . . . . . . . . . . 15
   Nn           
  
                      |
99 | 68, 98 | syld 40 |
. . . . . . . . . . . . . 14
   Nn           
  
  
1c  
1c      |
100 | 99 | alrimivv 1632 |
. . . . . . . . . . . . 13
   Nn           
  
      
1c  
1c      |
101 | 100 | expr 598 |
. . . . . . . . . . . 12
  Nn            
        1c 
 1c       |
102 | 101 | ancoms 439 |
. . . . . . . . . . 11
  Nn                      1c 
 1c       |
103 | 13, 18, 23, 35, 40, 49, 102 | findsd 4411 |
. . . . . . . . . 10
  Nn                |
104 | 103 | 19.21bbi 1865 |
. . . . . . . . 9
  Nn            |
105 | 104 | ex 423 |
. . . . . . . 8
 Nn        
    |
106 | 105 | imp3a 420 |
. . . . . . 7
 Nn             |
107 | 10, 106 | mpcom 32 |
. . . . . 6
        
  |
108 | 107 | ex 423 |
. . . . 5
           |
109 | 108 | alrimivv 1632 |
. . . 4
               |
110 | 109 | alrimiv 1631 |
. . 3
                 |
111 | | dffun2 5120 |
. . 3
                 |
112 | 110, 111 | sylibr 203 |
. 2
   |
113 | | df-fn 4791 |
. 2
 Nn  Nn   |
114 | 112, 7, 113 | sylanbrc 645 |
1
 Nn  |