Step | Hyp | Ref
| Expression |
1 | | domtriomlem.2 |
. . . . 5
 
    |
2 | | domtriomlem.1 |
. . . . . . 7
 |
3 | 2 | pwex 4586 |
. . . . . 6
  |
4 | | simpl 459 |
. . . . . . . 8
 
    |
5 | 4 | ss2abi 3501 |
. . . . . . 7
        |
6 | | df-pw 3953 |
. . . . . . 7
    |
7 | 5, 6 | sseqtr4i 3465 |
. . . . . 6
       |
8 | 3, 7 | ssexi 4548 |
. . . . 5
      |
9 | 1, 8 | eqeltri 2525 |
. . . 4
 |
10 | | omex 8148 |
. . . . 5
 |
11 | 10 | enref 7602 |
. . . 4
 |
12 | 9, 11 | axcc3 8868 |
. . 3
    
       |
13 | | nfv 1761 |
. . . . . . . 8

 |
14 | | nfra1 2769 |
. . . . . . . 8
  

      |
15 | 13, 14 | nfan 2011 |
. . . . . . 7
  
         |
16 | | nnfi 7765 |
. . . . . . . . . . . . . 14
   |
17 | | pwfi 7869 |
. . . . . . . . . . . . . 14

   |
18 | 16, 17 | sylib 200 |
. . . . . . . . . . . . 13
 
  |
19 | | ficardom 8395 |
. . . . . . . . . . . . 13
         |
20 | | isinf 7785 |
. . . . . . . . . . . . . 14
        |
21 | | breq2 4406 |
. . . . . . . . . . . . . . . . 17
      
        |
22 | 21 | anbi2d 710 |
. . . . . . . . . . . . . . . 16
       
 
         |
23 | 22 | exbidv 1768 |
. . . . . . . . . . . . . . 15
                       |
24 | 23 | rspcv 3146 |
. . . . . . . . . . . . . 14
           
  
         |
25 | 20, 24 | syl5 33 |
. . . . . . . . . . . . 13
                   |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . 12
 
            |
27 | | finnum 8382 |
. . . . . . . . . . . . . . 15
     |
28 | | cardid2 8387 |
. . . . . . . . . . . . . . 15
      
   |
29 | | entr 7621 |
. . . . . . . . . . . . . . . 16
           
 
   |
30 | 29 | expcom 437 |
. . . . . . . . . . . . . . 15
     
           |
31 | 18, 27, 28, 30 | 4syl 19 |
. . . . . . . . . . . . . 14
 
    
    |
32 | 31 | anim2d 569 |
. . . . . . . . . . . . 13
  
            |
33 | 32 | eximdv 1764 |
. . . . . . . . . . . 12
          
  
     |
34 | 26, 33 | syld 45 |
. . . . . . . . . . 11
 
        |
35 | 1 | neeq1i 2688 |
. . . . . . . . . . . 12
  
     |
36 | | abn0 3751 |
. . . . . . . . . . . 12
             |
37 | 35, 36 | bitri 253 |
. . . . . . . . . . 11
        |
38 | 34, 37 | syl6ibr 231 |
. . . . . . . . . 10
 
   |
39 | 38 | com12 32 |
. . . . . . . . 9
     |
40 | 39 | adantr 467 |
. . . . . . . 8
   
          |
41 | | rsp 2754 |
. . . . . . . . 9
 

    


        |
42 | 41 | adantl 468 |
. . . . . . . 8
   
                |
43 | 40, 42 | mpdd 41 |
. . . . . . 7
   
              |
44 | 15, 43 | ralrimi 2788 |
. . . . . 6
   
      
      |
45 | 44 | 3adant2 1027 |
. . . . 5
   
             |
46 | 45 | 3expib 1211 |
. . . 4
    
      
       |
47 | 46 | eximdv 1764 |
. . 3
     

        
       |
48 | 12, 47 | mpi 20 |
. 2
          |
49 | | axcc2 8867 |
. . . . 5
                    |
50 | | simp2 1009 |
. . . . . . . 8
      

                 |
51 | | nfra1 2769 |
. . . . . . . . . . 11
  
     |
52 | | nfra1 2769 |
. . . . . . . . . . 11
  
               |
53 | 51, 52 | nfan 2011 |
. . . . . . . . . 10
                         |
54 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
     |
55 | | sseq1 3453 |
. . . . . . . . . . . . . . . . 17
     
       |
56 | | breq1 4405 |
. . . . . . . . . . . . . . . . 17
     
         |
57 | 55, 56 | anbi12d 717 |
. . . . . . . . . . . . . . . 16
      
                |
58 | 54, 57, 1 | elab2 3188 |
. . . . . . . . . . . . . . 15
    
             |
59 | 58 | simprbi 466 |
. . . . . . . . . . . . . 14
            |
60 | 59 | ralimi 2781 |
. . . . . . . . . . . . 13
 
   
        |
61 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
62 | | pweq 3954 |
. . . . . . . . . . . . . . . . 17
 
   |
63 | 61, 62 | breq12d 4415 |
. . . . . . . . . . . . . . . 16
     
         |
64 | 63 | cbvralv 3019 |
. . . . . . . . . . . . . . 15
 
    
        |
65 | | peano2 6713 |
. . . . . . . . . . . . . . . . . 18

  |
66 | | omelon 8151 |
. . . . . . . . . . . . . . . . . . 19
 |
67 | 66 | onelssi 5531 |
. . . . . . . . . . . . . . . . . 18

  |
68 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . 18

     
           |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
  
   
           |
70 | | pwsdompw 8634 |
. . . . . . . . . . . . . . . . . 18
       
 
           |
71 | 70 | ex 436 |
. . . . . . . . . . . . . . . . 17
  
                  |
72 | 69, 71 | syld 45 |
. . . . . . . . . . . . . . . 16
  
   
             |
73 | | sdomdif 7720 |
. . . . . . . . . . . . . . . 16
 
       
             |
74 | 72, 73 | syl6 34 |
. . . . . . . . . . . . . . 15
  
   
      
        |
75 | 64, 74 | syl5bi 221 |
. . . . . . . . . . . . . 14
  
   
      
        |
76 | | difss 3560 |
. . . . . . . . . . . . . . . . 17
                |
77 | 54, 76 | ssexi 4548 |
. . . . . . . . . . . . . . . 16
            |
78 | | domtriomlem.3 |
. . . . . . . . . . . . . . . . 17
      
       |
79 | 78 | fvmpt2 5957 |
. . . . . . . . . . . . . . . 16
       
                       |
80 | 77, 79 | mpan2 677 |
. . . . . . . . . . . . . . 15
          
       |
81 | 80 | neeq1d 2683 |
. . . . . . . . . . . . . 14
     
              |
82 | 75, 81 | sylibrd 238 |
. . . . . . . . . . . . 13
  
   
        |
83 | 60, 82 | syl5com 31 |
. . . . . . . . . . . 12
 
   
        |
84 | 83 | adantr 467 |
. . . . . . . . . . 11
                               |
85 | | rsp 2754 |
. . . . . . . . . . . 12
 
                                |
86 | 85 | adantl 468 |
. . . . . . . . . . 11
                                         |
87 | 84, 86 | mpdd 41 |
. . . . . . . . . 10
                                   |
88 | 53, 87 | ralrimi 2788 |
. . . . . . . . 9
                       
          |
89 | 88 | 3adant2 1027 |
. . . . . . . 8
      

               
          |
90 | 50, 89 | jca 535 |
. . . . . . 7
      

                            |
91 | 90 | 3expib 1211 |
. . . . . 6
 
   
                                |
92 | 91 | eximdv 1764 |
. . . . 5
 
   
   
                                |
93 | 49, 92 | mpi 20 |
. . . 4
 
   
               |
94 | | simp2 1009 |
. . . . . . . . . 10
      

           |
95 | | nfra1 2769 |
. . . . . . . . . . . . 13
  
         |
96 | 51, 95 | nfan 2011 |
. . . . . . . . . . . 12
                   |
97 | | rsp 2754 |
. . . . . . . . . . . . . . . 16
 
       

           |
98 | 97 | com12 32 |
. . . . . . . . . . . . . . 15
  
                   |
99 | | rsp 2754 |
. . . . . . . . . . . . . . . . . 18
 
   
        |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . 17
  
           |
101 | 80 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . 19
         
        
         |
102 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . 19
          
               |
103 | 101, 102 | syl6bi 232 |
. . . . . . . . . . . . . . . . . 18
                     |
104 | 58 | simplbi 462 |
. . . . . . . . . . . . . . . . . . 19
           |
105 | 104 | sseld 3431 |
. . . . . . . . . . . . . . . . . 18
                     |
106 | 103, 105 | syl9 73 |
. . . . . . . . . . . . . . . . 17
                       |
107 | 100, 106 | syld 45 |
. . . . . . . . . . . . . . . 16
  
                     |
108 | 107 | com23 81 |
. . . . . . . . . . . . . . 15
                        |
109 | 98, 108 | syld 45 |
. . . . . . . . . . . . . 14
  
                      |
110 | 109 | com13 83 |
. . . . . . . . . . . . 13
 
   
 
       

        |
111 | 110 | imp 431 |
. . . . . . . . . . . 12
                         |
112 | 96, 111 | ralrimi 2788 |
. . . . . . . . . . 11
                        |
113 | 112 | 3adant2 1027 |
. . . . . . . . . 10
      

                |
114 | | ffnfv 6049 |
. . . . . . . . . 10
    
         |
115 | 94, 113, 114 | sylanbrc 670 |
. . . . . . . . 9
      

               |
116 | | nfv 1761 |
. . . . . . . . . . . 12

 |
117 | | nnord 6700 |
. . . . . . . . . . . . . . . 16
   |
118 | | nnord 6700 |
. . . . . . . . . . . . . . . 16
   |
119 | | ordtri3or 5455 |
. . . . . . . . . . . . . . . 16
       |
120 | 117, 118,
119 | syl2an 480 |
. . . . . . . . . . . . . . 15
 
 
   |
121 | 97, 101 | mpbidi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       

        
         |
122 | 95, 121 | ralrimi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
       
         
        |
123 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
124 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
125 | 124 | cbviunv 4317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

    
     |
126 | | iuneq1 4292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
    
      |
127 | 125, 126 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
    
      |
128 | 61, 127 | difeq12d 3552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
           
       |
129 | 123, 128 | eleq12d 2523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
        
         |
130 | 129 | rspccv 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
         
    

        
         |
131 | 122, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       

        
         |
132 | 131 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
                          |
133 | 132 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                           
         |
134 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
               |
135 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 
           |
136 | 134, 135 | syl5ib 223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                    |
137 | 136 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                  
                 |
138 | 133, 137 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                              |
139 | 138 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . 22
                     
          |
140 | | ssiun2 4321 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
141 | 140 | sseld 3431 |
. . . . . . . . . . . . . . . . . . . . . 22
              
       |
142 | 139, 141 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . 21
   
                  
    
       |
143 | 142 | 3impib 1206 |
. . . . . . . . . . . . . . . . . . . 20
                     
    
      |
144 | 121 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                          |
145 | 144 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                           
         |
146 | 145 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . 22
                     
        
        |
147 | 146 | eldifbd 3417 |
. . . . . . . . . . . . . . . . . . . . 21
                     
           |
148 | 147 | 3adant1 1026 |
. . . . . . . . . . . . . . . . . . . 20
                     
           |
149 | 143, 148 | pm2.21dd 178 |
. . . . . . . . . . . . . . . . . . 19
                     
  |
150 | 149 | 3exp 1207 |
. . . . . . . . . . . . . . . . . 18
                          |
151 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
                          |
152 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
153 | 152 | ssiun2s 4322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
154 | 153 | sseld 3431 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
       |
155 | 102, 154 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
156 | 146, 155 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . 21
   
                  
    
       |
157 | 156 | 3impib 1206 |
. . . . . . . . . . . . . . . . . . . 20
                     
    
      |
158 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                        
        
         |
159 | | eldifn 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
         
      |
160 | 158, 159 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             
       |
161 | 160 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                  
          
       |
162 | 133, 161 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                  
    
       |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
                     
    
        |
164 | 163 | 3imp 1202 |
. . . . . . . . . . . . . . . . . . . 20
                     
           |
165 | 157, 164 | pm2.21dd 178 |
. . . . . . . . . . . . . . . . . . 19
                     
  |
166 | 165 | 3exp 1207 |
. . . . . . . . . . . . . . . . . 18
                          |
167 | 150, 151,
166 | 3jaoi 1331 |
. . . . . . . . . . . . . . . . 17
               
            |
168 | 167 | com12 32 |
. . . . . . . . . . . . . . . 16
 
             
            |
169 | 168 | 3expia 1210 |
. . . . . . . . . . . . . . 15
 
           
  
             |
170 | 120, 169 | mpid 42 |
. . . . . . . . . . . . . 14
 
                        |
171 | 170 | com3r 82 |
. . . . . . . . . . . . 13
 
       
 
              |
172 | 171 | expd 438 |
. . . . . . . . . . . 12
 
       


              |
173 | 95, 116, 172 | ralrimd 2792 |
. . . . . . . . . . 11
 
       

         
    |
174 | 173 | ralrimiv 2800 |
. . . . . . . . . 10
 
       
          
   |
175 | 174 | 3ad2ant3 1031 |
. . . . . . . . 9
      

                   
   |
176 | | dff13 6159 |
. . . . . . . . 9
    
     
         
    |
177 | 115, 175,
176 | sylanbrc 670 |
. . . . . . . 8
      

               |
178 | | 19.8a 1935 |
. . . . . . . 8
     
      |
179 | 177, 178 | syl 17 |
. . . . . . 7
      

                |
180 | 2 | brdom 7581 |
. . . . . . 7
        |
181 | 179, 180 | sylibr 216 |
. . . . . 6
      

           |
182 | 181 | 3expib 1211 |
. . . . 5
 
   
               |
183 | 182 | exlimdv 1779 |
. . . 4
 
   
   
         
   |
184 | 93, 183 | mpd 15 |
. . 3
 
   
  |
185 | 184 | exlimiv 1776 |
. 2
          |
186 | 48, 185 | syl 17 |
1
   |