Step | Hyp | Ref
| Expression |
1 | | iundomg.2 |
. . 3
  
 AC   |
2 | | iundomg.3 |
. . . . 5
    |
3 | | brdomi 7598 |
. . . . . . . . 9

       |
4 | 3 | adantl 473 |
. . . . . . . 8
   
      |
5 | | f1f 5792 |
. . . . . . . . . . . 12
           |
6 | | reldom 7593 |
. . . . . . . . . . . . . . 15
 |
7 | 6 | brrelex2i 4881 |
. . . . . . . . . . . . . 14

  |
8 | 6 | brrelexi 4880 |
. . . . . . . . . . . . . 14

  |
9 | 7, 8 | elmapd 7504 |
. . . . . . . . . . . . 13

          |
10 | 9 | adantl 473 |
. . . . . . . . . . . 12
             |
11 | 5, 10 | syl5ibr 229 |
. . . . . . . . . . 11
             |
12 | | ssiun2 4312 |
. . . . . . . . . . . . 13
        |
13 | 12 | adantr 472 |
. . . . . . . . . . . 12
    
     |
14 | 13 | sseld 3417 |
. . . . . . . . . . 11
      
     |
15 | 11, 14 | syld 44 |
. . . . . . . . . 10
        
     |
16 | 15 | ancrd 563 |
. . . . . . . . 9
          
         |
17 | 16 | eximdv 1772 |
. . . . . . . 8
             
         |
18 | 4, 17 | mpd 15 |
. . . . . . 7
       
        |
19 | | df-rex 2762 |
. . . . . . 7
 
      
             |
20 | 18, 19 | sylibr 217 |
. . . . . 6
   
         |
21 | 20 | ralimiaa 2795 |
. . . . 5
 
 
         |
22 | 2, 21 | syl 17 |
. . . 4
  
         |
23 | | nfv 1769 |
. . . . 5
  
        |
24 | | nfiu1 4299 |
. . . . . 6
  

  |
25 | | nfcv 2612 |
. . . . . . 7
   |
26 | | nfcsb1v 3365 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)  |
27 | | nfcv 2612 |
. . . . . . 7
   |
28 | 25, 26, 27 | nff1 5790 |
. . . . . 6
     ![]_ ]_](_urbrack.gif)    |
29 | 24, 28 | nfrex 2848 |
. . . . 5
  
       ![]_ ]_](_urbrack.gif)    |
30 | | csbeq1a 3358 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   |
31 | | f1eq2 5788 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)      |
32 | 30, 31 | syl 17 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)      |
33 | 32 | rexbidv 2892 |
. . . . 5
  
      

       ![]_ ]_](_urbrack.gif)      |
34 | 23, 29, 33 | cbvral 3001 |
. . . 4
 

      
 
       ![]_ ]_](_urbrack.gif)     |
35 | 22, 34 | sylib 201 |
. . 3
  
       ![]_ ]_](_urbrack.gif)     |
36 | | f1eq1 5787 |
. . . 4
          ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)      |
37 | 36 | acni3 8496 |
. . 3
   
 AC

 
      ![]_ ]_](_urbrack.gif)   
                   ![]_ ]_](_urbrack.gif)      |
38 | 1, 35, 37 | syl2anc 673 |
. 2
        
  
        ![]_ ]_](_urbrack.gif)      |
39 | | nfv 1769 |
. . . . . 6
           |
40 | | nfcv 2612 |
. . . . . . 7
       |
41 | 40, 26, 27 | nff1 5790 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)    |
42 | | fveq2 5879 |
. . . . . . . 8
           |
43 | | f1eq1 5787 |
. . . . . . . 8
                             |
44 | 42, 43 | syl 17 |
. . . . . . 7
                     |
45 | | f1eq2 5788 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)      |
46 | 30, 45 | syl 17 |
. . . . . . 7
                  ![]_ ]_](_urbrack.gif)      |
47 | 44, 46 | bitrd 261 |
. . . . . 6
                  ![]_ ]_](_urbrack.gif)      |
48 | 39, 41, 47 | cbvral 3001 |
. . . . 5
 
       
         ![]_ ]_](_urbrack.gif)     |
49 | | df-ne 2643 |
. . . . . . . 8

  |
50 | | acnrcl 8491 |
. . . . . . . . . 10
 
  AC   |
51 | 1, 50 | syl 17 |
. . . . . . . . 9
   |
52 | | r19.2z 3849 |
. . . . . . . . . . . 12
  
 
  |
53 | 7 | rexlimivw 2869 |
. . . . . . . . . . . 12
    |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
  
   |
55 | 54 | expcom 442 |
. . . . . . . . . 10
 
    |
56 | 2, 55 | syl 17 |
. . . . . . . . 9
     |
57 | | xpexg 6612 |
. . . . . . . . 9
 
     |
58 | 51, 56, 57 | syl6an 554 |
. . . . . . . 8
       |
59 | 49, 58 | syl5bir 226 |
. . . . . . 7
       |
60 | | xpeq1 4853 |
. . . . . . . 8

  
   |
61 | | 0xp 4920 |
. . . . . . . . 9
   |
62 | | 0ex 4528 |
. . . . . . . . 9
 |
63 | 61, 62 | eqeltri 2545 |
. . . . . . . 8
   |
64 | 60, 63 | syl6eqel 2557 |
. . . . . . 7

    |
65 | 59, 64 | pm2.61d2 165 |
. . . . . 6
     |
66 | | iunfo.1 |
. . . . . . . . . 10
      |
67 | 66 | eleq2i 2541 |
. . . . . . . . 9

       |
68 | | eliun 4274 |
. . . . . . . . 9
     

      |
69 | 67, 68 | bitri 257 |
. . . . . . . 8


      |
70 | | r19.29 2912 |
. . . . . . . . . 10
           
     
        
       |
71 | | xp1st 6842 |
. . . . . . . . . . . . . . 15
             |
72 | 71 | ad2antll 743 |
. . . . . . . . . . . . . 14
                         |
73 | | elsni 3985 |
. . . . . . . . . . . . . 14
             |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
                       |
75 | | simpl 464 |
. . . . . . . . . . . . 13
                   |
76 | 74, 75 | eqeltrd 2549 |
. . . . . . . . . . . 12
                       |
77 | 74 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                               |
78 | 77 | fveq1d 5881 |
. . . . . . . . . . . . 13
                                               |
79 | | f1f 5792 |
. . . . . . . . . . . . . . 15
                   |
80 | 79 | ad2antrl 742 |
. . . . . . . . . . . . . 14
                           |
81 | | xp2nd 6843 |
. . . . . . . . . . . . . . 15
           |
82 | 81 | ad2antll 743 |
. . . . . . . . . . . . . 14
                       |
83 | 80, 82 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
                               |
84 | 78, 83 | eqeltrd 2549 |
. . . . . . . . . . . 12
                                   |
85 | | opelxpi 4871 |
. . . . . . . . . . . 12
                                                  |
86 | 76, 84, 85 | syl2anc 673 |
. . . . . . . . . . 11
                                       
    |
87 | 86 | rexlimiva 2868 |
. . . . . . . . . 10
          
                           
    |
88 | 70, 87 | syl 17 |
. . . . . . . . 9
           
                                |
89 | 88 | ex 441 |
. . . . . . . 8
 
       
                            
     |
90 | 69, 89 | syl5bi 225 |
. . . . . . 7
 
       
                             |
91 | | fvex 5889 |
. . . . . . . . . 10
     |
92 | | fvex 5889 |
. . . . . . . . . 10
                 |
93 | 91, 92 | opth 4676 |
. . . . . . . . 9
                       
                                                                   |
94 | | simpr 468 |
. . . . . . . . . . . . . . 15
                                  |
95 | 94 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                                          |
96 | 95 | fveq1d 5881 |
. . . . . . . . . . . . 13
                                                          |
97 | 96 | eqeq2d 2481 |
. . . . . . . . . . . 12
                                                        
                                   |
98 | | djussxp 4985 |
. . . . . . . . . . . . . . . . . 18

   
   |
99 | 66, 98 | eqsstri 3448 |
. . . . . . . . . . . . . . . . 17

  |
100 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
           
    |
101 | 99, 100 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
           
      |
102 | 101 | adantr 472 |
. . . . . . . . . . . . . . 15
                            |
103 | | xp1st 6842 |
. . . . . . . . . . . . . . 15
  
      |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . 14
                              |
105 | | simpll 768 |
. . . . . . . . . . . . . 14
                        
          |
106 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
           |
107 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif)  |
108 | 106, 107,
27 | nff1 5790 |
. . . . . . . . . . . . . . 15
                  ![]_ ]_](_urbrack.gif)    |
109 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
    
              |
110 | | f1eq1 5787 |
. . . . . . . . . . . . . . . . 17
            
        
               |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
    
        
               |
112 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . 17
    
      ![]_ ]_](_urbrack.gif)   |
113 | | f1eq2 5788 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)
            
                ![]_ ]_](_urbrack.gif)      |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
    
            
                ![]_ ]_](_urbrack.gif)      |
115 | 111, 114 | bitrd 261 |
. . . . . . . . . . . . . . 15
    
        
                ![]_ ]_](_urbrack.gif)      |
116 | 108, 115 | rspc 3130 |
. . . . . . . . . . . . . 14
      
                        ![]_ ]_](_urbrack.gif)      |
117 | 104, 105,
116 | sylc 61 |
. . . . . . . . . . . . 13
                                        ![]_ ]_](_urbrack.gif)     |
118 | 107 | nfel2 2628 |
. . . . . . . . . . . . . . . . . . . 20
            ![]_ ]_](_urbrack.gif)  |
119 | 74 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
120 | 119, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                       ![]_ ]_](_urbrack.gif)   |
121 | 82, 120 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . . . 21
                           ![]_ ]_](_urbrack.gif)   |
122 | 121 | ex 441 |
. . . . . . . . . . . . . . . . . . . 20
                          ![]_ ]_](_urbrack.gif)    |
123 | 118, 122 | rexlimi 2864 |
. . . . . . . . . . . . . . . . . . 19
          
               ![]_ ]_](_urbrack.gif)   |
124 | 70, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
           
               ![]_ ]_](_urbrack.gif)   |
125 | 124 | ex 441 |
. . . . . . . . . . . . . . . . 17
 
       
                ![]_ ]_](_urbrack.gif)    |
126 | 69, 125 | syl5bi 225 |
. . . . . . . . . . . . . . . 16
 
       
           ![]_ ]_](_urbrack.gif)    |
127 | 126 | imp 436 |
. . . . . . . . . . . . . . 15
          

          ![]_ ]_](_urbrack.gif)   |
128 | 127 | adantrr 731 |
. . . . . . . . . . . . . 14
           
            ![]_ ]_](_urbrack.gif)   |
129 | 128 | adantr 472 |
. . . . . . . . . . . . 13
                                  ![]_ ]_](_urbrack.gif)   |
130 | 126 | ralrimiv 2808 |
. . . . . . . . . . . . . . . . 17
 
       

          ![]_ ]_](_urbrack.gif)   |
131 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
132 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
133 | 132 | csbeq1d 3356 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
134 | 131, 133 | eleq12d 2543 |
. . . . . . . . . . . . . . . . . 18
            ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)    |
135 | 134 | rspccva 3135 |
. . . . . . . . . . . . . . . . 17
             ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)   |
136 | 130, 135 | sylan 479 |
. . . . . . . . . . . . . . . 16
          

          ![]_ ]_](_urbrack.gif)   |
137 | 136 | adantrl 730 |
. . . . . . . . . . . . . . 15
           
            ![]_ ]_](_urbrack.gif)   |
138 | 137 | adantr 472 |
. . . . . . . . . . . . . 14
                                  ![]_ ]_](_urbrack.gif)   |
139 | 94 | csbeq1d 3356 |
. . . . . . . . . . . . . 14
                              ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
140 | 138, 139 | eleqtrrd 2552 |
. . . . . . . . . . . . 13
                                  ![]_ ]_](_urbrack.gif)   |
141 | | f1fveq 6181 |
. . . . . . . . . . . . 13
                  ![]_ ]_](_urbrack.gif)  
           ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)                                               |
142 | 117, 129,
140, 141 | syl12anc 1290 |
. . . . . . . . . . . 12
                                                        
           |
143 | 97, 142 | bitr3d 263 |
. . . . . . . . . . 11
                                                        
           |
144 | 143 | pm5.32da 653 |
. . . . . . . . . 10
           
                                            
        
            |
145 | | simprr 774 |
. . . . . . . . . . . 12
           
    |
146 | 99, 145 | sseldi 3416 |
. . . . . . . . . . 11
           
      |
147 | | xpopth 6851 |
. . . . . . . . . . 11
   
                     
   |
148 | 101, 146,
147 | syl2anc 673 |
. . . . . . . . . 10
           
                    
   |
149 | 144, 148 | bitrd 261 |
. . . . . . . . 9
           
                                            
   |
150 | 93, 149 | syl5bb 265 |
. . . . . . . 8
           
                         
                          |
151 | 150 | ex 441 |
. . . . . . 7
 
       
 
                        
                           |
152 | 90, 151 | dom2d 7628 |
. . . . . 6
 
       
   
    |
153 | 65, 152 | syl5com 30 |
. . . . 5
                |
154 | 48, 153 | syl5bir 226 |
. . . 4
           ![]_ ]_](_urbrack.gif)        |
155 | 154 | adantld 474 |
. . 3
        
          ![]_ ]_](_urbrack.gif)   
     |
156 | 155 | exlimdv 1787 |
. 2
         
  
        ![]_ ]_](_urbrack.gif)         |
157 | 38, 156 | mpd 15 |
1
     |