Step | Hyp | Ref
| Expression |
1 | | foima 5825 |
. . 3
           |
2 | 1 | adantl 472 |
. 2
             |
3 | | fofn 5822 |
. . . 4
    
  |
4 | | imaeq2 5186 |
. . . . . . . 8

          |
5 | | ima0 5205 |
. . . . . . . 8
     |
6 | 4, 5 | syl6eq 2512 |
. . . . . . 7

      |
7 | | id 22 |
. . . . . . 7

  |
8 | 6, 7 | breq12d 4431 |
. . . . . 6

        |
9 | 8 | imbi2d 322 |
. . . . 5

      

    |
10 | | imaeq2 5186 |
. . . . . . 7
           |
11 | | id 22 |
. . . . . . 7
   |
12 | 10, 11 | breq12d 4431 |
. . . . . 6
     
       |
13 | 12 | imbi2d 322 |
. . . . 5
       

        |
14 | | imaeq2 5186 |
. . . . . . 7
                   |
15 | | id 22 |
. . . . . . 7
           |
16 | 14, 15 | breq12d 4431 |
. . . . . 6
                         |
17 | 16 | imbi2d 322 |
. . . . 5
                             |
18 | | imaeq2 5186 |
. . . . . . 7
           |
19 | | id 22 |
. . . . . . 7
   |
20 | 18, 19 | breq12d 4431 |
. . . . . 6
     
       |
21 | 20 | imbi2d 322 |
. . . . 5
       

        |
22 | | 0ex 4551 |
. . . . . . 7
 |
23 | 22 | 0dom 7733 |
. . . . . 6
 |
24 | 23 | a1i 11 |
. . . . 5
   |
25 | | fnfun 5699 |
. . . . . . . . . . . . . . 15
   |
26 | 25 | ad2antrl 739 |
. . . . . . . . . . . . . 14
             |
27 | | funressn 6106 |
. . . . . . . . . . . . . 14

               |
28 | | rnss 5085 |
. . . . . . . . . . . . . 14
 
                           |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . . 13
           
              |
30 | | df-ima 4869 |
. . . . . . . . . . . . 13
           |
31 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
32 | 31 | rnsnop 5340 |
. . . . . . . . . . . . . 14
        
       |
33 | 32 | eqcomi 2471 |
. . . . . . . . . . . . 13
                |
34 | 29, 30, 33 | 3sstr4g 3485 |
. . . . . . . . . . . 12
                
        |
35 | | snex 4658 |
. . . . . . . . . . . 12
       |
36 | | ssexg 4565 |
. . . . . . . . . . . 12
                             |
37 | 34, 35, 36 | sylancl 673 |
. . . . . . . . . . 11
                   |
38 | | fvi 5950 |
. . . . . . . . . . 11
                       |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
                           |
40 | 39 | uneq2d 3600 |
. . . . . . . . 9
                                       |
41 | | imaundi 5270 |
. . . . . . . . 9
                     |
42 | 40, 41 | syl6eqr 2514 |
. . . . . . . 8
                                   |
43 | | simprr 771 |
. . . . . . . . 9
                 |
44 | | ssdomg 7646 |
. . . . . . . . . . . 12
                                   |
45 | 35, 34, 44 | mpsyl 65 |
. . . . . . . . . . 11
                         |
46 | | fvex 5902 |
. . . . . . . . . . . . 13
     |
47 | 46 | ensn1 7664 |
. . . . . . . . . . . 12
       |
48 | 31 | ensn1 7664 |
. . . . . . . . . . . 12
   |
49 | 47, 48 | entr4i 7657 |
. . . . . . . . . . 11
         |
50 | | domentr 7659 |
. . . . . . . . . . 11
                                 |
51 | 45, 49, 50 | sylancl 673 |
. . . . . . . . . 10
                     |
52 | 39, 51 | eqbrtrd 4439 |
. . . . . . . . 9
                       |
53 | | simplr 767 |
. . . . . . . . . 10
          
  |
54 | | disjsn 4044 |
. . . . . . . . . 10
    
  |
55 | 53, 54 | sylibr 217 |
. . . . . . . . 9
           
     |
56 | | undom 7691 |
. . . . . . . . 9
      
           
                        |
57 | 43, 52, 55, 56 | syl21anc 1275 |
. . . . . . . 8
                               |
58 | 42, 57 | eqbrtrrd 4441 |
. . . . . . 7
                         |
59 | 58 | exp32 614 |
. . . . . 6
 


    
                |
60 | 59 | a2d 29 |
. . . . 5
 

 
     
                |
61 | 9, 13, 17, 21, 24, 60 | findcard2s 7843 |
. . . 4
 
       |
62 | 3, 61 | syl5 33 |
. . 3
             |
63 | 62 | imp 435 |
. 2
             |
64 | 2, 63 | eqbrtrrd 4441 |
1
         |