Step | Hyp | Ref
| Expression |
1 | | iccssxr 11714 |
. . . . . . 7
    |
2 | | carsgval.2 |
. . . . . . . 8
           |
3 | | carsgclctunlem3.1 |
. . . . . . . . 9
    |
4 | 3 | elpwincl1 28147 |
. . . . . . . 8
       |
5 | 2, 4 | ffvelrnd 6021 |
. . . . . . 7
             |
6 | 1, 5 | sseldi 3429 |
. . . . . 6
          |
7 | 3 | elpwdifcl 28148 |
. . . . . . . 8
       |
8 | 2, 7 | ffvelrnd 6021 |
. . . . . . 7
             |
9 | 1, 8 | sseldi 3429 |
. . . . . 6
          |
10 | 6, 9 | xaddcld 11584 |
. . . . 5
     
                |
11 | 10 | adantr 467 |
. . . 4
 
                   
      |
12 | | pnfge 11429 |
. . . 4
                                      
  |
13 | 11, 12 | syl 17 |
. . 3
 
                   
      |
14 | | simpr 463 |
. . 3
 
           |
15 | 13, 14 | breqtrrd 4428 |
. 2
 
                   
          |
16 | | unieq 4205 |
. . . . . . . . . . . . 13

    |
17 | | uni0 4224 |
. . . . . . . . . . . . 13
  |
18 | 16, 17 | syl6eq 2500 |
. . . . . . . . . . . 12

   |
19 | 18 | ineq2d 3633 |
. . . . . . . . . . 11

       |
20 | | in0 3759 |
. . . . . . . . . . 11
   |
21 | 19, 20 | syl6eq 2500 |
. . . . . . . . . 10

     |
22 | 21 | fveq2d 5867 |
. . . . . . . . 9

             |
23 | 18 | difeq2d 3550 |
. . . . . . . . . . 11

       |
24 | | dif0 3836 |
. . . . . . . . . . 11
   |
25 | 23, 24 | syl6eq 2500 |
. . . . . . . . . 10

     |
26 | 25 | fveq2d 5867 |
. . . . . . . . 9

             |
27 | 22, 26 | oveq12d 6306 |
. . . . . . . 8

                                  |
28 | 27 | adantl 468 |
. . . . . . 7
 

                                  |
29 | | carsgsiga.1 |
. . . . . . . . 9
       |
30 | 29 | adantr 467 |
. . . . . . . 8
 

      |
31 | 30 | oveq1d 6303 |
. . . . . . 7
 

                        |
32 | 2, 3 | ffvelrnd 6021 |
. . . . . . . . . 10
          |
33 | 1, 32 | sseldi 3429 |
. . . . . . . . 9
       |
34 | 33 | adantr 467 |
. . . . . . . 8
 

      |
35 | | xaddid2 11530 |
. . . . . . . 8
    
               |
36 | 34, 35 | syl 17 |
. . . . . . 7
 

               |
37 | 28, 31, 36 | 3eqtrd 2488 |
. . . . . 6
 

                         |
38 | 37, 34 | eqeltrd 2528 |
. . . . . . 7
 

                     |
39 | | xeqlelt 28351 |
. . . . . . 7
      
                                  
                           
        
                      |
40 | 38, 34, 39 | syl2anc 666 |
. . . . . 6
 

                       
                   
        
                      |
41 | 37, 40 | mpbid 214 |
. . . . 5
 

                   
        
                     |
42 | 41 | simpld 461 |
. . . 4
 

                         |
43 | 42 | adantlr 720 |
. . 3
                           
      |
44 | | carsgclctun.2 |
. . . . . . . 8

toCaraSiga    |
45 | | fvex 5873 |
. . . . . . . . 9
toCaraSiga   |
46 | | ssexg 4548 |
. . . . . . . . 9
 
toCaraSiga 
toCaraSiga     |
47 | 45, 46 | mpan2 676 |
. . . . . . . 8
 toCaraSiga 
  |
48 | | 0sdomg 7698 |
. . . . . . . 8
 
   |
49 | 44, 47, 48 | 3syl 18 |
. . . . . . 7
 
   |
50 | 49 | biimpar 488 |
. . . . . 6
 

  |
51 | 50 | adantlr 720 |
. . . . 5
           |
52 | | carsgclctun.1 |
. . . . . . 7
   |
53 | | nnenom 12190 |
. . . . . . . 8
 |
54 | | ensymb 7614 |
. . . . . . . 8

  |
55 | 53, 54 | mpbi 212 |
. . . . . . 7
 |
56 | | domentr 7625 |
. . . . . . 7
 

  |
57 | 52, 55, 56 | sylancl 667 |
. . . . . 6
   |
58 | 57 | ad2antrr 731 |
. . . . 5
           |
59 | | fodomr 7720 |
. . . . 5
  
       |
60 | 51, 58, 59 | syl2anc 666 |
. . . 4
                |
61 | | fveq2 5863 |
. . . . . . . . . 10
           |
62 | 61 | iundisj 22494 |
. . . . . . . . 9
     
    
  ..^        |
63 | | fofn 5793 |
. . . . . . . . . . . 12
       |
64 | | fniunfv 6150 |
. . . . . . . . . . . 12
         |
65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
     
       |
66 | | forn 5794 |
. . . . . . . . . . . 12
    
  |
67 | 66 | unieqd 4207 |
. . . . . . . . . . 11
         |
68 | 65, 67 | eqtrd 2484 |
. . . . . . . . . 10
     
       |
69 | 68 | adantl 468 |
. . . . . . . . 9
                       |
70 | 62, 69 | syl5eqr 2498 |
. . . . . . . 8
                     
 ..^          |
71 | 70 | ineq2d 3633 |
. . . . . . 7
                      
 ..^             |
72 | 71 | fveq2d 5867 |
. . . . . 6
                         
 ..^                  |
73 | 70 | difeq2d 3550 |
. . . . . . 7
                      
 ..^             |
74 | 73 | fveq2d 5867 |
. . . . . 6
                         
 ..^                  |
75 | 72, 74 | oveq12d 6306 |
. . . . 5
                          
 ..^                      
 ..^                        
      |
76 | | carsgval.1 |
. . . . . . 7
   |
77 | 76 | ad3antrrr 735 |
. . . . . 6
                 |
78 | 2 | ad3antrrr 735 |
. . . . . 6
                         |
79 | 29 | ad3antrrr 735 |
. . . . . 6
                     |
80 | | carsgsiga.2 |
. . . . . . . . 9
 
      
Σ*        |
81 | 80 | 3adant1r 1260 |
. . . . . . . 8
               Σ*        |
82 | 81 | 3adant1r 1260 |
. . . . . . 7
                 Σ*        |
83 | 82 | 3adant1r 1260 |
. . . . . 6
         
            
Σ*        |
84 | | carsgsiga.3 |
. . . . . . . . 9
 
            |
85 | 84 | 3adant1r 1260 |
. . . . . . . 8
             
      |
86 | 85 | 3adant1r 1260 |
. . . . . . 7
               
      |
87 | 86 | 3adant1r 1260 |
. . . . . 6
         
     
            |
88 | 61 | iundisj2 22495 |
. . . . . . 7
Disj      
 ..^        |
89 | 88 | a1i 11 |
. . . . . 6
               Disj      
 ..^         |
90 | 77 | adantr 467 |
. . . . . . 7
         
         |
91 | 78 | adantr 467 |
. . . . . . 7
         
                 |
92 | 44 | ad4antr 737 |
. . . . . . . 8
         
       toCaraSiga    |
93 | | fof 5791 |
. . . . . . . . . 10
           |
94 | 93 | ad2antlr 732 |
. . . . . . . . 9
         
             |
95 | | simpr 463 |
. . . . . . . . 9
         
         |
96 | 94, 95 | ffvelrnd 6021 |
. . . . . . . 8
         
             |
97 | 92, 96 | sseldd 3432 |
. . . . . . 7
         
           toCaraSiga    |
98 | 79 | adantr 467 |
. . . . . . . 8
         
             |
99 | 83 | 3adant1r 1260 |
. . . . . . . 8
     
                  
Σ*        |
100 | 90, 91, 98, 99 | carsgsigalem 29140 |
. . . . . . 7
     
                                    |
101 | 93 | ad3antlr 736 |
. . . . . . . . . . 11
     
             ..^        |
102 | | fzossnn 11961 |
. . . . . . . . . . . . 13
 ..^  |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
         
        ..^
  |
104 | 103 | sselda 3431 |
. . . . . . . . . . 11
     
             ..^    |
105 | 101, 104 | ffvelrnd 6021 |
. . . . . . . . . 10
     
             ..^        |
106 | 105 | ralrimiva 2801 |
. . . . . . . . 9
         
         ..^        |
107 | | dfiun2g 4309 |
. . . . . . . . 9
 
 ..^     
  ..^          ..^         |
108 | 106, 107 | syl 17 |
. . . . . . . 8
         
         ..^          ..^         |
109 | | eqid 2450 |
. . . . . . . . . . . 12
  ..^        ..^       |
110 | 109 | rnmpt 5079 |
. . . . . . . . . . 11
  ..^         ..^        |
111 | | fzofi 12184 |
. . . . . . . . . . . 12
 ..^  |
112 | | mptfi 7870 |
. . . . . . . . . . . 12
  ..^   ..^        |
113 | | rnfi 7854 |
. . . . . . . . . . . 12
   ..^        ..^        |
114 | 111, 112,
113 | mp2b 10 |
. . . . . . . . . . 11
  ..^       |
115 | 110, 114 | eqeltrri 2525 |
. . . . . . . . . 10
   ..^        |
116 | 115 | a1i 11 |
. . . . . . . . 9
         
          ..^         |
117 | 92 | adantr 467 |
. . . . . . . . . . . . 13
     
             ..^  toCaraSiga    |
118 | 117, 105 | sseldd 3432 |
. . . . . . . . . . . 12
     
             ..^      toCaraSiga    |
119 | 118 | ralrimiva 2801 |
. . . . . . . . . . 11
         
         ..^      toCaraSiga    |
120 | 109 | rnmptss 6050 |
. . . . . . . . . . 11
 
 ..^      toCaraSiga    ..^     
toCaraSiga    |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
         
      
  ..^      toCaraSiga    |
122 | 110, 121 | syl5eqssr 3476 |
. . . . . . . . 9
         
          ..^       toCaraSiga    |
123 | 90, 91, 98, 99, 116, 122 | fiunelcarsg 29141 |
. . . . . . . 8
         
           ..^       toCaraSiga    |
124 | 108, 123 | eqeltrd 2528 |
. . . . . . 7
         
         ..^      toCaraSiga    |
125 | 90, 91, 97, 100, 124 | difelcarsg2 29138 |
. . . . . 6
         
            
 ..^       toCaraSiga    |
126 | 3 | ad3antrrr 735 |
. . . . . 6
                  |
127 | | simpllr 768 |
. . . . . 6
                     |
128 | 77, 78, 79, 83, 87, 89, 125, 126, 127 | carsgclctunlem2 29144 |
. . . . 5
                          
 ..^                      
 ..^                |
129 | 75, 128 | eqbrtrrd 4424 |
. . . 4
                                 
      |
130 | 60, 129 | exlimddv 1780 |
. . 3
                           
      |
131 | 43, 130 | pm2.61dane 2710 |
. 2
 
                   
          |
132 | 15, 131 | pm2.61dane 2710 |
1
     
                    |