Step | Hyp | Ref
| Expression |
1 | | tsksdom 9207 |
. . . . . . . . . . . 12
     |
2 | | cardidg 8999 |
. . . . . . . . . . . . . 14
    
  |
3 | 2 | ensymd 7646 |
. . . . . . . . . . . . 13
       |
4 | 3 | adantr 471 |
. . . . . . . . . . . 12
         |
5 | | sdomentr 7732 |
. . . . . . . . . . . 12
 
           |
6 | 1, 4, 5 | syl2anc 671 |
. . . . . . . . . . 11
         |
7 | | eqid 2462 |
. . . . . . . . . . . . . . 15
             |
8 | 7 | rnmpt 5099 |
. . . . . . . . . . . . . 14
              |
9 | | cardon 8404 |
. . . . . . . . . . . . . . . . 17
     |
10 | | sdomdom 7623 |
. . . . . . . . . . . . . . . . 17
    
      |
11 | | ondomen 8494 |
. . . . . . . . . . . . . . . . 17
             |
12 | 9, 10, 11 | sylancr 674 |
. . . . . . . . . . . . . . . 16
    
  |
13 | 12 | adantl 472 |
. . . . . . . . . . . . . . 15
         |
14 | | vex 3060 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | imaexg 6757 |
. . . . . . . . . . . . . . . . . 18
       |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
17 | 16, 7 | fnmpti 5728 |
. . . . . . . . . . . . . . . 16
       |
18 | | dffn4 5822 |
. . . . . . . . . . . . . . . 16
      

                 |
19 | 17, 18 | mpbi 213 |
. . . . . . . . . . . . . . 15
                 |
20 | | fodomnum 8514 |
. . . . . . . . . . . . . . 15
                  
        |
21 | 13, 19, 20 | mpisyl 21 |
. . . . . . . . . . . . . 14
       
       |
22 | 8, 21 | syl5eqbrr 4451 |
. . . . . . . . . . . . 13
                |
23 | | domsdomtr 7733 |
. . . . . . . . . . . . 13
   
                
      |
24 | 22, 23 | sylancom 678 |
. . . . . . . . . . . 12
             
      |
25 | 24 | adantll 725 |
. . . . . . . . . . 11
          
           |
26 | 6, 25 | mpdan 679 |
. . . . . . . . . 10
         
      |
27 | | ne0i 3749 |
. . . . . . . . . . . 12
   |
28 | | tskcard 9232 |
. . . . . . . . . . . 12
         |
29 | 27, 28 | sylan2 481 |
. . . . . . . . . . 11
         |
30 | | elina 9138 |
. . . . . . . . . . . 12
                            
       |
31 | 30 | simp2bi 1030 |
. . . . . . . . . . 11
    
              |
32 | 29, 31 | syl 17 |
. . . . . . . . . 10
                 |
33 | 26, 32 | breqtrrd 4443 |
. . . . . . . . 9
         
          |
34 | 33 | 3adant2 1033 |
. . . . . . . 8
  
 
               |
35 | 34 | adantr 471 |
. . . . . . 7
                    
          |
36 | 29 | 3adant2 1033 |
. . . . . . . . . 10
  
      |
37 | 36 | adantr 471 |
. . . . . . . . 9
                    |
38 | | inawina 9141 |
. . . . . . . . 9
    
       |
39 | | winalim 9146 |
. . . . . . . . 9
            |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . . 8
                    |
41 | | vex 3060 |
. . . . . . . . . . 11
 |
42 | | eqeq1 2466 |
. . . . . . . . . . . 12
     
       |
43 | 42 | rexbidv 2913 |
. . . . . . . . . . 11
  
   

       |
44 | 41, 43 | elab 3197 |
. . . . . . . . . 10
  
     
      |
45 | | imassrn 5198 |
. . . . . . . . . . . . . 14
     |
46 | | f1ofo 5844 |
. . . . . . . . . . . . . . 15
                     |
47 | | forn 5819 |
. . . . . . . . . . . . . . 15
         
      |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . 14
         
      |
49 | 45, 48 | syl5sseq 3492 |
. . . . . . . . . . . . 13
                    |
50 | 49 | ad2antlr 738 |
. . . . . . . . . . . 12
   
           
          |
51 | | f1of1 5836 |
. . . . . . . . . . . . . . . 16
                     |
52 | | elssuni 4241 |
. . . . . . . . . . . . . . . 16
    |
53 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
54 | 53 | f1imaen 7657 |
. . . . . . . . . . . . . . . 16
          
 
      |
55 | 51, 52, 54 | syl2an 484 |
. . . . . . . . . . . . . . 15
          
    
  |
56 | 55 | adantll 725 |
. . . . . . . . . . . . . 14
   
           
      |
57 | | simpl1 1017 |
. . . . . . . . . . . . . . . . 17
       |
58 | | trss 4520 |
. . . . . . . . . . . . . . . . . . . 20


   |
59 | 58 | imp 435 |
. . . . . . . . . . . . . . . . . . 19
     |
60 | 59 | 3adant1 1032 |
. . . . . . . . . . . . . . . . . 18
  
  |
61 | 60 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
       |
62 | | tsksdom 9207 |
. . . . . . . . . . . . . . . . 17
     |
63 | 57, 61, 62 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
       |
64 | 57, 3 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
65 | | sdomentr 7732 |
. . . . . . . . . . . . . . . 16
 
           |
66 | 63, 64, 65 | syl2anc 671 |
. . . . . . . . . . . . . . 15
           |
67 | 66 | adantlr 726 |
. . . . . . . . . . . . . 14
   
           
      |
68 | | ensdomtr 7734 |
. . . . . . . . . . . . . 14
     
               |
69 | 56, 67, 68 | syl2anc 671 |
. . . . . . . . . . . . 13
   
           
          |
70 | 37, 31 | syl 17 |
. . . . . . . . . . . . . 14
                            |
71 | 70 | adantr 471 |
. . . . . . . . . . . . 13
   
           
              |
72 | 69, 71 | breqtrrd 4443 |
. . . . . . . . . . . 12
   
           
              |
73 | | sseq1 3465 |
. . . . . . . . . . . . . 14
     
   
           |
74 | | breq1 4419 |
. . . . . . . . . . . . . 14
                             |
75 | 73, 74 | anbi12d 722 |
. . . . . . . . . . . . 13
                                             |
76 | 75 | biimprcd 233 |
. . . . . . . . . . . 12
     
                
     
                |
77 | 50, 72, 76 | syl2anc 671 |
. . . . . . . . . . 11
   
           
     
                |
78 | 77 | rexlimdva 2891 |
. . . . . . . . . 10
               
                     |
79 | 44, 78 | syl5bi 225 |
. . . . . . . . 9
                     
    
            |
80 | 79 | ralrimiv 2812 |
. . . . . . . 8
                
     
               |
81 | | fvex 5898 |
. . . . . . . . 9
     |
82 | 81 | cfslb2n 8724 |
. . . . . . . 8
     
  
     
                
               
            |
83 | 40, 80, 82 | syl2anc 671 |
. . . . . . 7
                
               
            |
84 | 35, 83 | mpd 15 |
. . . . . 6
                
           |
85 | 16 | dfiun2 4326 |
. . . . . . . 8

      
      |
86 | 49 | ralrimivw 2815 |
. . . . . . . . . 10
          
          |
87 | | iunss 4333 |
. . . . . . . . . 10
 
            
      |
88 | 86, 87 | sylibr 217 |
. . . . . . . . 9
          
          |
89 | | fof 5816 |
. . . . . . . . . . . 12
                     |
90 | | foelrn 6064 |
. . . . . . . . . . . . 13
          
              |
91 | 90 | ex 440 |
. . . . . . . . . . . 12
                         |
92 | | eluni2 4216 |
. . . . . . . . . . . . . . 15
 

  |
93 | | nfv 1772 |
. . . . . . . . . . . . . . . 16
           |
94 | | nfiu1 4322 |
. . . . . . . . . . . . . . . . 17
  
     |
95 | 94 | nfel2 2619 |
. . . . . . . . . . . . . . . 16
      
     |
96 | | ssiun2 4335 |
. . . . . . . . . . . . . . . . . . 19
            |
97 | 96 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . 18
          

           |
98 | | ffn 5751 |
. . . . . . . . . . . . . . . . . . . 20
             |
99 | 98 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . 19
          

   |
100 | 52 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . 19
          

   |
101 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . 19
          

  |
102 | | fnfvima 6168 |
. . . . . . . . . . . . . . . . . . 19
  


          |
103 | 99, 100, 101, 102 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . 18
          

          |
104 | 97, 103 | sseldd 3445 |
. . . . . . . . . . . . . . . . 17
          

    
      |
105 | 104 | 3exp 1214 |
. . . . . . . . . . . . . . . 16
                
        |
106 | 93, 95, 105 | rexlimd 2883 |
. . . . . . . . . . . . . . 15
           
            |
107 | 92, 106 | syl5bi 225 |
. . . . . . . . . . . . . 14
                
       |
108 | | eleq1a 2535 |
. . . . . . . . . . . . . 14
               
       |
109 | 107, 108 | syl6 34 |
. . . . . . . . . . . . 13
                 
        |
110 | 109 | rexlimdv 2889 |
. . . . . . . . . . . 12
           
      
       |
111 | 89, 91, 110 | sylsyld 58 |
. . . . . . . . . . 11
               
       |
112 | 46, 111 | syl 17 |
. . . . . . . . . 10
                       |
113 | 112 | ssrdv 3450 |
. . . . . . . . 9
                     |
114 | 88, 113 | eqssd 3461 |
. . . . . . . 8
          
          |
115 | 85, 114 | syl5eqr 2510 |
. . . . . . 7
            
           |
116 | 115 | necon3ai 2661 |
. . . . . 6
   
                    |
117 | 84, 116 | syl 17 |
. . . . 5
                         |
118 | 117 | pm2.01da 448 |
. . . 4
  
           |
119 | 118 | nexdv 1793 |
. . 3
  
            |
120 | | entr 7647 |
. . . . . . 7
  
     
      |
121 | 3, 120 | sylan2 481 |
. . . . . 6
  
 
      |
122 | | bren 7604 |
. . . . . 6
                  |
123 | 121, 122 | sylib 201 |
. . . . 5
  
 
           |
124 | 123 | expcom 441 |
. . . 4
  
             |
125 | 124 | 3ad2ant1 1035 |
. . 3
  
               |
126 | 119, 125 | mtod 182 |
. 2
  
   |
127 | | uniss 4233 |
. . . . . . . . 9
     |
128 | | df-tr 4512 |
. . . . . . . . . 10
    |
129 | 128 | biimpi 199 |
. . . . . . . . 9

   |
130 | 127, 129 | sylan9ss 3457 |
. . . . . . . 8
 
    |
131 | 130 | expcom 441 |
. . . . . . 7


    |
132 | 58, 131 | syld 45 |
. . . . . 6


    |
133 | 132 | imp 435 |
. . . . 5
      |
134 | | tsken 9205 |
. . . . 5
     
    |
135 | 133, 134 | sylan2 481 |
. . . 4
  
   
    |
136 | 135 | 3impb 1211 |
. . 3
  
  
   |
137 | 136 | ord 383 |
. 2
  
  
   |
138 | 126, 137 | mpd 15 |
1
  
   |