Step | Hyp | Ref
| Expression |
1 | | unieq 4206 |
. . . . . . . . 9

    |
2 | | uni0 4225 |
. . . . . . . . 9
  |
3 | 1, 2 | syl6eq 2501 |
. . . . . . . 8

   |
4 | 3 | eleq1d 2513 |
. . . . . . 7

 
   |
5 | | mretopd.j |
. . . . . . . . . . . . . 14
 
    |
6 | | ssrab2 3514 |
. . . . . . . . . . . . . 14
       |
7 | 5, 6 | eqsstri 3462 |
. . . . . . . . . . . . 13
  |
8 | | sstr 3440 |
. . . . . . . . . . . . 13
 
     |
9 | 7, 8 | mpan2 677 |
. . . . . . . . . . . 12
    |
10 | 9 | adantl 468 |
. . . . . . . . . . 11
 
    |
11 | | sspwuni 4367 |
. . . . . . . . . . 11
 
   |
12 | 10, 11 | sylib 200 |
. . . . . . . . . 10
 
    |
13 | | vex 3048 |
. . . . . . . . . . . 12
 |
14 | 13 | uniex 6587 |
. . . . . . . . . . 11
  |
15 | 14 | elpw 3957 |
. . . . . . . . . 10
 
 
  |
16 | 12, 15 | sylibr 216 |
. . . . . . . . 9
 
     |
17 | 16 | adantr 467 |
. . . . . . . 8
         |
18 | | uniiun 4331 |
. . . . . . . . . 10
   |
19 | 18 | difeq2i 3548 |
. . . . . . . . 9
    
  |
20 | | iindif2 4347 |
. . . . . . . . . . 11

    
   |
21 | 20 | adantl 468 |
. . . . . . . . . 10
     
   
   |
22 | | mretopd.m |
. . . . . . . . . . . 12
 Moore    |
23 | 22 | ad2antrr 732 |
. . . . . . . . . . 11
     Moore    |
24 | | simpr 463 |
. . . . . . . . . . 11
       |
25 | | difeq2 3545 |
. . . . . . . . . . . . . . . . 17
       |
26 | 25 | eleq1d 2513 |
. . . . . . . . . . . . . . . 16
   
     |
27 | 26, 5 | elrab2 3198 |
. . . . . . . . . . . . . . 15

       |
28 | 27 | simprbi 466 |
. . . . . . . . . . . . . 14
     |
29 | 28 | rgen 2747 |
. . . . . . . . . . . . 13

   |
30 | | ssralv 3493 |
. . . . . . . . . . . . . 14
  

 
     |
31 | 30 | adantl 468 |
. . . . . . . . . . . . 13
 
  

 
     |
32 | 29, 31 | mpi 20 |
. . . . . . . . . . . 12
 
 
    |
33 | 32 | adantr 467 |
. . . . . . . . . . 11
     
    |
34 | | mreiincl 15502 |
. . . . . . . . . . 11
  Moore  
  
     |
35 | 23, 24, 33, 34 | syl3anc 1268 |
. . . . . . . . . 10
     
    |
36 | 21, 35 | eqeltrrd 2530 |
. . . . . . . . 9
          |
37 | 19, 36 | syl5eqel 2533 |
. . . . . . . 8
          |
38 | | difeq2 3545 |
. . . . . . . . . 10
         |
39 | 38 | eleq1d 2513 |
. . . . . . . . 9
           |
40 | 39, 5 | elrab2 3198 |
. . . . . . . 8
 
 
       |
41 | 17, 37, 40 | sylanbrc 670 |
. . . . . . 7
        |
42 | | 0elpw 4572 |
. . . . . . . . . 10
  |
43 | 42 | a1i 11 |
. . . . . . . . 9

   |
44 | | mre1cl 15500 |
. . . . . . . . . 10
 Moore 
  |
45 | 22, 44 | syl 17 |
. . . . . . . . 9
   |
46 | | difeq2 3545 |
. . . . . . . . . . . 12

      |
47 | | dif0 3837 |
. . . . . . . . . . . 12
   |
48 | 46, 47 | syl6eq 2501 |
. . . . . . . . . . 11

    |
49 | 48 | eleq1d 2513 |
. . . . . . . . . 10

  
   |
50 | 49, 5 | elrab2 3198 |
. . . . . . . . 9

     |
51 | 43, 45, 50 | sylanbrc 670 |
. . . . . . . 8

  |
52 | 51 | adantr 467 |
. . . . . . 7
 
   |
53 | 4, 41, 52 | pm2.61ne 2709 |
. . . . . 6
 
    |
54 | 53 | ex 436 |
. . . . 5
      |
55 | 54 | alrimiv 1773 |
. . . 4
        |
56 | | inss1 3652 |
. . . . . . . 8
   |
57 | | difeq2 3545 |
. . . . . . . . . . . . 13
       |
58 | 57 | eleq1d 2513 |
. . . . . . . . . . . 12
   
     |
59 | 58, 5 | elrab2 3198 |
. . . . . . . . . . 11

       |
60 | 59 | simplbi 462 |
. . . . . . . . . 10
    |
61 | 60 | elpwid 3961 |
. . . . . . . . 9
   |
62 | 61 | ad2antrl 734 |
. . . . . . . 8
 

 
  |
63 | 56, 62 | syl5ss 3443 |
. . . . . . 7
 

   
  |
64 | 13 | inex1 4544 |
. . . . . . . 8
   |
65 | 64 | elpw 3957 |
. . . . . . 7
   
    |
66 | 63, 65 | sylibr 216 |
. . . . . 6
 

       |
67 | | difindi 3697 |
. . . . . . 7
           |
68 | 59 | simprbi 466 |
. . . . . . . . 9
     |
69 | 68 | ad2antrl 734 |
. . . . . . . 8
 

      |
70 | 28 | ad2antll 735 |
. . . . . . . 8
 

      |
71 | | simpl 459 |
. . . . . . . 8
 

    |
72 | | uneq1 3581 |
. . . . . . . . . . . 12
           |
73 | 72 | eleq1d 2513 |
. . . . . . . . . . 11
     
       |
74 | 73 | imbi2d 318 |
. . . . . . . . . 10
    
  
         |
75 | | uneq2 3582 |
. . . . . . . . . . . 12
               |
76 | 75 | eleq1d 2513 |
. . . . . . . . . . 11
       
         |
77 | 76 | imbi2d 318 |
. . . . . . . . . 10
    
    
           |
78 | | mretopd.u |
. . . . . . . . . . . 12
 

    |
79 | 78 | 3expb 1209 |
. . . . . . . . . . 11
 

      |
80 | 79 | expcom 437 |
. . . . . . . . . 10
 
       |
81 | 74, 77, 80 | vtocl2ga 3115 |
. . . . . . . . 9
    
            |
82 | 81 | imp 431 |
. . . . . . . 8
                 |
83 | 69, 70, 71, 82 | syl21anc 1267 |
. . . . . . 7
 

          |
84 | 67, 83 | syl5eqel 2533 |
. . . . . 6
 

   
    |
85 | | difeq2 3545 |
. . . . . . . 8
      
    |
86 | 85 | eleq1d 2513 |
. . . . . . 7
     
       |
87 | 86, 5 | elrab2 3198 |
. . . . . 6
  
 
         |
88 | 66, 84, 87 | sylanbrc 670 |
. . . . 5
 

      |
89 | 88 | ralrimivva 2809 |
. . . 4
  
    |
90 | | pwexg 4587 |
. . . . . . 7
 
  |
91 | 45, 90 | syl 17 |
. . . . . 6
    |
92 | 5, 91 | rabexd 4555 |
. . . . 5
   |
93 | | istopg 19925 |
. . . . 5
 
     


      |
94 | 92, 93 | syl 17 |
. . . 4
       


      |
95 | 55, 89, 94 | mpbir2and 933 |
. . 3
   |
96 | 7 | unissi 4221 |
. . . . . 6
    |
97 | | unipw 4650 |
. . . . . 6
 
 |
98 | 96, 97 | sseqtri 3464 |
. . . . 5
  |
99 | | pwidg 3964 |
. . . . . . 7
    |
100 | 45, 99 | syl 17 |
. . . . . 6
    |
101 | | difid 3835 |
. . . . . . 7
   |
102 | | mretopd.z |
. . . . . . 7

  |
103 | 101, 102 | syl5eqel 2533 |
. . . . . 6
     |
104 | | difeq2 3545 |
. . . . . . . 8
       |
105 | 104 | eleq1d 2513 |
. . . . . . 7
   
     |
106 | 105, 5 | elrab2 3198 |
. . . . . 6

       |
107 | 100, 103,
106 | sylanbrc 670 |
. . . . 5
   |
108 | | unissel 4228 |
. . . . 5
  

   |
109 | 98, 107, 108 | sylancr 669 |
. . . 4
    |
110 | 109 | eqcomd 2457 |
. . 3
    |
111 | | istopon 19940 |
. . 3
 TopOn  
    |
112 | 95, 110, 111 | sylanbrc 670 |
. 2
 TopOn    |
113 | | eqid 2451 |
. . . . 5
   |
114 | 113 | cldval 20038 |
. . . 4
              |
115 | 95, 114 | syl 17 |
. . 3
              |
116 | 109 | pweqd 3956 |
. . . 4
      |
117 | 109 | difeq1d 3550 |
. . . . 5
        |
118 | 117 | eleq1d 2513 |
. . . 4
          |
119 | 116, 118 | rabeqbidv 3040 |
. . 3
               |
120 | 5 | eleq2i 2521 |
. . . . . . 7
  
         |
121 | | difss 3560 |
. . . . . . . . . 10
   |
122 | | elpw2g 4566 |
. . . . . . . . . . 11
          |
123 | 45, 122 | syl 17 |
. . . . . . . . . 10
      
   |
124 | 121, 123 | mpbiri 237 |
. . . . . . . . 9
      |
125 | | difeq2 3545 |
. . . . . . . . . . 11
           |
126 | 125 | eleq1d 2513 |
. . . . . . . . . 10
     
       |
127 | 126 | elrab3 3197 |
. . . . . . . . 9
                   |
128 | 124, 127 | syl 17 |
. . . . . . . 8
                |
129 | 128 | adantr 467 |
. . . . . . 7
 
                 |
130 | 120, 129 | syl5bb 261 |
. . . . . 6
 
    
       |
131 | | elpwi 3960 |
. . . . . . . . 9
    |
132 | | dfss4 3677 |
. . . . . . . . 9

      |
133 | 131, 132 | sylib 200 |
. . . . . . . 8
        |
134 | 133 | adantl 468 |
. . . . . . 7
 
        |
135 | 134 | eleq1d 2513 |
. . . . . 6
 
      
   |
136 | 130, 135 | bitrd 257 |
. . . . 5
 
    
   |
137 | 136 | rabbidva 3035 |
. . . 4
  
  
     |
138 | | incom 3625 |
. . . . . 6
       |
139 | | dfin5 3412 |
. . . . . 6
       |
140 | 138, 139 | eqtri 2473 |
. . . . 5
       |
141 | | mresspw 15498 |
. . . . . . 7
 Moore 
   |
142 | 22, 141 | syl 17 |
. . . . . 6

   |
143 | | df-ss 3418 |
. . . . . 6
 
     |
144 | 142, 143 | sylib 200 |
. . . . 5
      |
145 | 140, 144 | syl5eqr 2499 |
. . . 4
  

  |
146 | 137, 145 | eqtrd 2485 |
. . 3
  
  
  |
147 | 115, 119,
146 | 3eqtrrd 2490 |
. 2
       |
148 | 112, 147 | jca 535 |
1
  TopOn         |