Step | Hyp | Ref
| Expression |
1 | | wuncval2.f |
. . . 4
        
     
              |
2 | | wuncval2.u |
. . . 4

 |
3 | 1, 2 | wunex2 9163 |
. . 3
 
WUni    |
4 | | wuncss 9170 |
. . 3
  WUni  wUniCl    |
5 | 3, 4 | syl 17 |
. 2
 wUniCl    |
6 | | frfnom 7152 |
. . . . . 6
            
 
              |
7 | 1 | fneq1i 5670 |
. . . . . 6

            
 
               |
8 | 6, 7 | mpbir 213 |
. . . . 5
 |
9 | | fniunfv 6152 |
. . . . 5
         |
10 | 8, 9 | ax-mp 5 |
. . . 4
       |
11 | 2, 10 | eqtr4i 2476 |
. . 3
      |
12 | | fveq2 5865 |
. . . . . . . 8

          |
13 | 12 | sseq1d 3459 |
. . . . . . 7

     wUniCl      wUniCl     |
14 | | fveq2 5865 |
. . . . . . . 8
           |
15 | 14 | sseq1d 3459 |
. . . . . . 7
     
wUniCl      wUniCl     |
16 | | fveq2 5865 |
. . . . . . . 8
       
   |
17 | 16 | sseq1d 3459 |
. . . . . . 7
      wUniCl 
    wUniCl     |
18 | | 1on 7189 |
. . . . . . . . . 10
 |
19 | | unexg 6592 |
. . . . . . . . . 10
    
  |
20 | 18, 19 | mpan2 677 |
. . . . . . . . 9
 
   |
21 | 1 | fveq1i 5866 |
. . . . . . . . . 10
             
     
                 |
22 | | fr0g 7153 |
. . . . . . . . . 10
            
     
                    |
23 | 21, 22 | syl5eq 2497 |
. . . . . . . . 9
           |
24 | 20, 23 | syl 17 |
. . . . . . . 8
         |
25 | | wuncid 9168 |
. . . . . . . . 9
 wUniCl    |
26 | | df1o2 7194 |
. . . . . . . . . 10
   |
27 | | wunccl 9169 |
. . . . . . . . . . . 12
 wUniCl  WUni |
28 | 27 | wun0 9143 |
. . . . . . . . . . 11
 wUniCl    |
29 | 28 | snssd 4117 |
. . . . . . . . . 10
   wUniCl    |
30 | 26, 29 | syl5eqss 3476 |
. . . . . . . . 9
 wUniCl    |
31 | 25, 30 | unssd 3610 |
. . . . . . . 8
 
 wUniCl    |
32 | 24, 31 | eqsstrd 3466 |
. . . . . . 7
     wUniCl    |
33 | | simplr 762 |
. . . . . . . . . . 11
  
     wUniCl  
  |
34 | | fvex 5875 |
. . . . . . . . . . . . 13
     |
35 | 34 | uniex 6587 |
. . . . . . . . . . . . 13
      |
36 | 34, 35 | unex 6589 |
. . . . . . . . . . . 12
            |
37 | | prex 4642 |
. . . . . . . . . . . . . 14
  
 
 |
38 | 34 | mptex 6136 |
. . . . . . . . . . . . . . 15
          |
39 | 38 | rnex 6727 |
. . . . . . . . . . . . . 14
          |
40 | 37, 39 | unex 6589 |
. . . . . . . . . . . . 13
     
           |
41 | 34, 40 | iunex 6773 |
. . . . . . . . . . . 12
         
 
           |
42 | 36, 41 | unex 6589 |
. . . . . . . . . . 11
                     
 
            |
43 | | id 22 |
. . . . . . . . . . . . . 14
   |
44 | | unieq 4206 |
. . . . . . . . . . . . . 14
     |
45 | 43, 44 | uneq12d 3589 |
. . . . . . . . . . . . 13
         |
46 | | pweq 3954 |
. . . . . . . . . . . . . . . . 17
 
   |
47 | | unieq 4206 |
. . . . . . . . . . . . . . . . 17
     |
48 | 46, 47 | preq12d 4059 |
. . . . . . . . . . . . . . . 16
   
 
  
    |
49 | | preq1 4051 |
. . . . . . . . . . . . . . . . . 18
         |
50 | 49 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . 17
             |
51 | 50 | rneqd 5062 |
. . . . . . . . . . . . . . . 16
             |
52 | 48, 51 | uneq12d 3589 |
. . . . . . . . . . . . . . 15
      
                    |
53 | 52 | cbviunv 4317 |
. . . . . . . . . . . . . 14

     
      
     
       |
54 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . 19
         |
55 | 54 | cbvmptv 4495 |
. . . . . . . . . . . . . . . . . 18
           |
56 | | mpteq1 4483 |
. . . . . . . . . . . . . . . . . 18
             |
57 | 55, 56 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
             |
58 | 57 | rneqd 5062 |
. . . . . . . . . . . . . . . 16
             |
59 | 58 | uneq2d 3588 |
. . . . . . . . . . . . . . 15
      
                    |
60 | 43, 59 | iuneq12d 4304 |
. . . . . . . . . . . . . 14
 
     
      
     
        |
61 | 53, 60 | syl5eq 2497 |
. . . . . . . . . . . . 13
 
     
      
     
        |
62 | 45, 61 | uneq12d 3589 |
. . . . . . . . . . . 12
     
     
               
 
         |
63 | | id 22 |
. . . . . . . . . . . . . 14
           |
64 | | unieq 4206 |
. . . . . . . . . . . . . 14
             |
65 | 63, 64 | uneq12d 3589 |
. . . . . . . . . . . . 13
                     |
66 | | mpteq1 4483 |
. . . . . . . . . . . . . . . 16
                     |
67 | 66 | rneqd 5062 |
. . . . . . . . . . . . . . 15
                     |
68 | 67 | uneq2d 3588 |
. . . . . . . . . . . . . 14
          
                        |
69 | 63, 68 | iuneq12d 4304 |
. . . . . . . . . . . . 13
     
     
               
 
            |
70 | 65, 69 | uneq12d 3589 |
. . . . . . . . . . . 12
         
     
                            
 
             |
71 | 1, 62, 70 | frsucmpt2 7157 |
. . . . . . . . . . 11
                                                               
 
             |
72 | 33, 42, 71 | sylancl 668 |
. . . . . . . . . 10
  
     wUniCl                            
 
             |
73 | | simpr 463 |
. . . . . . . . . . . 12
  
     wUniCl      
wUniCl    |
74 | 27 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
         wUniCl  
    
wUniCl 
WUni |
75 | 73 | sselda 3432 |
. . . . . . . . . . . . . . 15
         wUniCl  
    
wUniCl    |
76 | 74, 75 | wunelss 9133 |
. . . . . . . . . . . . . 14
         wUniCl  
    
wUniCl    |
77 | 76 | ralrimiva 2802 |
. . . . . . . . . . . . 13
  
     wUniCl   
    
wUniCl    |
78 | | unissb 4229 |
. . . . . . . . . . . . 13
      wUniCl        wUniCl    |
79 | 77, 78 | sylibr 216 |
. . . . . . . . . . . 12
  
     wUniCl       
wUniCl    |
80 | 73, 79 | unssd 3610 |
. . . . . . . . . . 11
  
     wUniCl             
wUniCl    |
81 | 74, 75 | wunpw 9132 |
. . . . . . . . . . . . . . 15
         wUniCl  
    
 wUniCl    |
82 | 74, 75 | wununi 9131 |
. . . . . . . . . . . . . . 15
         wUniCl  
    
 wUniCl    |
83 | | prssi 4128 |
. . . . . . . . . . . . . . 15
   wUniCl  
wUniCl     
  wUniCl    |
84 | 81, 82, 83 | syl2anc 667 |
. . . . . . . . . . . . . 14
         wUniCl  
    
  
  wUniCl    |
85 | 74 | adantr 467 |
. . . . . . . . . . . . . . . . 17
          wUniCl  
          wUniCl  WUni |
86 | 75 | adantr 467 |
. . . . . . . . . . . . . . . . 17
          wUniCl  
          wUniCl    |
87 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
         wUniCl  
    
    wUniCl    |
88 | 87 | sselda 3432 |
. . . . . . . . . . . . . . . . 17
          wUniCl  
          wUniCl    |
89 | 85, 86, 88 | wunpr 9134 |
. . . . . . . . . . . . . . . 16
          wUniCl  
             wUniCl    |
90 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
                   |
91 | 89, 90 | fmptd 6046 |
. . . . . . . . . . . . . . 15
         wUniCl  
    
                 wUniCl    |
92 | | frn 5735 |
. . . . . . . . . . . . . . 15
                  wUniCl           wUniCl    |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
         wUniCl  
    
         wUniCl    |
94 | 84, 93 | unssd 3610 |
. . . . . . . . . . . . 13
         wUniCl  
    
     
         
wUniCl    |
95 | 94 | ralrimiva 2802 |
. . . . . . . . . . . 12
  
     wUniCl   
                     wUniCl    |
96 | | iunss 4319 |
. . . . . . . . . . . 12
 
          
          wUniCl 
         
 
         
wUniCl    |
97 | 95, 96 | sylibr 216 |
. . . . . . . . . . 11
  
     wUniCl   
                     wUniCl    |
98 | 80, 97 | unssd 3610 |
. . . . . . . . . 10
  
     wUniCl                                      wUniCl    |
99 | 72, 98 | eqsstrd 3466 |
. . . . . . . . 9
  
     wUniCl       wUniCl    |
100 | 99 | ex 436 |
. . . . . . . 8
 
      wUniCl      wUniCl     |
101 | 100 | expcom 437 |
. . . . . . 7
 
    
wUniCl 
    wUniCl      |
102 | 13, 15, 17, 32, 101 | finds2 6721 |
. . . . . 6
 
    wUniCl     |
103 | 102 | com12 32 |
. . . . 5
      wUniCl     |
104 | 103 | ralrimiv 2800 |
. . . 4
      wUniCl    |
105 | | iunss 4319 |
. . . 4
 
    wUniCl       wUniCl    |
106 | 104, 105 | sylibr 216 |
. . 3
      wUniCl    |
107 | 11, 106 | syl5eqss 3476 |
. 2
 wUniCl    |
108 | 5, 107 | eqssd 3449 |
1
 wUniCl    |