Step | Hyp | Ref
| Expression |
1 | | infxpidm2 8479 |
. . . . . . 7
    
  |
2 | | infn0 7864 |
. . . . . . . 8

  |
3 | 2 | adantl 472 |
. . . . . . 7
     |
4 | | fseqen 8489 |
. . . . . . 7
   
        |
5 | 1, 3, 4 | syl2anc 671 |
. . . . . 6
   


    |
6 | | xpdom1g 7700 |
. . . . . . 7
         |
7 | | domentr 7659 |
. . . . . . 7
             |
8 | 6, 1, 7 | syl2anc 671 |
. . . . . 6
       |
9 | | endomtr 7658 |
. . . . . 6
   

    
     |
10 | 5, 8, 9 | syl2anc 671 |
. . . . 5
   

   |
11 | | numdom 8500 |
. . . . 5
   
  

   |
12 | 10, 11 | syldan 477 |
. . . 4
   

   |
13 | | eliun 4297 |
. . . . . . . . 9
   
     |
14 | | elmapi 7524 |
. . . . . . . . . . . . . . 15
         |
15 | 14 | ad2antll 740 |
. . . . . . . . . . . . . 14
    
   
      |
16 | | frn 5762 |
. . . . . . . . . . . . . 14
    
  |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
    
   
  |
18 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
19 | 18 | rnex 6759 |
. . . . . . . . . . . . . 14
 |
20 | 19 | elpw 3969 |
. . . . . . . . . . . . 13
 
  |
21 | 17, 20 | sylibr 217 |
. . . . . . . . . . . 12
    
   
   |
22 | | simprl 769 |
. . . . . . . . . . . . . 14
    
   
  |
23 | | ssid 3463 |
. . . . . . . . . . . . . 14
 |
24 | | ssnnfi 7822 |
. . . . . . . . . . . . . 14
  
  |
25 | 22, 23, 24 | sylancl 673 |
. . . . . . . . . . . . 13
    
   
  |
26 | | ffn 5755 |
. . . . . . . . . . . . . . 15
    
  |
27 | | dffn4 5826 |
. . . . . . . . . . . . . . 15

      |
28 | 26, 27 | sylib 201 |
. . . . . . . . . . . . . 14
           |
29 | 15, 28 | syl 17 |
. . . . . . . . . . . . 13
    
   
      |
30 | | fofi 7891 |
. . . . . . . . . . . . 13
      
  |
31 | 25, 29, 30 | syl2anc 671 |
. . . . . . . . . . . 12
    
   
  |
32 | 21, 31 | elind 3630 |
. . . . . . . . . . 11
    
   
     |
33 | 32 | expr 624 |
. . . . . . . . . 10
   
   
      |
34 | 33 | rexlimdva 2891 |
. . . . . . . . 9
      
      |
35 | 13, 34 | syl5bi 225 |
. . . . . . . 8
    
        |
36 | 35 | imp 435 |
. . . . . . 7
   
         |
37 | | eqid 2462 |
. . . . . . 7
           |
38 | 36, 37 | fmptd 6074 |
. . . . . 6
    
     
         |
39 | | ffn 5755 |
. . . . . 6
                 
   
    |
40 | 38, 39 | syl 17 |
. . . . 5
    
   
    |
41 | | frn 5762 |
. . . . . . 7
                  

      |
42 | 38, 41 | syl 17 |
. . . . . 6
    
    
   |
43 | | inss2 3665 |
. . . . . . . . . . . 12
    |
44 | | simpr 467 |
. . . . . . . . . . . 12
   
         |
45 | 43, 44 | sseldi 3442 |
. . . . . . . . . . 11
   
      |
46 | | isfi 7624 |
. . . . . . . . . . 11

   |
47 | 45, 46 | sylib 201 |
. . . . . . . . . 10
   
       |
48 | | ensym 7649 |
. . . . . . . . . . . . 13
   |
49 | | bren 7609 |
. . . . . . . . . . . . 13

       |
50 | 48, 49 | sylib 201 |
. . . . . . . . . . . 12
        |
51 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
   
           
  |
52 | | f1of 5841 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
53 | 52 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . 19
   
                  |
54 | | inss1 3664 |
. . . . . . . . . . . . . . . . . . . . 21
     |
55 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . 21
   
                 |
56 | 54, 55 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . . 20
   
               |
57 | 56 | elpwid 3973 |
. . . . . . . . . . . . . . . . . . 19
   
           
  |
58 | 53, 57 | fssd 5765 |
. . . . . . . . . . . . . . . . . 18
   
                  |
59 | | simplll 773 |
. . . . . . . . . . . . . . . . . . 19
   
           
  |
60 | | vex 3060 |
. . . . . . . . . . . . . . . . . . 19
 |
61 | | elmapg 7516 |
. . . . . . . . . . . . . . . . . . 19
             |
62 | 59, 60, 61 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
   
                      |
63 | 58, 62 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
   
           
    |
64 | | oveq2 6328 |
. . . . . . . . . . . . . . . . . . 19
       |
65 | 64 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . 18
   

    |
66 | 65 | rspcev 3162 |
. . . . . . . . . . . . . . . . 17
 
   
    |
67 | 51, 63, 66 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
   
            
    |
68 | 67, 13 | sylibr 217 |
. . . . . . . . . . . . . . 15
   
           
     |
69 | | f1ofo 5848 |
. . . . . . . . . . . . . . . . . 18
    
      |
70 | 69 | ad2antll 740 |
. . . . . . . . . . . . . . . . 17
   
                  |
71 | | forn 5823 |
. . . . . . . . . . . . . . . . 17
       |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
   
              |
73 | 72 | eqcomd 2468 |
. . . . . . . . . . . . . . 15
   
              |
74 | 68, 73 | jca 539 |
. . . . . . . . . . . . . 14
   
             
 
   |
75 | 74 | expr 624 |
. . . . . . . . . . . . 13
   
            
 
    |
76 | 75 | eximdv 1775 |
. . . . . . . . . . . 12
   
       
              |
77 | 50, 76 | syl5 33 |
. . . . . . . . . . 11
   
      
    

    |
78 | 77 | rexlimdva 2891 |
. . . . . . . . . 10
   
                |
79 | 47, 78 | mpd 15 |
. . . . . . . . 9
   
             |
80 | 79 | ex 440 |
. . . . . . . 8
                 |
81 | | vex 3060 |
. . . . . . . . . 10
 |
82 | 37 | elrnmpt 5103 |
. . . . . . . . . 10
       
      |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . 9
      
     |
84 | | df-rex 2755 |
. . . . . . . . 9
    
   
 
   |
85 | 83, 84 | bitri 257 |
. . . . . . . 8
               |
86 | 80, 85 | syl6ibr 235 |
. . . . . . 7
       
       |
87 | 86 | ssrdv 3450 |
. . . . . 6
     
       |
88 | 42, 87 | eqssd 3461 |
. . . . 5
    
        |
89 | | df-fo 5611 |
. . . . 5
                  
   
   
         |
90 | 40, 88, 89 | sylanbrc 675 |
. . . 4
    
     
         |
91 | | fodomnum 8519 |
. . . 4
 
 
                    
    |
92 | 12, 90, 91 | sylc 62 |
. . 3
       
   |
93 | | domtr 7653 |
. . 3
      

         |
94 | 92, 10, 93 | syl2anc 671 |
. 2
        |
95 | | pwexg 4604 |
. . . . 5
    |
96 | 95 | adantr 471 |
. . . 4
   
  |
97 | | inex1g 4562 |
. . . 4
    
  |
98 | 96, 97 | syl 17 |
. . 3
        |
99 | | infpwfidom 8490 |
. . 3
   
     |
100 | 98, 99 | syl 17 |
. 2
        |
101 | | sbth 7723 |
. 2
          
   |
102 | 94, 100, 101 | syl2anc 671 |
1
        |