Step | Hyp | Ref
| Expression |
1 | | elex 3054 |
. 2
   |
2 | | 0wdom 8085 |
. . . . . 6
 *   |
3 | | breq1 4405 |
. . . . . 6

 * *    |
4 | 2, 3 | syl5ibrcom 226 |
. . . . 5
 
*    |
5 | 4 | imp 431 |
. . . 4
 
 *   |
6 | | 0elpw 4572 |
. . . . . . 7
  |
7 | | f1o0 5849 |
. . . . . . . 8
     |
8 | | f1ofo 5821 |
. . . . . . . 8
           |
9 | | 0ex 4535 |
. . . . . . . . 9
 |
10 | | foeq1 5789 |
. . . . . . . . 9

            |
11 | 9, 10 | spcev 3141 |
. . . . . . . 8
    
       |
12 | 7, 8, 11 | mp2b 10 |
. . . . . . 7
      |
13 | | foeq2 5790 |
. . . . . . . . 9

    
       |
14 | 13 | exbidv 1768 |
. . . . . . . 8

              |
15 | 14 | rspcev 3150 |
. . . . . . 7
 
                |
16 | 6, 12, 15 | mp2an 678 |
. . . . . 6
        |
17 | | foeq3 5791 |
. . . . . . . 8

    
       |
18 | 17 | exbidv 1768 |
. . . . . . 7

              |
19 | 18 | rexbidv 2901 |
. . . . . 6

   
   
          |
20 | 16, 19 | mpbiri 237 |
. . . . 5

         |
21 | 20 | adantl 468 |
. . . 4
 
 
        |
22 | 5, 21 | 2thd 244 |
. . 3
 
  *           |
23 | | brwdomn0 8084 |
. . . . 5

 * 
       |
24 | 23 | adantl 468 |
. . . 4
    *         |
25 | | foeq1 5789 |
. . . . . . 7
             |
26 | 25 | cbvexv 2117 |
. . . . . 6
             |
27 | | pwidg 3964 |
. . . . . . . . 9
    |
28 | 27 | ad2antrr 732 |
. . . . . . . 8
             |
29 | | foeq2 5790 |
. . . . . . . . . 10
             |
30 | 29 | exbidv 1768 |
. . . . . . . . 9
  
   
        |
31 | 30 | rspcev 3150 |
. . . . . . . 8
                  |
32 | 28, 31 | sylancom 673 |
. . . . . . 7
                   |
33 | 32 | ex 436 |
. . . . . 6
    
   
          |
34 | 26, 33 | syl5bi 221 |
. . . . 5
    
   
          |
35 | | n0 3741 |
. . . . . . . . . . 11
    |
36 | 35 | biimpi 198 |
. . . . . . . . . 10


  |
37 | 36 | ad2antlr 733 |
. . . . . . . . 9
            
  |
38 | | vex 3048 |
. . . . . . . . . . . . 13
 |
39 | | difexg 4551 |
. . . . . . . . . . . . . 14
     |
40 | | snex 4641 |
. . . . . . . . . . . . . 14
 
 |
41 | | xpexg 6593 |
. . . . . . . . . . . . . 14
               |
42 | 39, 40, 41 | sylancl 668 |
. . . . . . . . . . . . 13
         |
43 | | unexg 6592 |
. . . . . . . . . . . . 13
                   |
44 | 38, 42, 43 | sylancr 669 |
. . . . . . . . . . . 12
           |
45 | 44 | adantr 467 |
. . . . . . . . . . 11
             |
46 | 45 | ad2antrr 732 |
. . . . . . . . . 10
   
                    |
47 | | fofn 5795 |
. . . . . . . . . . . . . . 15
       |
48 | 47 | adantl 468 |
. . . . . . . . . . . . . 14
       
  |
49 | 48 | ad2antlr 733 |
. . . . . . . . . . . . 13
   
            |
50 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
51 | | fnconstg 5771 |
. . . . . . . . . . . . . 14
           |
52 | 50, 51 | mp1i 13 |
. . . . . . . . . . . . 13
   
                    |
53 | | disjdif 3839 |
. . . . . . . . . . . . . 14
     |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
   
          
     |
55 | | fnun 5682 |
. . . . . . . . . . . . 13
            
   
              |
56 | 49, 52, 54, 55 | syl21anc 1267 |
. . . . . . . . . . . 12
   
                        |
57 | | elpwi 3960 |
. . . . . . . . . . . . . . . 16
 
  |
58 | | undif 3848 |
. . . . . . . . . . . . . . . 16

      |
59 | 57, 58 | sylib 200 |
. . . . . . . . . . . . . . 15
        |
60 | 59 | ad2antrl 734 |
. . . . . . . . . . . . . 14
                  |
61 | 60 | adantr 467 |
. . . . . . . . . . . . 13
   
                |
62 | 61 | fneq2d 5667 |
. . . . . . . . . . . 12
   
                                  |
63 | 56, 62 | mpbid 214 |
. . . . . . . . . . 11
   
                    |
64 | | rnun 5244 |
. . . . . . . . . . . 12
                 |
65 | | forn 5796 |
. . . . . . . . . . . . . . . 16
    
  |
66 | 65 | ad2antll 735 |
. . . . . . . . . . . . . . 15
           
  |
67 | 66 | adantr 467 |
. . . . . . . . . . . . . 14
   
         
  |
68 | 67 | uneq1d 3587 |
. . . . . . . . . . . . 13
   
          
                 |
69 | | fconst6g 5772 |
. . . . . . . . . . . . . . . 16
               |
70 | | frn 5735 |
. . . . . . . . . . . . . . . 16
            
     
  |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
         |
72 | 71 | adantl 468 |
. . . . . . . . . . . . . 14
   
                  |
73 | | ssequn2 3607 |
. . . . . . . . . . . . . 14
                 |
74 | 72, 73 | sylib 200 |
. . . . . . . . . . . . 13
   
          
         |
75 | 68, 74 | eqtrd 2485 |
. . . . . . . . . . . 12
   
          
         |
76 | 64, 75 | syl5eq 2497 |
. . . . . . . . . . 11
   
                    |
77 | | df-fo 5588 |
. . . . . . . . . . 11
                                 |
78 | 63, 76, 77 | sylanbrc 670 |
. . . . . . . . . 10
   
                        |
79 | | foeq1 5789 |
. . . . . . . . . . 11
             
               |
80 | 79 | spcegv 3135 |
. . . . . . . . . 10
                      
       |
81 | 46, 78, 80 | sylc 62 |
. . . . . . . . 9
   
                 |
82 | 37, 81 | exlimddv 1781 |
. . . . . . . 8
            
      |
83 | 82 | expr 620 |
. . . . . . 7
   
 
     
       |
84 | 83 | exlimdv 1779 |
. . . . . 6
   
 
     
        |
85 | 84 | rexlimdva 2879 |
. . . . 5
    
     
        |
86 | 34, 85 | impbid 194 |
. . . 4
    
   
          |
87 | 24, 86 | bitrd 257 |
. . 3
    *           |
88 | 22, 87 | pm2.61dane 2711 |
. 2
  *           |
89 | 1, 88 | syl 17 |
1
  *           |