Step | Hyp | Ref
| Expression |
1 | | ensym 7605 |
. 2
     
     |
2 | | bren 7565 |
. . 3
    
           |
3 | | ssdif0 3791 |
. . . . . 6
   
                     |
4 | | dmxpid 5032 |
. . . . . . . . . . . . . 14
   |
5 | | f1ofo 5804 |
. . . . . . . . . . . . . . . . 17
        
          |
6 | | forn 5779 |
. . . . . . . . . . . . . . . . 17
        
    |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . 16
        
    |
8 | | vex 3016 |
. . . . . . . . . . . . . . . . 17
 |
9 | 8 | rnex 6715 |
. . . . . . . . . . . . . . . 16
 |
10 | 7, 9 | syl6eqelr 2539 |
. . . . . . . . . . . . . . 15
        
    |
11 | | dmexg 6712 |
. . . . . . . . . . . . . . 15
   
   |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . 14
        
    |
13 | 4, 12 | syl5eqelr 2535 |
. . . . . . . . . . . . 13
        
  |
14 | | imassrn 5157 |
. . . . . . . . . . . . . 14
                 |
15 | | f1stres 6803 |
. . . . . . . . . . . . . . . 16
           |
16 | | f1of 5797 |
. . . . . . . . . . . . . . . 16
        
          |
17 | | fco 5722 |
. . . . . . . . . . . . . . . 16
                                   |
18 | 15, 16, 17 | sylancr 674 |
. . . . . . . . . . . . . . 15
        
              |
19 | | frn 5718 |
. . . . . . . . . . . . . . 15
                     |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
        
 
      |
21 | 14, 20 | syl5ss 3411 |
. . . . . . . . . . . . 13
        
  
         |
22 | 13, 21 | ssexd 4522 |
. . . . . . . . . . . 12
        
  
         |
23 | 22 | adantr 471 |
. . . . . . . . . . 11
            
                    |
24 | | simpr 467 |
. . . . . . . . . . 11
            
                    |
25 | | ssdomg 7602 |
. . . . . . . . . . 11
                                   |
26 | 23, 24, 25 | sylc 62 |
. . . . . . . . . 10
            
                    |
27 | | domwdom 8076 |
. . . . . . . . . 10
           *             |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
            
        *             |
29 | | ffun 5714 |
. . . . . . . . . . . 12
                     |
30 | 18, 29 | syl 17 |
. . . . . . . . . . 11
        
 
      |
31 | | ssun1 3565 |
. . . . . . . . . . . 12

  |
32 | | f1odm 5801 |
. . . . . . . . . . . . 13
        
    |
33 | 8 | dmex 6714 |
. . . . . . . . . . . . 13
 |
34 | 32, 33 | syl6eqelr 2539 |
. . . . . . . . . . . 12
        
    |
35 | | ssexg 4521 |
. . . . . . . . . . . 12
 
  
    |
36 | 31, 34, 35 | sylancr 674 |
. . . . . . . . . . 11
        
  |
37 | | wdomima2g 8088 |
. . . . . . . . . . 11
       
  
                  *   |
38 | 30, 36, 22, 37 | syl3anc 1271 |
. . . . . . . . . 10
        
  
       *   |
39 | 38 | adantr 471 |
. . . . . . . . 9
            
                  *   |
40 | | wdomtr 8077 |
. . . . . . . . 9
  *             
       *  *   |
41 | 28, 39, 40 | syl2anc 671 |
. . . . . . . 8
            
        *   |
42 | 41 | orcd 398 |
. . . . . . 7
            
         *    |
43 | 42 | ex 440 |
. . . . . 6
        
            *
    |
44 | 3, 43 | syl5bir 226 |
. . . . 5
        
    
         *     |
45 | | n0 3709 |
. . . . . 6
                            |
46 | | ssun2 3566 |
. . . . . . . . . . . . 13

  |
47 | | ssexg 4521 |
. . . . . . . . . . . . 13
 
  
    |
48 | 46, 34, 47 | sylancr 674 |
. . . . . . . . . . . 12
        
  |
49 | 48 | adantr 471 |
. . . . . . . . . . 11
         
               |
50 | | f1ofn 5798 |
. . . . . . . . . . . . . . 15
        

   |
51 | | elpreima 5986 |
. . . . . . . . . . . . . . 15
            
  
            |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . 14
        
         
  
            |
53 | 52 | adantr 471 |
. . . . . . . . . . . . 13
         
                      
  
            |
54 | | elun 3542 |
. . . . . . . . . . . . . . . 16
  

   |
55 | | df-or 376 |
. . . . . . . . . . . . . . . 16
 
     |
56 | 54, 55 | bitri 257 |
. . . . . . . . . . . . . . 15
  

   |
57 | | eldifn 3524 |
. . . . . . . . . . . . . . . . . . 19
            
            |
58 | 57 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . 18
                                
            |
59 | 16 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
                                             |
60 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                     |
61 | 31, 60 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
62 | | fvco3 5926 |
. . . . . . . . . . . . . . . . . . . . . 22
            
  
                     |
63 | 59, 61, 62 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . 21
                                                           |
64 | | eldifi 3523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
  |
65 | 64 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
               |
66 | 65 | snssd 4086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
                 |
67 | | xpss1 4921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
                     |
69 | 68 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                           |
70 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                             |
71 | 69, 70 | sseldd 3401 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                           |
72 | | fvres 5862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
                    |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                         |
74 | | xp1st 6811 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
75 | 70, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                               |
76 | 73, 75 | eqeltrd 2530 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                   |
77 | | elsni 3961 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
79 | 63, 78 | eqtrd 2486 |
. . . . . . . . . . . . . . . . . . . 20
                                               |
80 | | ffn 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
        |
81 | 18, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
        
      
   |
82 | 81 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
83 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
84 | | fnfvima 6129 |
. . . . . . . . . . . . . . . . . . . . 21
         



  
                   |
85 | 82, 83, 60, 84 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . 20
                                                         |
86 | 79, 85 | eqeltrrd 2531 |
. . . . . . . . . . . . . . . . . . 19
                                  
  
         |
87 | 86 | expr 624 |
. . . . . . . . . . . . . . . . . 18
                                               |
88 | 58, 87 | mtod 182 |
. . . . . . . . . . . . . . . . 17
                                
  |
89 | 88 | ex 440 |
. . . . . . . . . . . . . . . 16
         
                     
   |
90 | 89 | imim1d 78 |
. . . . . . . . . . . . . . 15
         
              
         
    |
91 | 56, 90 | syl5bi 225 |
. . . . . . . . . . . . . 14
         
                             |
92 | 91 | impd 437 |
. . . . . . . . . . . . 13
         
                             |
93 | 53, 92 | sylbid 223 |
. . . . . . . . . . . 12
         
                          |
94 | 93 | ssrdv 3406 |
. . . . . . . . . . 11
         
                        |
95 | | ssdomg 7602 |
. . . . . . . . . . 11
                       |
96 | 49, 94, 95 | sylc 62 |
. . . . . . . . . 10
         
                        |
97 | | f1ocnv 5809 |
. . . . . . . . . . . . . . 15
        
           |
98 | | f1of1 5796 |
. . . . . . . . . . . . . . 15
                     |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . 14
        
           |
100 | 99 | adantr 471 |
. . . . . . . . . . . . 13
         
                        |
101 | 34 | adantr 471 |
. . . . . . . . . . . . 13
         
             
   |
102 | | snex 4614 |
. . . . . . . . . . . . . 14
 
 |
103 | 13 | adantr 471 |
. . . . . . . . . . . . . 14
         
               |
104 | | xpexg 6581 |
. . . . . . . . . . . . . 14
           |
105 | 102, 103,
104 | sylancr 674 |
. . . . . . . . . . . . 13
         
                   |
106 | | f1imaen2g 7617 |
. . . . . . . . . . . . 13
            
                              |
107 | 100, 101,
68, 105, 106 | syl22anc 1272 |
. . . . . . . . . . . 12
         
                            |
108 | | vex 3016 |
. . . . . . . . . . . . 13
 |
109 | | xpsnen2g 7652 |
. . . . . . . . . . . . 13
 
       |
110 | 108, 103,
109 | sylancr 674 |
. . . . . . . . . . . 12
         
                   |
111 | | entr 7608 |
. . . . . . . . . . . 12
                   
           |
112 | 107, 110,
111 | syl2anc 671 |
. . . . . . . . . . 11
         
                        |
113 | | domen1 7701 |
. . . . . . . . . . 11
                   
   |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
         
                          |
115 | 96, 114 | mpbid 215 |
. . . . . . . . 9
         
               |
116 | 115 | olcd 399 |
. . . . . . . 8
         
              *    |
117 | 116 | ex 440 |
. . . . . . 7
        
              *     |
118 | 117 | exlimdv 1783 |
. . . . . 6
        
 
   
         *     |
119 | 45, 118 | syl5bi 225 |
. . . . 5
        
    
         *     |
120 | 44, 119 | pm2.61dne 2710 |
. . . 4
        
 *    |
121 | 120 | exlimiv 1780 |
. . 3
           *
   |
122 | 2, 121 | sylbi 200 |
. 2
      *    |
123 | 1, 122 | syl 17 |
1
      *    |