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

       |
4 | 3 | adantl 453 |
. . . . . . . 8
   
      |
5 | | f1f 5602 |
. . . . . . . . . . . 12
           |
6 | | reldom 7078 |
. . . . . . . . . . . . . . 15
 |
7 | 6 | brrelex2i 4882 |
. . . . . . . . . . . . . 14

  |
8 | 6 | brrelexi 4881 |
. . . . . . . . . . . . . 14

  |
9 | | elmapg 6994 |
. . . . . . . . . . . . . 14
 
           |
10 | 7, 8, 9 | syl2anc 643 |
. . . . . . . . . . . . 13

          |
11 | 10 | adantl 453 |
. . . . . . . . . . . 12
             |
12 | 5, 11 | syl5ibr 213 |
. . . . . . . . . . 11
             |
13 | | ssiun2 4098 |
. . . . . . . . . . . . 13
        |
14 | 13 | adantr 452 |
. . . . . . . . . . . 12
    
     |
15 | 14 | sseld 3311 |
. . . . . . . . . . 11
      
     |
16 | 12, 15 | syld 42 |
. . . . . . . . . 10
        
     |
17 | 16 | ancrd 538 |
. . . . . . . . 9
          
         |
18 | 17 | eximdv 1629 |
. . . . . . . 8
             
         |
19 | 4, 18 | mpd 15 |
. . . . . . 7
       
        |
20 | | df-rex 2676 |
. . . . . . 7
 
      
             |
21 | 19, 20 | sylibr 204 |
. . . . . 6
   
         |
22 | 21 | ralimiaa 2744 |
. . . . 5
 
 
         |
23 | 2, 22 | syl 16 |
. . . 4
  
         |
24 | | nfv 1626 |
. . . . 5
  
        |
25 | | nfiu1 4085 |
. . . . . 6
  

  |
26 | | nfcv 2544 |
. . . . . . 7
   |
27 | | nfcsb1v 3247 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)  |
28 | | nfcv 2544 |
. . . . . . 7
   |
29 | 26, 27, 28 | nff1 5600 |
. . . . . 6
     ![]_ ]_](_urbrack.gif)    |
30 | 25, 29 | nfrex 2725 |
. . . . 5
  
       ![]_ ]_](_urbrack.gif)    |
31 | | csbeq1a 3223 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   |
32 | | f1eq2 5598 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)      |
33 | 31, 32 | syl 16 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)      |
34 | 33 | rexbidv 2691 |
. . . . 5
  
      

       ![]_ ]_](_urbrack.gif)      |
35 | 24, 30, 34 | cbvral 2892 |
. . . 4
 

      
 
       ![]_ ]_](_urbrack.gif)     |
36 | 23, 35 | sylib 189 |
. . 3
  
       ![]_ ]_](_urbrack.gif)     |
37 | | f1eq1 5597 |
. . . 4
          ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)      |
38 | 37 | acni3 7888 |
. . 3
   
 AC

 
      ![]_ ]_](_urbrack.gif)   
                   ![]_ ]_](_urbrack.gif)      |
39 | 1, 36, 38 | syl2anc 643 |
. 2
        
  
        ![]_ ]_](_urbrack.gif)      |
40 | | nfv 1626 |
. . . . . 6
           |
41 | | nfcv 2544 |
. . . . . . 7
       |
42 | 41, 27, 28 | nff1 5600 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)    |
43 | | fveq2 5691 |
. . . . . . . 8
           |
44 | | f1eq1 5597 |
. . . . . . . 8
                             |
45 | 43, 44 | syl 16 |
. . . . . . 7
                     |
46 | | f1eq2 5598 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)      |
47 | 31, 46 | syl 16 |
. . . . . . 7
                  ![]_ ]_](_urbrack.gif)      |
48 | 45, 47 | bitrd 245 |
. . . . . 6
                  ![]_ ]_](_urbrack.gif)      |
49 | 40, 42, 48 | cbvral 2892 |
. . . . 5
 
       
         ![]_ ]_](_urbrack.gif)     |
50 | | df-ne 2573 |
. . . . . . . 8

  |
51 | | acnrcl 7883 |
. . . . . . . . . 10
 
  AC   |
52 | 1, 51 | syl 16 |
. . . . . . . . 9
   |
53 | | r19.2z 3681 |
. . . . . . . . . . . 12
  
 
  |
54 | 7 | rexlimivw 2790 |
. . . . . . . . . . . 12
    |
55 | 53, 54 | syl 16 |
. . . . . . . . . . 11
  
   |
56 | 55 | expcom 425 |
. . . . . . . . . 10
 
    |
57 | 2, 56 | syl 16 |
. . . . . . . . 9
     |
58 | | xpexg 4952 |
. . . . . . . . 9
 
     |
59 | 52, 57, 58 | ee12an 1369 |
. . . . . . . 8
       |
60 | 50, 59 | syl5bir 210 |
. . . . . . 7
       |
61 | | xpeq1 4855 |
. . . . . . . 8

  
   |
62 | | xp0r 4919 |
. . . . . . . . 9
   |
63 | | 0ex 4303 |
. . . . . . . . 9
 |
64 | 62, 63 | eqeltri 2478 |
. . . . . . . 8
   |
65 | 61, 64 | syl6eqel 2496 |
. . . . . . 7

    |
66 | 60, 65 | pm2.61d2 154 |
. . . . . 6
     |
67 | | iunfo.1 |
. . . . . . . . . 10
      |
68 | 67 | eleq2i 2472 |
. . . . . . . . 9

       |
69 | | eliun 4061 |
. . . . . . . . 9
     

      |
70 | 68, 69 | bitri 241 |
. . . . . . . 8


      |
71 | | r19.29 2810 |
. . . . . . . . . 10
           
     
        
       |
72 | | xp1st 6339 |
. . . . . . . . . . . . . . 15
             |
73 | 72 | ad2antll 710 |
. . . . . . . . . . . . . 14
                         |
74 | | elsni 3802 |
. . . . . . . . . . . . . 14
             |
75 | 73, 74 | syl 16 |
. . . . . . . . . . . . 13
                       |
76 | | simpl 444 |
. . . . . . . . . . . . 13
                   |
77 | 75, 76 | eqeltrd 2482 |
. . . . . . . . . . . 12
                       |
78 | 75 | fveq2d 5695 |
. . . . . . . . . . . . . 14
                               |
79 | 78 | fveq1d 5693 |
. . . . . . . . . . . . 13
                                               |
80 | | f1f 5602 |
. . . . . . . . . . . . . . 15
                   |
81 | 80 | ad2antrl 709 |
. . . . . . . . . . . . . 14
                           |
82 | | xp2nd 6340 |
. . . . . . . . . . . . . . 15
           |
83 | 82 | ad2antll 710 |
. . . . . . . . . . . . . 14
                       |
84 | 81, 83 | ffvelrnd 5834 |
. . . . . . . . . . . . 13
                               |
85 | 79, 84 | eqeltrd 2482 |
. . . . . . . . . . . 12
                                   |
86 | | opelxpi 4873 |
. . . . . . . . . . . 12
                                                  |
87 | 77, 85, 86 | syl2anc 643 |
. . . . . . . . . . 11
                                       
    |
88 | 87 | rexlimiva 2789 |
. . . . . . . . . 10
          
                           
    |
89 | 71, 88 | syl 16 |
. . . . . . . . 9
           
                                |
90 | 89 | ex 424 |
. . . . . . . 8
 
       
                            
     |
91 | 70, 90 | syl5bi 209 |
. . . . . . 7
 
       
                             |
92 | | fvex 5705 |
. . . . . . . . . 10
     |
93 | | fvex 5705 |
. . . . . . . . . 10
                 |
94 | 92, 93 | opth 4399 |
. . . . . . . . 9
                       
                                                                   |
95 | | simpr 448 |
. . . . . . . . . . . . . . 15
                                  |
96 | 95 | fveq2d 5695 |
. . . . . . . . . . . . . 14
                                          |
97 | 96 | fveq1d 5693 |
. . . . . . . . . . . . 13
                                                          |
98 | 97 | eqeq2d 2419 |
. . . . . . . . . . . 12
                                                        
                                   |
99 | | djussxp 4981 |
. . . . . . . . . . . . . . . . . 18

   
   |
100 | 67, 99 | eqsstri 3342 |
. . . . . . . . . . . . . . . . 17

  |
101 | | simprl 733 |
. . . . . . . . . . . . . . . . 17
           
    |
102 | 100, 101 | sseldi 3310 |
. . . . . . . . . . . . . . . 16
           
      |
103 | 102 | adantr 452 |
. . . . . . . . . . . . . . 15
                            |
104 | | xp1st 6339 |
. . . . . . . . . . . . . . 15
  
      |
105 | 103, 104 | syl 16 |
. . . . . . . . . . . . . 14
                              |
106 | | simpll 731 |
. . . . . . . . . . . . . 14
                        
          |
107 | | nfcv 2544 |
. . . . . . . . . . . . . . . 16
           |
108 | | nfcsb1v 3247 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif)  |
109 | 107, 108,
28 | nff1 5600 |
. . . . . . . . . . . . . . 15
                  ![]_ ]_](_urbrack.gif)    |
110 | | fveq2 5691 |
. . . . . . . . . . . . . . . . 17
    
              |
111 | | f1eq1 5597 |
. . . . . . . . . . . . . . . . 17
            
        
               |
112 | 110, 111 | syl 16 |
. . . . . . . . . . . . . . . 16
    
        
               |
113 | | csbeq1a 3223 |
. . . . . . . . . . . . . . . . 17
    
      ![]_ ]_](_urbrack.gif)   |
114 | | f1eq2 5598 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)
            
                ![]_ ]_](_urbrack.gif)      |
115 | 113, 114 | syl 16 |
. . . . . . . . . . . . . . . 16
    
            
                ![]_ ]_](_urbrack.gif)      |
116 | 112, 115 | bitrd 245 |
. . . . . . . . . . . . . . 15
    
        
                ![]_ ]_](_urbrack.gif)      |
117 | 109, 116 | rspc 3010 |
. . . . . . . . . . . . . 14
      
                        ![]_ ]_](_urbrack.gif)      |
118 | 105, 106,
117 | sylc 58 |
. . . . . . . . . . . . 13
                                        ![]_ ]_](_urbrack.gif)     |
119 | 108 | nfel2 2556 |
. . . . . . . . . . . . . . . . . . . 20
            ![]_ ]_](_urbrack.gif)  |
120 | 75 | eqcomd 2413 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
121 | 120, 113 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
                       ![]_ ]_](_urbrack.gif)   |
122 | 83, 121 | eleqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . 21
                           ![]_ ]_](_urbrack.gif)   |
123 | 122 | ex 424 |
. . . . . . . . . . . . . . . . . . . 20
                          ![]_ ]_](_urbrack.gif)    |
124 | 119, 123 | rexlimi 2787 |
. . . . . . . . . . . . . . . . . . 19
          
               ![]_ ]_](_urbrack.gif)   |
125 | 71, 124 | syl 16 |
. . . . . . . . . . . . . . . . . 18
           
               ![]_ ]_](_urbrack.gif)   |
126 | 125 | ex 424 |
. . . . . . . . . . . . . . . . 17
 
       
                ![]_ ]_](_urbrack.gif)    |
127 | 70, 126 | syl5bi 209 |
. . . . . . . . . . . . . . . 16
 
       
           ![]_ ]_](_urbrack.gif)    |
128 | 127 | imp 419 |
. . . . . . . . . . . . . . 15
          

          ![]_ ]_](_urbrack.gif)   |
129 | 128 | adantrr 698 |
. . . . . . . . . . . . . 14
           
            ![]_ ]_](_urbrack.gif)   |
130 | 129 | adantr 452 |
. . . . . . . . . . . . 13
                                  ![]_ ]_](_urbrack.gif)   |
131 | 127 | ralrimiv 2752 |
. . . . . . . . . . . . . . . . 17
 
       

          ![]_ ]_](_urbrack.gif)   |
132 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . . 19
           |
133 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . . . 20
           |
134 | 133 | csbeq1d 3221 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
135 | 132, 134 | eleq12d 2476 |
. . . . . . . . . . . . . . . . . 18
            ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)    |
136 | 135 | rspccva 3015 |
. . . . . . . . . . . . . . . . 17
             ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)   |
137 | 131, 136 | sylan 458 |
. . . . . . . . . . . . . . . 16
          

          ![]_ ]_](_urbrack.gif)   |
138 | 137 | adantrl 697 |
. . . . . . . . . . . . . . 15
           
            ![]_ ]_](_urbrack.gif)   |
139 | 138 | adantr 452 |
. . . . . . . . . . . . . 14
                                  ![]_ ]_](_urbrack.gif)   |
140 | 95 | csbeq1d 3221 |
. . . . . . . . . . . . . 14
                              ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
141 | 139, 140 | eleqtrrd 2485 |
. . . . . . . . . . . . 13
                                  ![]_ ]_](_urbrack.gif)   |
142 | | f1fveq 5971 |
. . . . . . . . . . . . 13
                  ![]_ ]_](_urbrack.gif)  
           ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)                                               |
143 | 118, 130,
141, 142 | syl12anc 1182 |
. . . . . . . . . . . 12
                                                        
           |
144 | 98, 143 | bitr3d 247 |
. . . . . . . . . . 11
                                                        
           |
145 | 144 | pm5.32da 623 |
. . . . . . . . . 10
           
                                            
        
            |
146 | | simprr 734 |
. . . . . . . . . . . 12
           
    |
147 | 100, 146 | sseldi 3310 |
. . . . . . . . . . 11
           
      |
148 | | xpopth 6351 |
. . . . . . . . . . 11
   
                     
   |
149 | 102, 147,
148 | syl2anc 643 |
. . . . . . . . . 10
           
                    
   |
150 | 145, 149 | bitrd 245 |
. . . . . . . . 9
           
                                            
   |
151 | 94, 150 | syl5bb 249 |
. . . . . . . 8
           
                         
                          |
152 | 151 | ex 424 |
. . . . . . 7
 
       
 
                        
                           |
153 | 91, 152 | dom2d 7111 |
. . . . . 6
 
       
   
    |
154 | 66, 153 | syl5com 28 |
. . . . 5
                |
155 | 49, 154 | syl5bir 210 |
. . . 4
           ![]_ ]_](_urbrack.gif)        |
156 | 155 | adantld 454 |
. . 3
        
          ![]_ ]_](_urbrack.gif)   
     |
157 | 156 | exlimdv 1643 |
. 2
         
  
        ![]_ ]_](_urbrack.gif)         |
158 | 39, 157 | mpd 15 |
1
     |