Step | Hyp | Ref
| Expression |
1 | | r0weon.1 |
. . . . 5
       
                                                    |
2 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
3 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
4 | 2, 3 | uneq12d 3600 |
. . . . . . . . . . 11
                       |
5 | | eqid 2461 |
. . . . . . . . . . 11
  
                          |
6 | | fvex 5897 |
. . . . . . . . . . . 12
     |
7 | | fvex 5897 |
. . . . . . . . . . . 12
     |
8 | 6, 7 | unex 6615 |
. . . . . . . . . . 11
           |
9 | 4, 5, 8 | fvmpt 5970 |
. . . . . . . . . 10
  
                              |
10 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
11 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
12 | 10, 11 | uneq12d 3600 |
. . . . . . . . . . 11
                       |
13 | | fvex 5897 |
. . . . . . . . . . . 12
     |
14 | | fvex 5897 |
. . . . . . . . . . . 12
     |
15 | 13, 14 | unex 6615 |
. . . . . . . . . . 11
           |
16 | 12, 5, 15 | fvmpt 5970 |
. . . . . . . . . 10
  
                              |
17 | 9, 16 | breqan12d 4431 |
. . . . . . . . 9
   
       
                               
                       |
18 | 15 | epelc 4765 |
. . . . . . . . 9
                    
                      |
19 | 17, 18 | syl6bb 269 |
. . . . . . . 8
   
       
                               
                       |
20 | 9, 16 | eqeqan12d 2477 |
. . . . . . . . 9
   
       
                               
                       |
21 | 20 | anbi1d 716 |
. . . . . . . 8
   
                                                                       |
22 | 19, 21 | orbi12d 721 |
. . . . . . 7
   
                                                                                 
                                                 |
23 | 22 | pm5.32i 647 |
. . . . . 6
                                                                                      
   
                                                    |
24 | 23 | opabbii 4480 |
. . . . 5
                                                                                              
                                                        |
25 | 1, 24 | eqtr4i 2486 |
. . . 4
       
                         
                                    
                     |
26 | | xp1st 6849 |
. . . . . . . 8
  
      |
27 | | xp2nd 6850 |
. . . . . . . 8
  
      |
28 | | fvex 5897 |
. . . . . . . . . 10
     |
29 | 28 | elon 5450 |
. . . . . . . . 9
    
      |
30 | | fvex 5897 |
. . . . . . . . . 10
     |
31 | 30 | elon 5450 |
. . . . . . . . 9
    
      |
32 | | ordun 5542 |
. . . . . . . . 9
     
                 |
33 | 29, 31, 32 | syl2anb 486 |
. . . . . . . 8
                       |
34 | 26, 27, 33 | syl2anc 671 |
. . . . . . 7
  
            |
35 | 28, 30 | unex 6615 |
. . . . . . . 8
           |
36 | 35 | elon 5450 |
. . . . . . 7
                       |
37 | 34, 36 | sylibr 217 |
. . . . . 6
  
            |
38 | 5, 37 | fmpti 6067 |
. . . . 5
  
                  |
39 | 38 | a1i 11 |
. . . 4
                      |
40 | | epweon 6636 |
. . . . 5
 |
41 | 40 | a1i 11 |
. . . 4
  |
42 | | leweon.1 |
. . . . . 6
   
   
                                  |
43 | 42 | leweon 8467 |
. . . . 5

  |
44 | 43 | a1i 11 |
. . . 4
    |
45 | | vex 3059 |
. . . . . . . 8
 |
46 | 45 | dmex 6752 |
. . . . . . 7
 |
47 | 45 | rnex 6753 |
. . . . . . 7
 |
48 | 46, 47 | unex 6615 |
. . . . . 6
   |
49 | | imadmres 5345 |
. . . . . . 7
                
                                    |
50 | | inss2 3664 |
. . . . . . . . . 10
       |
51 | | ssun1 3608 |
. . . . . . . . . . . . . 14
   |
52 | 50 | sseli 3439 |
. . . . . . . . . . . . . . . . 17
         |
53 | | 1st2nd2 6856 |
. . . . . . . . . . . . . . . . 17
  
             |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
                  |
55 | | inss1 3663 |
. . . . . . . . . . . . . . . . 17
     |
56 | 55 | sseli 3439 |
. . . . . . . . . . . . . . . 16
       |
57 | 54, 56 | eqeltrrd 2540 |
. . . . . . . . . . . . . . 15
                  |
58 | 28, 30 | opeldm 5056 |
. . . . . . . . . . . . . . 15
                  |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
           |
60 | 51, 59 | sseldi 3441 |
. . . . . . . . . . . . 13
             |
61 | | ssun2 3609 |
. . . . . . . . . . . . . 14
   |
62 | 28, 30 | opelrn 5084 |
. . . . . . . . . . . . . . 15
                  |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . . 14
           |
64 | 61, 63 | sseldi 3441 |
. . . . . . . . . . . . 13
             |
65 | | prssi 4140 |
. . . . . . . . . . . . 13
       
                      |
66 | 60, 64, 65 | syl2anc 671 |
. . . . . . . . . . . 12
                    |
67 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
           |
68 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
           |
69 | | ordunpr 6679 |
. . . . . . . . . . . . 13
                                  |
70 | 67, 68, 69 | syl2anc 671 |
. . . . . . . . . . . 12
                            |
71 | 66, 70 | sseldd 3444 |
. . . . . . . . . . 11
                   |
72 | 71 | rgen 2758 |
. . . . . . . . . 10
                   |
73 | | ssrab 3518 |
. . . . . . . . . 10
       
            
 
   
                      |
74 | 50, 72, 73 | mpbir2an 936 |
. . . . . . . . 9
      
              |
75 | | dmres 5143 |
. . . . . . . . . 10
                                 |
76 | 38 | fdmi 5756 |
. . . . . . . . . . 11
                 |
77 | 76 | ineq2i 3642 |
. . . . . . . . . 10

                    |
78 | 75, 77 | eqtri 2483 |
. . . . . . . . 9
                     |
79 | 5 | mptpreima 5346 |
. . . . . . . . 9
                       
              |
80 | 74, 78, 79 | 3sstr4i 3482 |
. . . . . . . 8
                                      |
81 | | funmpt 5636 |
. . . . . . . . 9
               |
82 | | resss 5146 |
. . . . . . . . . 10
                               |
83 | | dmss 5052 |
. . . . . . . . . 10
                              
                
               |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . 9
                
              |
85 | | funimass3 6020 |
. . . . . . . . 9
                                
             
                 
                  
                                        |
86 | 81, 84, 85 | mp2an 683 |
. . . . . . . 8
                 
                  
                                       |
87 | 80, 86 | mpbir 214 |
. . . . . . 7
                
                    |
88 | 49, 87 | eqsstr3i 3474 |
. . . . . 6
                     |
89 | 48, 88 | ssexi 4561 |
. . . . 5
                   |
90 | 89 | a1i 11 |
. . . 4
                    |
91 | 25, 39, 41, 44, 90 | fnwe 6938 |
. . 3
    |
92 | | epse 4835 |
. . . . 5
Se  |
93 | 92 | a1i 11 |
. . . 4
Se   |
94 | 45 | uniex 6613 |
. . . . . . . 8
  |
95 | 94 | pwex 4599 |
. . . . . . 7
 
 |
96 | 95, 95 | xpex 6621 |
. . . . . 6
       |
97 | 5 | mptpreima 5346 |
. . . . . . . 8
                                  |
98 | | df-rab 2757 |
. . . . . . . 8
  
          
                 |
99 | 97, 98 | eqtri 2483 |
. . . . . . 7
                                    |
100 | 53 | adantr 471 |
. . . . . . . . 9
                            |
101 | | elssuni 4240 |
. . . . . . . . . . . . 13
          
             |
102 | 101 | adantl 472 |
. . . . . . . . . . . 12
                            |
103 | 102 | unssad 3622 |
. . . . . . . . . . 11
                      |
104 | 28 | elpw 3968 |
. . . . . . . . . . 11
              |
105 | 103, 104 | sylibr 217 |
. . . . . . . . . 10
                       |
106 | 102 | unssbd 3623 |
. . . . . . . . . . 11
                      |
107 | 30 | elpw 3968 |
. . . . . . . . . . 11
              |
108 | 106, 107 | sylibr 217 |
. . . . . . . . . 10
                       |
109 | 105, 108 | jca 539 |
. . . . . . . . 9
                               |
110 | | elxp6 6851 |
. . . . . . . . 9
                                    |
111 | 100, 109,
110 | sylanbrc 675 |
. . . . . . . 8
                       |
112 | 111 | abssi 3515 |
. . . . . . 7
                       |
113 | 99, 112 | eqsstri 3473 |
. . . . . 6
                          |
114 | 96, 113 | ssexi 4561 |
. . . . 5
                    |
115 | 114 | a1i 11 |
. . . 4
    
                |
116 | 25, 39, 93, 115 | fnse 6939 |
. . 3
Se     |
117 | 91, 116 | jca 539 |
. 2
   Se      |
118 | 117 | trud 1463 |
1
  
Se     |