Step | Hyp | Ref
| Expression |
1 | | reldom 7572 |
. . 3
 |
2 | 1 | brrelexi 4874 |
. 2

  |
3 | | elex 3053 |
. . 3
     |
4 | | pwexb 6599 |
. . 3

   |
5 | 3, 4 | sylibr 216 |
. 2
    |
6 | | elex 3053 |
. . . . 5
   |
7 | | snex 4640 |
. . . . . . . 8
 
 |
8 | 7 | 2a1i 12 |
. . . . . . 7
       |
9 | | vex 3047 |
. . . . . . . . . 10
 |
10 | 9 | sneqr 4138 |
. . . . . . . . 9
       |
11 | | sneq 3977 |
. . . . . . . . 9
  
    |
12 | 10, 11 | impbii 191 |
. . . . . . . 8
    
  |
13 | 12 | 2a1i 12 |
. . . . . . 7
  

    
    |
14 | 8, 13 | dom2lem 7606 |
. . . . . 6
           |
15 | | f1f1orn 5823 |
. . . . . 6
        
        
     |
16 | 14, 15 | syl 17 |
. . . . 5
               |
17 | | f1oeng 7585 |
. . . . 5
  
                  |
18 | 6, 16, 17 | syl2anc 666 |
. . . 4
       |
19 | | domen1 7711 |
. . . 4


   
       |
20 | 18, 19 | syl 17 |
. . 3
 
       |
21 | | distop 20004 |
. . . . . . 7
 
  |
22 | | simpr 463 |
. . . . . . . . . 10
 
   |
23 | 9 | snelpw 4645 |
. . . . . . . . . 10

 
   |
24 | 22, 23 | sylib 200 |
. . . . . . . . 9
 
      |
25 | | eqid 2450 |
. . . . . . . . 9
         |
26 | 24, 25 | fmptd 6044 |
. . . . . . . 8
            |
27 | | frn 5733 |
. . . . . . . 8
                 |
28 | 26, 27 | syl 17 |
. . . . . . 7
 
      |
29 | | elpwi 3959 |
. . . . . . . . . . . . 13
 
  |
30 | 29 | ad2antrl 733 |
. . . . . . . . . . . 12
        |
31 | | simprr 765 |
. . . . . . . . . . . 12
        |
32 | 30, 31 | sseldd 3432 |
. . . . . . . . . . 11
        |
33 | | eqidd 2451 |
. . . . . . . . . . 11
            |
34 | | sneq 3977 |
. . . . . . . . . . . . 13
  
    |
35 | 34 | eqeq2d 2460 |
. . . . . . . . . . . 12
     
 
     |
36 | 35 | rspcev 3149 |
. . . . . . . . . . 11
       
      |
37 | 32, 33, 36 | syl2anc 666 |
. . . . . . . . . 10
      
 
    |
38 | | snex 4640 |
. . . . . . . . . . 11
   |
39 | 25 | elrnmpt 5080 |
. . . . . . . . . . 11
         

 
     |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
   
   
      |
41 | 37, 40 | sylibr 216 |
. . . . . . . . 9
              |
42 | | ssnid 3996 |
. . . . . . . . . 10
   |
43 | 42 | a1i 11 |
. . . . . . . . 9
          |
44 | 31 | snssd 4116 |
. . . . . . . . 9
       
  |
45 | | eleq2 2517 |
. . . . . . . . . . 11
         |
46 | | sseq1 3452 |
. . . . . . . . . . 11
         |
47 | 45, 46 | anbi12d 716 |
. . . . . . . . . 10
     
         |
48 | 47 | rspcev 3149 |
. . . . . . . . 9
                         |
49 | 41, 43, 44, 48 | syl12anc 1265 |
. . . . . . . 8
                |
50 | 49 | ralrimivva 2808 |
. . . . . . 7
   
          |
51 | | basgen2 19998 |
. . . . . . 7
      
     
    
 
           |
52 | 21, 28, 50, 51 | syl3anc 1267 |
. . . . . 6
   

       |
53 | 52 | adantr 467 |
. . . . 5
         

       |
54 | 52, 21 | eqeltrd 2528 |
. . . . . . 7
   

      |
55 | | tgclb 19979 |
. . . . . . 7
               |
56 | 54, 55 | sylibr 216 |
. . . . . 6
 
     |
57 | | 2ndci 20456 |
. . . . . 6
      
      

      |
58 | 56, 57 | sylan 474 |
. . . . 5
         

      |
59 | 53, 58 | eqeltrrd 2529 |
. . . 4
       
  |
60 | | is2ndc 20454 |
. . . . . 6
 
          |
61 | | vex 3047 |
. . . . . . . . . 10
 |
62 | | simpr 463 |
. . . . . . . . . . . . . . . 16
   
            |
63 | 62, 23 | sylib 200 |
. . . . . . . . . . . . . . 15
   
           
   |
64 | | simplrr 770 |
. . . . . . . . . . . . . . 15
   
                 |
65 | 63, 64 | eleqtrrd 2531 |
. . . . . . . . . . . . . 14
   
           
      |
66 | | ssnid 3996 |
. . . . . . . . . . . . . 14
   |
67 | | tg2 19973 |
. . . . . . . . . . . . . 14
       
   

     |
68 | 65, 66, 67 | sylancl 667 |
. . . . . . . . . . . . 13
   
          

     |
69 | | simprrl 773 |
. . . . . . . . . . . . . . . 16
             
       
  |
70 | 69 | snssd 4116 |
. . . . . . . . . . . . . . 15
             
       
    |
71 | | simprrr 774 |
. . . . . . . . . . . . . . 15
             
       
    |
72 | 70, 71 | eqssd 3448 |
. . . . . . . . . . . . . 14
             
       
 
  |
73 | | simprl 763 |
. . . . . . . . . . . . . 14
             
       
  |
74 | 72, 73 | eqeltrd 2528 |
. . . . . . . . . . . . 13
             
       
 
  |
75 | 68, 74 | rexlimddv 2882 |
. . . . . . . . . . . 12
   
           
  |
76 | 75, 25 | fmptd 6044 |
. . . . . . . . . . 11
                      |
77 | | frn 5733 |
. . . . . . . . . . 11
         
     |
78 | 76, 77 | syl 17 |
. . . . . . . . . 10
           

     |
79 | | ssdomg 7612 |
. . . . . . . . . 10
      
      |
80 | 61, 78, 79 | mpsyl 65 |
. . . . . . . . 9
           

     |
81 | | simprl 763 |
. . . . . . . . 9
              |
82 | | domtr 7619 |
. . . . . . . . 9
      
      |
83 | 80, 81, 82 | syl2anc 666 |
. . . . . . . 8
           

     |
84 | 83 | ex 436 |
. . . . . . 7
 
                |
85 | 84 | rexlimdva 2878 |
. . . . . 6
  
       
      |
86 | 60, 85 | syl5bi 221 |
. . . . 5
  
       |
87 | 86 | imp 431 |
. . . 4
  


     |
88 | 59, 87 | impbida 842 |
. . 3
          |
89 | 20, 88 | bitrd 257 |
. 2
 
    |
90 | 2, 5, 89 | pm5.21nii 355 |
1
    |