Step | Hyp | Ref
| Expression |
1 | | dfrdg3 30491 |
. 2
  
              
                           |
2 | | an12 811 |
. . . . . . . 8
            
                            
                                     |
3 | | df-fn 5603 |
. . . . . . . . . 10

    |
4 | | ancom 456 |
. . . . . . . . . 10
 
     |
5 | | eqcom 2468 |
. . . . . . . . . . 11

  |
6 | 5 | anbi1i 706 |
. . . . . . . . . 10
       |
7 | 3, 4, 6 | 3bitri 279 |
. . . . . . . . 9

    |
8 | 7 | anbi1i 706 |
. . . . . . . 8
  
         
                                         
                          |
9 | | anass 659 |
. . . . . . . 8
     
                                  
 
            
                           |
10 | 2, 8, 9 | 3bitri 279 |
. . . . . . 7
            
                           
            
                           |
11 | 10 | exbii 1728 |
. . . . . 6
     
                                  
              
                             |
12 | | vex 3059 |
. . . . . . . 8
 |
13 | 12 | dmex 6752 |
. . . . . . 7
 |
14 | | eleq1 2527 |
. . . . . . . . 9
     |
15 | | raleq 2998 |
. . . . . . . . 9
                                                                          |
16 | 14, 15 | anbi12d 722 |
. . . . . . . 8
   
                                 


           
                          |
17 | 16 | anbi2d 715 |
. . . . . . 7
             
                                                                    |
18 | 13, 17 | ceqsexv 3095 |
. . . . . 6
    
            
                        
                                         |
19 | 11, 18 | bitri 257 |
. . . . 5
     
                                  
                                         |
20 | | df-rex 2754 |
. . . . 5
              
                           
                                     |
21 | | eldif 3425 |
. . . . . 6
    Domain     Domain   Apply                Img     FullFun Apply pprod    
Succ     
 
 Domain    
Domain   Apply                Img     FullFun Apply pprod    
Succ        |
22 | | elin 3628 |
. . . . . . . 8
   Domain     Domain     |
23 | 12 | elfuns 30730 |
. . . . . . . . 9

  |
24 | 12 | elima 5191 |
. . . . . . . . . 10
  Domain    Domain  |
25 | | df-rex 2754 |
. . . . . . . . . 10
   Domain     Domain   |
26 | | ancom 456 |
. . . . . . . . . . . . 13
   Domain
  Domain    |
27 | | vex 3059 |
. . . . . . . . . . . . . . . 16
 |
28 | 27, 12 | brcnv 5035 |
. . . . . . . . . . . . . . 15
  Domain Domain  |
29 | 12, 27 | brdomain 30748 |
. . . . . . . . . . . . . . 15
 Domain
  |
30 | 28, 29 | bitri 257 |
. . . . . . . . . . . . . 14
  Domain
  |
31 | 30 | anbi1i 706 |
. . . . . . . . . . . . 13
   Domain
 
   |
32 | 26, 31 | bitri 257 |
. . . . . . . . . . . 12
   Domain
    |
33 | 32 | exbii 1728 |
. . . . . . . . . . 11
     Domain
      |
34 | 13, 14 | ceqsexv 3095 |
. . . . . . . . . . 11
    
  |
35 | 33, 34 | bitri 257 |
. . . . . . . . . 10
     Domain
  |
36 | 24, 25, 35 | 3bitri 279 |
. . . . . . . . 9
  Domain    |
37 | 23, 36 | anbi12i 708 |
. . . . . . . 8
   Domain  
    |
38 | 22, 37 | bitri 257 |
. . . . . . 7
   Domain   
   |
39 | 38 | anbi1i 706 |
. . . . . 6
    Domain  
 
Domain   Apply                Img     FullFun Apply pprod    
Succ     
 

 
Domain   Apply                Img     FullFun Apply pprod    
Succ        |
40 | | brdif 4466 |
. . . . . . . . . . . . . . 15
    Domain   Apply                Img     FullFun Apply pprod    
Succ     
   Domain    Apply                Img     FullFun Apply pprod   
 Succ        |
41 | | vex 3059 |
. . . . . . . . . . . . . . . . . 18
 |
42 | 12, 41 | brco 5023 |
. . . . . . . . . . . . . . . . 17
   Domain    Domain
    |
43 | 29 | anbi1i 706 |
. . . . . . . . . . . . . . . . . . 19
  Domain  
     |
44 | 43 | exbii 1728 |
. . . . . . . . . . . . . . . . . 18
    Domain      
   |
45 | | breq1 4418 |
. . . . . . . . . . . . . . . . . . 19
       |
46 | 13, 45 | ceqsexv 3095 |
. . . . . . . . . . . . . . . . . 18
     
   |
47 | 44, 46 | bitri 257 |
. . . . . . . . . . . . . . . . 17
    Domain      |
48 | 13, 41 | brcnv 5035 |
. . . . . . . . . . . . . . . . . 18
    |
49 | 13 | epelc 4765 |
. . . . . . . . . . . . . . . . . 18

  |
50 | 48, 49 | bitri 257 |
. . . . . . . . . . . . . . . . 17
    |
51 | 42, 47, 50 | 3bitri 279 |
. . . . . . . . . . . . . . . 16
   Domain   |
52 | 51 | anbi1i 706 |
. . . . . . . . . . . . . . 15
    Domain    Apply                Img
    FullFun Apply pprod    
Succ     
    Apply                Img
    FullFun Apply pprod    
Succ        |
53 | 40, 52 | bitri 257 |
. . . . . . . . . . . . . 14
    Domain   Apply                Img     FullFun Apply pprod    
Succ     
    Apply                Img
    FullFun Apply pprod    
Succ        |
54 | | onelon 5466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
  |
55 | 54 | 3adant1 1032 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
56 | | brun 4464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    Img
    FullFun Apply pprod    
Succ                            Img
    FullFun Apply pprod    
Succ      |
57 | | brxp 4883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                
                |
58 | | opelxp 4882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
      |
59 | 12, 58 | mpbiran 934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
    |
60 | | elsn 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
  |
61 | 59, 60 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
  |
62 | | elsn 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     |
63 | 61, 62 | anbi12i 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              
       |
64 | 57, 63 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                
       |
65 | | brun 4464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Img
    FullFun Apply pprod    
Succ  
      
Img          FullFun Apply pprod    
Succ     |
66 | 27 | brres 5129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       Img    
      Img         |
67 | | opex 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    |
68 | 67, 27 | brco 5023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
Img       Img      |
69 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
70 | 12, 41, 69 | brimg 30752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    Img       |
71 | 27 | brbigcup 30713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
   |
72 | 70, 71 | anbi12i 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     Img             |
73 | 72 | exbii 1728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       Img   
           |
74 | | imaexg 6756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
75 | 12, 74 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
76 | | unieq 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
77 | 76 | eqeq1d 2463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
        |
78 | 75, 77 | ceqsexv 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
 
       |
79 | | eqcom 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       |
80 | 78, 79 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
 
       |
81 | 68, 73, 80 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
Img        |
82 | | opelxp 4882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          |
83 | 12, 82 | mpbiran 934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        |
84 | 41 | ellimits 30725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
85 | 83, 84 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        |
86 | 81, 85 | anbi12ci 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
Img      
         |
87 | 66, 86 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       Img    
         |
88 | 27 | brres 5129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      FullFun Apply pprod    
Succ 
     FullFun Apply pprod         Succ   |
89 | 67, 27 | brco 5023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     FullFun
Apply pprod    
       Apply
pprod    FullFun    |
90 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
91 | 67, 90 | brco 5023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     Apply
pprod   
      pprod   Apply   |
92 | 12, 41, 69 | brpprod3a 30701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    pprod
         
     |
93 | | 3anrot 996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    
  

        |
94 | 90 | ideq 5005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41

  |
95 | | equcom 1872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41

  |
96 | 94, 95 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
97 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 |
98 | 97 | brbigcup 30713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
  
   |
99 | | eqcom 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
   |
100 | 98, 99 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
  
   |
101 | | biid 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
         |
102 | 96, 100, 101 | 3anbi123i 1203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       
        |
103 | 93, 102 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
  

       |
104 | 103 | 2exbii 1729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
        
  
            |
105 | 41 | uniex 6613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  |
106 | | opeq1 4179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
         |
107 | 106 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
      |
108 | | opeq2 4180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
           |
109 | 108 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     
       |
110 | 12, 105, 107, 109 | ceqsex2v 3098 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     

          |
111 | 92, 104, 110 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    pprod
        |
112 | 111 | anbi1i 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     pprod
  Apply      Apply   |
113 | 112 | exbii 1728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       pprod   Apply
       Apply   |
114 | | opex 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
115 | | breq1 4418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
 Apply     Apply   |
116 | 114, 115 | ceqsexv 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        Apply     Apply  |
117 | 12, 105, 90 | brapply 30753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     Apply        |
118 | 116, 117 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        Apply        |
119 | 91, 113, 118 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     Apply
pprod   
       |
120 | 90, 27 | brfullfun 30763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 FullFun
      |
121 | 119, 120 | anbi12i 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      Apply
pprod    FullFun 
             |
122 | 121 | exbii 1728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        Apply pprod    FullFun 
       
       |
123 | | fvex 5897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      |
124 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     |
125 | 124 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          
            |
126 | 123, 125 | ceqsexv 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
           |
127 | 89, 122, 126 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     FullFun
Apply pprod    
           |
128 | | opelxp 4882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     Succ  Succ  |
129 | 12, 128 | mpbiran 934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     Succ Succ |
130 | 41 | elrn 5093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 Succ
 Succ  |
131 | 69, 41 | brsuccf 30756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 Succ   |
132 | 131 | exbii 1728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  Succ
   |
133 | 129, 130,
132 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     Succ 
  |
134 | 127, 133 | anbi12ci 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      FullFun
Apply pprod         Succ  
            |
135 | 88, 134 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      FullFun Apply pprod    
Succ 
 
            |
136 | 87, 135 | orbi12i 528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        Img          FullFun
Apply pprod    
Succ  
 
       
             |
137 | 65, 136 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        Img
    FullFun Apply pprod    
Succ  
 
       
             |
138 | 64, 137 | orbi12i 528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         Img
    FullFun Apply pprod    
Succ           
       
              |
139 | 56, 138 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                    Img
    FullFun Apply pprod    
Succ           
       
              |
140 | | onzsl 6699 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

 
     |
141 | | nlim0 5499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
142 | | limeq 5453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

    |
143 | 141, 142 | mtbiri 309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
144 | 143 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30


        |
145 | | nsuceq0 5521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
146 | | neeq2 2698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35


   |
147 | 145, 146 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
148 | 147 | necomd 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
149 | 148 | neneqd 2639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
150 | 149 | nexdv 1792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31


  |
151 | 150 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

 
            |
152 | | ioran 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
       
            
       
             |
153 | 144, 151,
152 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

 
                     |
154 | | orel2 389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
       
          
        
                            |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

        
                            |
156 | | iftrue 3898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

    
                               |
157 | | unisnif 30740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
 
    |
158 | 156, 157 | syl6eqr 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

    
                             |
159 | 158 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

       
                     
      |
160 | 159 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

                                    |
161 | 160 | adantld 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

     
                                |
162 | 155, 161 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

        
                                                    |
163 | 159 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

       
                     
      |
164 | 163 | anc2li 564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

       
                              |
165 | | orc 391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
               
              |
166 | 164, 165 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

       
                             
       
               |
167 | 162, 166 | impbid 195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

        
                        
                           |
168 | | neeq1 2697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   |
169 | 145, 168 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
170 | 169 | neneqd 2639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
171 | 170 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        |
172 | 171 | rexlimivw 2887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
173 | | orel1 388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
              
       
             
                      |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
       
             
                      |
175 | | nlimsucg 6695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
176 | 69, 175 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
177 | | limeq 5453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
178 | 176, 177 | mtbiri 309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
179 | 178 | rexlimivw 2887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    |
180 | 179 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
181 | | orel1 388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     
  
                    
             |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
       
          
 
             |
183 | 145 | neii 2636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
184 | 183 | iffalsei 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
          
                                      |
185 | | iffalse 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  
                            |
186 | 69, 175, 185 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
                           |
187 | 184, 186 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          
                            |
188 | | eqeq1 2465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
189 | | unieq 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
190 | 189 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |
191 | 190 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                     |
192 | 177, 191 | ifbieq2d 3917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                         |
193 | 188, 192 | ifbieq2d 3917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                        
                    |
194 | 187, 193,
191 | 3eqtr4a 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                         |
195 | 194 | rexlimivw 2887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                          |
196 | 195 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
                       
            |
197 | 196 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           
    
                           |
198 | 197 | adantld 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
                                          |
199 | 174, 182,
198 | 3syld 57 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          
       
                                            |
200 | | rexex 2855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
201 | 196 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
                       
            |
202 | | olc 390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                      
             |
203 | 202 | olcd 399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
             
              |
204 | 200, 201,
203 | syl6an 552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
                               
       
               |
205 | 199, 204 | impbid 195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
       
           
                                |
206 | 143 | con2i 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
207 | 206 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

       |
208 | 207, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

        
                             
              |
209 | 178 | exlimiv 1786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
  |
210 | 209 | con2i 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

   |
211 | 210 | intnanrd 933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

 
            |
212 | | orel2 389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
                    
          
          |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  
                   
         |
214 | 206 | iffalsed 3903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

    
                                             |
215 | | iftrue 3898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

                          |
216 | 214, 215 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

    
                               |
217 | 216 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

                             
        |
218 | 217 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

                                      |
219 | 218 | adantld 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

 
     
    
                           |
220 | 208, 213,
219 | 3syld 57 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

        
                                                    |
221 | 220 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
       
                                            |
222 | 217 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

                             
        |
223 | 222 | anc2li 564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

                             
          |
224 | | orc 391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
       
             |
225 | 224 | olcd 399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               
       
              |
226 | 223, 225 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

                             
               
               |
227 | 226 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
                               
       
               |
228 | 221, 227 | impbid 195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
       
           
                                |
229 | 167, 205,
228 | 3jaoi 1340 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
     
             
           
                                |
230 | 140, 229 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
       
           
                                |
231 | 139, 230 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     Img
    FullFun Apply pprod    
Succ        
                           |
232 | 55, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                     Img
    FullFun Apply pprod    
Succ        
                           |
233 | 27, 67 | brcnv 5035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Apply      Apply  |
234 | 12, 41, 27 | brapply 30753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    Apply       |
235 | 233, 234 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
  Apply         |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   Apply  
       |
237 | 232, 236 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . 21
 
                      Img     FullFun Apply pprod   
 Succ     Apply   
                                      |
238 | | ancom 456 |
. . . . . . . . . . . . . . . . . . . . 21
      
                       
    
                                     |
239 | 237, 238 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . 20
 
                      Img     FullFun Apply pprod   
 Succ     Apply   
    
                                 |
240 | 239 | exbidv 1778 |
. . . . . . . . . . . . . . . . . . 19
 
                        Img
    FullFun Apply pprod    
Succ     Apply          
                                 |
241 | | df-br 4416 |
. . . . . . . . . . . . . . . . . . . 20
    Apply                Img
    FullFun Apply pprod    
Succ          Apply                Img     FullFun Apply pprod    
Succ      |
242 | 67 | elfix 30718 |
. . . . . . . . . . . . . . . . . . . 20
      Apply                Img
    FullFun Apply pprod    
Succ         Apply
               Img     FullFun Apply pprod   
 Succ          |
243 | 67, 67 | brco 5023 |
. . . . . . . . . . . . . . . . . . . 20
      Apply
               Img     FullFun Apply pprod   
 Succ       
                      Img
    FullFun Apply pprod    
Succ     Apply      |
244 | 241, 242,
243 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . 19
    Apply                Img
    FullFun Apply pprod    
Succ                           Img
    FullFun Apply pprod    
Succ     Apply      |
245 | | fvex 5897 |
. . . . . . . . . . . . . . . . . . . 20
     |
246 | 245 | eqvinc 3177 |
. . . . . . . . . . . . . . . . . . 19
           
                     
                                       |
247 | 240, 244,
246 | 3bitr4g 296 |
. . . . . . . . . . . . . . . . . 18
 
     Apply                Img     FullFun Apply pprod    
Succ                                         |
248 | 247 | notbid 300 |
. . . . . . . . . . . . . . . . 17
 
     Apply                Img     FullFun Apply pprod   
 Succ    
                                    |
249 | 248 | 3expia 1217 |
. . . . . . . . . . . . . . . 16
 
      Apply                Img     FullFun Apply pprod   
 Succ    
                                     |
250 | 249 | pm5.32d 649 |
. . . . . . . . . . . . . . 15
 
      Apply                Img
    FullFun Apply pprod    
Succ     
         
                            |
251 | | annim 431 |
. . . . . . . . . . . . . . 15
                                   
         
                           |
252 | 250, 251 | syl6bb 269 |
. . . . . . . . . . . . . 14
 
      Apply                Img
    FullFun Apply pprod    
Succ     
         
                            |
253 | 53, 252 | syl5bb 265 |
. . . . . . . . . . . . 13
 
    
Domain   Apply                Img     FullFun Apply pprod    
Succ     
         
                            |
254 | 253 | exbidv 1778 |
. . . . . . . . . . . 12
 
      Domain   Apply                Img     FullFun Apply pprod    
Succ     
                                       |
255 | | exnal 1709 |
. . . . . . . . . . . 12
           
                                    
                           |
256 | 254, 255 | syl6rbb 270 |
. . . . . . . . . . 11
 
                                      
   
Domain   Apply                Img     FullFun Apply pprod    
Succ         |
257 | 12 | eldm 5050 |
. . . . . . . . . . 11
  
Domain   Apply                Img     FullFun Apply pprod    
Succ         Domain   Apply                Img
    FullFun Apply pprod    
Succ        |
258 | 256, 257 | syl6bbr 271 |
. . . . . . . . . 10
 
                                      
  Domain   Apply                Img     FullFun Apply pprod    
Succ        |
259 | 258 | con1bid 336 |
. . . . . . . . 9
 
   
Domain   Apply                Img     FullFun Apply pprod    
Succ                
                            |
260 | | df-ral 2753 |
. . . . . . . . 9
 
           
                     
                                       |
261 | 259, 260 | syl6bbr 271 |
. . . . . . . 8
 
   
Domain   Apply                Img     FullFun Apply pprod    
Succ                                           |
262 | 261 | pm5.32i 647 |
. . . . . . 7
  
  
Domain   Apply                Img     FullFun Apply pprod    
Succ     
 
 
           
                         |
263 | | anass 659 |
. . . . . . 7
  
                                    
                                         |
264 | 262, 263 | bitri 257 |
. . . . . 6
  
  
Domain   Apply                Img     FullFun Apply pprod    
Succ     
                                         |
265 | 21, 39, 264 | 3bitri 279 |
. . . . 5
    Domain     Domain   Apply                Img     FullFun Apply pprod    
Succ     
                                         |
266 | 19, 20, 265 | 3bitr4ri 286 |
. . . 4
    Domain     Domain   Apply                Img     FullFun Apply pprod    
Succ     
  
                                    |
267 | 266 | abbi2i 2576 |
. . 3
   Domain     Domain   Apply                Img     FullFun Apply pprod    
Succ         
                                    |
268 | 267 | unieqi 4220 |
. 2
  
 Domain  
 
Domain   Apply                Img     FullFun Apply pprod    
Succ        
            
                         |
269 | 1, 268 | eqtr4i 2486 |
1
  
     Domain     Domain   Apply                Img     FullFun Apply pprod    
Succ       |