Step | Hyp | Ref
| Expression |
1 | | fssxp 5671 |
. . 3
         |
2 | | ffun 5662 |
. . . . . . . . 9
       |
3 | 2 | adantr 465 |
. . . . . . . 8
     
   |
4 | | fdm 5664 |
. . . . . . . . . 10
       |
5 | 4 | eleq2d 2521 |
. . . . . . . . 9
         |
6 | 5 | biimpar 485 |
. . . . . . . 8
     
   |
7 | | funfvop 5917 |
. . . . . . . 8
            |
8 | 3, 6, 7 | syl2anc 661 |
. . . . . . 7
     
          |
9 | | df-br 4394 |
. . . . . . 7
      
         |
10 | 8, 9 | sylibr 212 |
. . . . . 6
     
         |
11 | | fvex 5802 |
. . . . . . 7
     |
12 | | breq2 4397 |
. . . . . . 7
       
         |
13 | 11, 12 | spcev 3163 |
. . . . . 6
            |
14 | 10, 13 | syl 16 |
. . . . 5
     
      |
15 | | funmo 5535 |
. . . . . . 7

     |
16 | 2, 15 | syl 16 |
. . . . . 6
     
    |
17 | 16 | adantr 465 |
. . . . 5
     
      |
18 | | eu5 2290 |
. . . . 5
              |
19 | 14, 17, 18 | sylanbrc 664 |
. . . 4
     
      |
20 | 19 | ralrimiva 2825 |
. . 3
     

    |
21 | 1, 20 | jca 532 |
. 2
               |
22 | | xpss 5047 |
. . . . . . . 8
  
  |
23 | | sstr 3465 |
. . . . . . . 8
 
    
 
    |
24 | 22, 23 | mpan2 671 |
. . . . . . 7
       |
25 | | df-rel 4948 |
. . . . . . 7

    |
26 | 24, 25 | sylibr 212 |
. . . . . 6
     |
27 | 26 | adantr 465 |
. . . . 5
 
  
   
  |
28 | | df-ral 2800 |
. . . . . . 7
 
  
         |
29 | | eumo 2293 |
. . . . . . . . . . . 12
         |
30 | 29 | imim2i 14 |
. . . . . . . . . . 11
  
    
     |
31 | 30 | adantl 466 |
. . . . . . . . . 10
 
   
           |
32 | | df-br 4394 |
. . . . . . . . . . . . . . . 16
  
  
  |
33 | | ssel 3451 |
. . . . . . . . . . . . . . . 16
      
        |
34 | 32, 33 | syl5bi 217 |
. . . . . . . . . . . . . . 15
              |
35 | | opelxp1 4973 |
. . . . . . . . . . . . . . 15
     
  |
36 | 34, 35 | syl6 33 |
. . . . . . . . . . . . . 14
     
   |
37 | 36 | exlimdv 1691 |
. . . . . . . . . . . . 13
    
 
   |
38 | 37 | con3d 133 |
. . . . . . . . . . . 12
   
      |
39 | | exmo 2289 |
. . . . . . . . . . . . 13
         |
40 | 39 | ori 375 |
. . . . . . . . . . . 12
   
     |
41 | 38, 40 | syl6 33 |
. . . . . . . . . . 11
   
      |
42 | 41 | adantr 465 |
. . . . . . . . . 10
 
   
    
      |
43 | 31, 42 | pm2.61d 158 |
. . . . . . . . 9
 
   
    
    |
44 | 43 | ex 434 |
. . . . . . . 8
               |
45 | 44 | alimdv 1676 |
. . . . . . 7
      
            |
46 | 28, 45 | syl5bi 217 |
. . . . . 6
    

 
  
     |
47 | 46 | imp 429 |
. . . . 5
 
  
           |
48 | | dffun6 5534 |
. . . . 5
          |
49 | 27, 47, 48 | sylanbrc 664 |
. . . 4
 
  
   
  |
50 | | dmss 5140 |
. . . . . . 7
  
    |
51 | | dmxpss 5370 |
. . . . . . 7
   |
52 | 50, 51 | syl6ss 3469 |
. . . . . 6
     |
53 | | breq1 4396 |
. . . . . . . . . 10
   
     |
54 | 53 | eubidv 2283 |
. . . . . . . . 9
  
        |
55 | 54 | rspccv 3169 |
. . . . . . . 8
 
          |
56 | | euex 2288 |
. . . . . . . . 9
         |
57 | | vex 3074 |
. . . . . . . . . 10
 |
58 | 57 | eldm 5138 |
. . . . . . . . 9

     |
59 | 56, 58 | sylibr 212 |
. . . . . . . 8
      |
60 | 55, 59 | syl6 33 |
. . . . . . 7
 
       |
61 | 60 | ssrdv 3463 |
. . . . . 6
 
     |
62 | 52, 61 | anim12i 566 |
. . . . 5
 
  
        |
63 | | eqss 3472 |
. . . . 5

    |
64 | 62, 63 | sylibr 212 |
. . . 4
 
  
   
  |
65 | | df-fn 5522 |
. . . 4

    |
66 | 49, 64, 65 | sylanbrc 664 |
. . 3
 
  
      |
67 | | rnss 5169 |
. . . . 5
  
    |
68 | | rnxpss 5371 |
. . . . 5
   |
69 | 67, 68 | syl6ss 3469 |
. . . 4
     |
70 | 69 | adantr 465 |
. . 3
 
  
   
  |
71 | | df-f 5523 |
. . 3
    

   |
72 | 66, 70, 71 | sylanbrc 664 |
. 2
 
  
          |
73 | 21, 72 | impbii 188 |
1
    
  

      |