Step | Hyp | Ref
| Expression |
1 | | onzsl 6692 |
. . . 4

 
     |
2 | 1 | biimpi 199 |
. . 3
 


    |
3 | | cfom 8712 |
. . . . . . 7
     |
4 | | aleph0 8515 |
. . . . . . . 8
   
 |
5 | 4 | fveq2i 5882 |
. . . . . . 7
             |
6 | 3, 5, 4 | 3eqtr4i 2503 |
. . . . . 6
             |
7 | | fveq2 5879 |
. . . . . . 7

          |
8 | 7 | fveq2d 5883 |
. . . . . 6

                  |
9 | 6, 8, 7 | 3eqtr4a 2531 |
. . . . 5

              |
10 | | fvex 5889 |
. . . . . . . . 9
     |
11 | 10 | canth2 7743 |
. . . . . . . 8
          |
12 | 10 | pw2en 7697 |
. . . . . . . 8
     
      |
13 | | sdomentr 7724 |
. . . . . . . 8
          
     
     
            |
14 | 11, 12, 13 | mp2an 686 |
. . . . . . 7
           |
15 | | alephon 8518 |
. . . . . . . . 9
     |
16 | | alephgeom 8531 |
. . . . . . . . . 10

      |
17 | | omelon 8169 |
. . . . . . . . . . . 12
 |
18 | | 2onn 7359 |
. . . . . . . . . . . 12
 |
19 | | onelss 5472 |
. . . . . . . . . . . 12
     |
20 | 17, 18, 19 | mp2 9 |
. . . . . . . . . . 11
 |
21 | | sstr 3426 |
. . . . . . . . . . 11
 
    
      |
22 | 20, 21 | mpan 684 |
. . . . . . . . . 10
    
      |
23 | 16, 22 | sylbi 200 |
. . . . . . . . 9
       |
24 | | ssdomg 7633 |
. . . . . . . . 9
    
            |
25 | 15, 23, 24 | mpsyl 64 |
. . . . . . . 8
       |
26 | | mapdom1 7755 |
. . . . . . . 8
               
       |
27 | 25, 26 | syl 17 |
. . . . . . 7
                   |
28 | | sdomdomtr 7723 |
. . . . . . 7
                            
                |
29 | 14, 27, 28 | sylancr 676 |
. . . . . 6
         
       |
30 | | oveq2 6316 |
. . . . . . 7
                 
                     |
31 | 30 | breq2d 4407 |
. . . . . 6
                               
                 |
32 | 29, 31 | syl5ibrcom 230 |
. . . . 5
             
                     |
33 | 9, 32 | syl5 32 |
. . . 4
 
        
            |
34 | | alephreg 9025 |
. . . . . . 7
             |
35 | | fveq2 5879 |
. . . . . . . 8
           |
36 | 35 | fveq2d 5883 |
. . . . . . 7
                   |
37 | 34, 36, 35 | 3eqtr4a 2531 |
. . . . . 6
               |
38 | 37 | rexlimivw 2869 |
. . . . 5
                |
39 | 38, 32 | syl5 32 |
. . . 4
  
        
            |
40 | | cfsmo 8719 |
. . . . . 6
    
                  
      
                |
41 | | limelon 5493 |
. . . . . . . . . . 11
     |
42 | | ffn 5739 |
. . . . . . . . . . . . . . . 16
                           |
43 | | fnrnfv 5925 |
. . . . . . . . . . . . . . . . 17
        
 
                |
44 | 43 | unieqd 4200 |
. . . . . . . . . . . . . . . 16
                             |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . 15
                                     |
46 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
     |
47 | 46 | dfiun2 4303 |
. . . . . . . . . . . . . . 15
                                |
48 | 45, 47 | syl6eqr 2523 |
. . . . . . . . . . . . . 14
                                  |
49 | 48 | ad2antrl 742 |
. . . . . . . . . . . . 13
                                  
                       |
50 | | fnfvelrn 6034 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
51 | 42, 50 | sylan 479 |
. . . . . . . . . . . . . . . . . . . 20
                 
               |
52 | | sseq2 3440 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
53 | 52 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . 20
     
     
  |
54 | 51, 53 | sylan 479 |
. . . . . . . . . . . . . . . . . . 19
                  
                 |
55 | 54 | ex 441 |
. . . . . . . . . . . . . . . . . 18
                 
             
    |
56 | 55 | rexlimdva 2871 |
. . . . . . . . . . . . . . . . 17
                           
        |
57 | 56 | ralimdv 2806 |
. . . . . . . . . . . . . . . 16
                        
            
      
   |
58 | 57 | imp 436 |
. . . . . . . . . . . . . . 15
                 
      
                    
  |
59 | 58 | adantl 473 |
. . . . . . . . . . . . . 14
                                  
            
  |
60 | | alephislim 8532 |
. . . . . . . . . . . . . . . 16

      |
61 | 60 | biimpi 199 |
. . . . . . . . . . . . . . 15
       |
62 | | frn 5747 |
. . . . . . . . . . . . . . . 16
                       |
63 | 62 | adantr 472 |
. . . . . . . . . . . . . . 15
                 
      
                    |
64 | | coflim 8709 |
. . . . . . . . . . . . . . 15
     
    
 
   
      
   |
65 | 61, 63, 64 | syl2an 485 |
. . . . . . . . . . . . . 14
                                  
       
   
      
   |
66 | 59, 65 | mpbird 240 |
. . . . . . . . . . . . 13
                                  
             |
67 | 49, 66 | eqtr3d 2507 |
. . . . . . . . . . . 12
                                  
                          |
68 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . 17
                 
                   |
69 | 15 | oneli 5537 |
. . . . . . . . . . . . . . . . 17
        
      |
70 | | harcard 8430 |
. . . . . . . . . . . . . . . . . . 19
   har       har       |
71 | | iscard 8427 |
. . . . . . . . . . . . . . . . . . . 20
    har       har     
 har       har       har         |
72 | 71 | simprbi 471 |
. . . . . . . . . . . . . . . . . . 19
    har       har      
har       har        |
73 | 70, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 har       har       |
74 | | domrefg 7622 |
. . . . . . . . . . . . . . . . . . . 20
               |
75 | 46, 74 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
         |
76 | | elharval 8096 |
. . . . . . . . . . . . . . . . . . . 20
     har                      |
77 | 76 | biimpri 211 |
. . . . . . . . . . . . . . . . . . 19
                   har        |
78 | 75, 77 | mpan2 685 |
. . . . . . . . . . . . . . . . . 18
         har        |
79 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . 19
      har          har         |
80 | 79 | rspccv 3133 |
. . . . . . . . . . . . . . . . . 18
 
har       har           har          har         |
81 | 73, 78, 80 | mpsyl 64 |
. . . . . . . . . . . . . . . . 17
         har        |
82 | 68, 69, 81 | 3syl 18 |
. . . . . . . . . . . . . . . 16
                 
             har        |
83 | | harcl 8094 |
. . . . . . . . . . . . . . . . . . 19
har       |
84 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
85 | 84 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
 har      har        |
86 | | pwcfsdom.1 |
. . . . . . . . . . . . . . . . . . . 20
         har        |
87 | 85, 86 | fvmptg 5961 |
. . . . . . . . . . . . . . . . . . 19
         
har           har        |
88 | 83, 87 | mpan2 685 |
. . . . . . . . . . . . . . . . . 18
             har        |
89 | 88 | breq2d 4407 |
. . . . . . . . . . . . . . . . 17
                      har         |
90 | 89 | adantl 473 |
. . . . . . . . . . . . . . . 16
                 
                      har         |
91 | 82, 90 | mpbird 240 |
. . . . . . . . . . . . . . 15
                 
                   |
92 | 91 | ralrimiva 2809 |
. . . . . . . . . . . . . 14
                                     |
93 | | fvex 5889 |
. . . . . . . . . . . . . . 15
         |
94 | | eqid 2471 |
. . . . . . . . . . . . . . 15
                             |
95 | | eqid 2471 |
. . . . . . . . . . . . . . 15
                             |
96 | 93, 94, 95 | konigth 9012 |
. . . . . . . . . . . . . 14
 
                                               |
97 | 92, 96 | syl 17 |
. . . . . . . . . . . . 13
                                               |
98 | 97 | ad2antrl 742 |
. . . . . . . . . . . 12
                                  
                                    |
99 | 67, 98 | eqbrtrrd 4418 |
. . . . . . . . . . 11
                                  
                          |
100 | 41, 99 | sylan 479 |
. . . . . . . . . 10
                                    
                          |
101 | | ovex 6336 |
. . . . . . . . . . . 12
               |
102 | 68 | ex 441 |
. . . . . . . . . . . . . . . 16
                                     |
103 | | alephlim 8516 |
. . . . . . . . . . . . . . . . . 18
              |
104 | 103 | eleq2d 2534 |
. . . . . . . . . . . . . . . . 17
           
    
       |
105 | | eliun 4274 |
. . . . . . . . . . . . . . . . . . 19
                     |
106 | | alephcard 8519 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
107 | 106 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
108 | | cardsdomelir 8425 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
109 | 107, 108 | sylbir 218 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
          |
110 | | elharval 8096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     har     
                |
111 | 110 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     har                |
112 | | domnsym 7716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
          |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     har                |
114 | 113 | con2i 124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             har        |
115 | | alephon 8518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
116 | | ontri1 5464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  har            har         
    har         |
117 | 83, 115, 116 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 har              har        |
118 | 114, 117 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
         har            |
119 | 109, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
        
har     
      |
120 | | alephord2i 8526 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
121 | 120 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
122 | | ontr2 5477 |
. . . . . . . . . . . . . . . . . . . . . . 23
  har             har                  
har             |
123 | 83, 15, 122 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . . 22
  har                  
har            |
124 | 119, 121,
123 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . 21
             har            |
125 | 124 | exp31 615 |
. . . . . . . . . . . . . . . . . . . 20
           har              |
126 | 125 | rexlimdv 2870 |
. . . . . . . . . . . . . . . . . . 19
  
        har             |
127 | 105, 126 | syl5bi 225 |
. . . . . . . . . . . . . . . . . 18
      
    har             |
128 | 41, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
        
    har             |
129 | 104, 128 | sylbid 223 |
. . . . . . . . . . . . . . . 16
            har             |
130 | 102, 129 | sylan9r 670 |
. . . . . . . . . . . . . . 15
                    
         har             |
131 | 130 | imp 436 |
. . . . . . . . . . . . . 14
   
                           har            |
132 | 85 | cbvmptv 4488 |
. . . . . . . . . . . . . . 15
         har                har        |
133 | 86, 132 | eqtri 2493 |
. . . . . . . . . . . . . 14
         har        |
134 | 131, 133 | fmptd 6061 |
. . . . . . . . . . . . 13
                    
                  |
135 | | ffvelrn 6035 |
. . . . . . . . . . . . . . 15
                 
                   |
136 | | onelss 5472 |
. . . . . . . . . . . . . . 15
    
            
       |
137 | 15, 135, 136 | mpsyl 64 |
. . . . . . . . . . . . . 14
                 
                   |
138 | 137 | ralrimiva 2809 |
. . . . . . . . . . . . 13
                                     |
139 | | ss2ixp 7553 |
. . . . . . . . . . . . . 14
 
                                               |
140 | 93, 10 | ixpconst 7550 |
. . . . . . . . . . . . . 14
                             |
141 | 139, 140 | syl6sseq 3464 |
. . . . . . . . . . . . 13
 
                                               |
142 | 134, 138,
141 | 3syl 18 |
. . . . . . . . . . . 12
                    
             
                |
143 | | ssdomg 7633 |
. . . . . . . . . . . 12
                                                                           |
144 | 101, 142,
143 | mpsyl 64 |
. . . . . . . . . . 11
                    
                              |
145 | 144 | adantrr 731 |
. . . . . . . . . 10
                                    
                        
           |
146 | | sdomdomtr 7723 |
. . . . . . . . . 10
                                      
                  
           |
147 | 100, 145,
146 | syl2anc 673 |
. . . . . . . . 9
                                    
                          |
148 | 147 | expcom 442 |
. . . . . . . 8
                 
      
                         
            |
149 | 148 | 3adant2 1049 |
. . . . . . 7
                 
               
      
                      |
150 | 149 | exlimiv 1784 |
. . . . . 6
                    
              
      
                      |
151 | 15, 40, 150 | mp2b 10 |
. . . . 5
           
           |
152 | 151 | a1i 11 |
. . . 4
            
            |
153 | 33, 39, 152 | 3jaod 1358 |
. . 3
   
                        |
154 | 2, 153 | mpd 15 |
. 2
         
           |
155 | | alephfnon 8514 |
. . . . 5
 |
156 | | fndm 5685 |
. . . . 5

  |
157 | 155, 156 | ax-mp 5 |
. . . 4
 |
158 | 157 | eleq2i 2541 |
. . 3

  |
159 | | ndmfv 5903 |
. . . 4
       |
160 | | 1n0 7215 |
. . . . . 6
 |
161 | | 1on 7207 |
. . . . . . . 8
 |
162 | 161 | elexi 3041 |
. . . . . . 7
 |
163 | 162 | 0sdom 7721 |
. . . . . 6
   |
164 | 160, 163 | mpbir 214 |
. . . . 5
 |
165 | | id 22 |
. . . . . 6
           |
166 | | fveq2 5879 |
. . . . . . . . 9
                   |
167 | | cf0 8699 |
. . . . . . . . 9
   
 |
168 | 166, 167 | syl6eq 2521 |
. . . . . . . 8
               |
169 | 165, 168 | oveq12d 6326 |
. . . . . . 7
                   
   |
170 | | 0ex 4528 |
. . . . . . . 8
 |
171 | | map0e 7527 |
. . . . . . . 8

    |
172 | 170, 171 | ax-mp 5 |
. . . . . . 7
 
 |
173 | 169, 172 | syl6eq 2521 |
. . . . . 6
                     |
174 | 165, 173 | breq12d 4408 |
. . . . 5
                       
   |
175 | 164, 174 | mpbiri 241 |
. . . 4
                         |
176 | 159, 175 | syl 17 |
. . 3
         
           |
177 | 158, 176 | sylnbir 314 |
. 2
         
           |
178 | 154, 177 | pm2.61i 169 |
1
                   |