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

    |
2 | | uni0 4217 |
. . . . . . . . 9
  |
3 | 1, 2 | syl6eq 2521 |
. . . . . . . 8

   |
4 | 3 | eleq1d 2533 |
. . . . . . 7

 
   |
5 | | mretopd.j |
. . . . . . . . . . . . . 14
 
    |
6 | | ssrab2 3500 |
. . . . . . . . . . . . . 14
       |
7 | 5, 6 | eqsstri 3448 |
. . . . . . . . . . . . 13
  |
8 | | sstr 3426 |
. . . . . . . . . . . . 13
 
     |
9 | 7, 8 | mpan2 685 |
. . . . . . . . . . . 12
    |
10 | 9 | adantl 473 |
. . . . . . . . . . 11
 
    |
11 | | sspwuni 4360 |
. . . . . . . . . . 11
 
   |
12 | 10, 11 | sylib 201 |
. . . . . . . . . 10
 
    |
13 | | vex 3034 |
. . . . . . . . . . . 12
 |
14 | 13 | uniex 6606 |
. . . . . . . . . . 11
  |
15 | 14 | elpw 3948 |
. . . . . . . . . 10
 
 
  |
16 | 12, 15 | sylibr 217 |
. . . . . . . . 9
 
     |
17 | 16 | adantr 472 |
. . . . . . . 8
         |
18 | | uniiun 4322 |
. . . . . . . . . 10
   |
19 | 18 | difeq2i 3537 |
. . . . . . . . 9
    
  |
20 | | iindif2 4338 |
. . . . . . . . . . 11

    
   |
21 | 20 | adantl 473 |
. . . . . . . . . 10
     
   
   |
22 | | mretopd.m |
. . . . . . . . . . . 12
 Moore    |
23 | 22 | ad2antrr 740 |
. . . . . . . . . . 11
     Moore    |
24 | | simpr 468 |
. . . . . . . . . . 11
       |
25 | | difeq2 3534 |
. . . . . . . . . . . . . . . . 17
       |
26 | 25 | eleq1d 2533 |
. . . . . . . . . . . . . . . 16
   
     |
27 | 26, 5 | elrab2 3186 |
. . . . . . . . . . . . . . 15

       |
28 | 27 | simprbi 471 |
. . . . . . . . . . . . . 14
     |
29 | 28 | rgen 2766 |
. . . . . . . . . . . . 13

   |
30 | | ssralv 3479 |
. . . . . . . . . . . . . 14
  

 
     |
31 | 30 | adantl 473 |
. . . . . . . . . . . . 13
 
  

 
     |
32 | 29, 31 | mpi 20 |
. . . . . . . . . . . 12
 
 
    |
33 | 32 | adantr 472 |
. . . . . . . . . . 11
     
    |
34 | | mreiincl 15580 |
. . . . . . . . . . 11
  Moore  
  
     |
35 | 23, 24, 33, 34 | syl3anc 1292 |
. . . . . . . . . 10
     
    |
36 | 21, 35 | eqeltrrd 2550 |
. . . . . . . . 9
          |
37 | 19, 36 | syl5eqel 2553 |
. . . . . . . 8
          |
38 | | difeq2 3534 |
. . . . . . . . . 10
         |
39 | 38 | eleq1d 2533 |
. . . . . . . . 9
           |
40 | 39, 5 | elrab2 3186 |
. . . . . . . 8
 
 
       |
41 | 17, 37, 40 | sylanbrc 677 |
. . . . . . 7
        |
42 | | 0elpw 4570 |
. . . . . . . . . 10
  |
43 | 42 | a1i 11 |
. . . . . . . . 9

   |
44 | | mre1cl 15578 |
. . . . . . . . . 10
 Moore 
  |
45 | 22, 44 | syl 17 |
. . . . . . . . 9
   |
46 | | difeq2 3534 |
. . . . . . . . . . . 12

      |
47 | | dif0 3749 |
. . . . . . . . . . . 12
   |
48 | 46, 47 | syl6eq 2521 |
. . . . . . . . . . 11

    |
49 | 48 | eleq1d 2533 |
. . . . . . . . . 10

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

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

  |
52 | 51 | adantr 472 |
. . . . . . 7
 
   |
53 | 4, 41, 52 | pm2.61ne 2728 |
. . . . . 6
 
    |
54 | 53 | ex 441 |
. . . . 5
      |
55 | 54 | alrimiv 1781 |
. . . 4
        |
56 | | inss1 3643 |
. . . . . . . 8
   |
57 | | difeq2 3534 |
. . . . . . . . . . . . 13
       |
58 | 57 | eleq1d 2533 |
. . . . . . . . . . . 12
   
     |
59 | 58, 5 | elrab2 3186 |
. . . . . . . . . . 11

       |
60 | 59 | simplbi 467 |
. . . . . . . . . 10
    |
61 | 60 | elpwid 3952 |
. . . . . . . . 9
   |
62 | 61 | ad2antrl 742 |
. . . . . . . 8
 

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

   
  |
64 | 13 | inex1 4537 |
. . . . . . . 8
   |
65 | 64 | elpw 3948 |
. . . . . . 7
   
    |
66 | 63, 65 | sylibr 217 |
. . . . . 6
 

       |
67 | | difindi 3688 |
. . . . . . 7
           |
68 | 59 | simprbi 471 |
. . . . . . . . 9
     |
69 | 68 | ad2antrl 742 |
. . . . . . . 8
 

      |
70 | 28 | ad2antll 743 |
. . . . . . . 8
 

      |
71 | | simpl 464 |
. . . . . . . 8
 

    |
72 | | uneq1 3572 |
. . . . . . . . . . . 12
           |
73 | 72 | eleq1d 2533 |
. . . . . . . . . . 11
     
       |
74 | 73 | imbi2d 323 |
. . . . . . . . . 10
    
  
         |
75 | | uneq2 3573 |
. . . . . . . . . . . 12
               |
76 | 75 | eleq1d 2533 |
. . . . . . . . . . 11
       
         |
77 | 76 | imbi2d 323 |
. . . . . . . . . 10
    
    
           |
78 | | mretopd.u |
. . . . . . . . . . . 12
 

    |
79 | 78 | 3expb 1232 |
. . . . . . . . . . 11
 

      |
80 | 79 | expcom 442 |
. . . . . . . . . 10
 
       |
81 | 74, 77, 80 | vtocl2ga 3101 |
. . . . . . . . 9
    
            |
82 | 81 | imp 436 |
. . . . . . . 8
                 |
83 | 69, 70, 71, 82 | syl21anc 1291 |
. . . . . . 7
 

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

   
    |
85 | | difeq2 3534 |
. . . . . . . 8
      
    |
86 | 85 | eleq1d 2533 |
. . . . . . 7
     
       |
87 | 86, 5 | elrab2 3186 |
. . . . . 6
  
 
         |
88 | 66, 84, 87 | sylanbrc 677 |
. . . . 5
 

      |
89 | 88 | ralrimivva 2814 |
. . . 4
  
    |
90 | | pwexg 4585 |
. . . . . . 7
 
  |
91 | 45, 90 | syl 17 |
. . . . . 6
    |
92 | 5, 91 | rabexd 4551 |
. . . . 5
   |
93 | | istopg 20002 |
. . . . 5
 
     


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


      |
95 | 55, 89, 94 | mpbir2and 936 |
. . 3
   |
96 | 7 | unissi 4213 |
. . . . . 6
    |
97 | | unipw 4650 |
. . . . . 6
 
 |
98 | 96, 97 | sseqtri 3450 |
. . . . 5
  |
99 | | pwidg 3955 |
. . . . . . 7
    |
100 | 45, 99 | syl 17 |
. . . . . 6
    |
101 | | difid 3747 |
. . . . . . 7
   |
102 | | mretopd.z |
. . . . . . 7

  |
103 | 101, 102 | syl5eqel 2553 |
. . . . . 6
     |
104 | | difeq2 3534 |
. . . . . . . 8
       |
105 | 104 | eleq1d 2533 |
. . . . . . 7
   
     |
106 | 105, 5 | elrab2 3186 |
. . . . . 6

       |
107 | 100, 103,
106 | sylanbrc 677 |
. . . . 5
   |
108 | | unissel 4220 |
. . . . 5
  

   |
109 | 98, 107, 108 | sylancr 676 |
. . . 4
    |
110 | 109 | eqcomd 2477 |
. . 3
    |
111 | | istopon 20017 |
. . 3
 TopOn  
    |
112 | 95, 110, 111 | sylanbrc 677 |
. 2
 TopOn    |
113 | | eqid 2471 |
. . . . 5
   |
114 | 113 | cldval 20115 |
. . . 4
              |
115 | 95, 114 | syl 17 |
. . 3
              |
116 | 109 | pweqd 3947 |
. . . 4
      |
117 | 109 | difeq1d 3539 |
. . . . 5
        |
118 | 117 | eleq1d 2533 |
. . . 4
          |
119 | 116, 118 | rabeqbidv 3026 |
. . 3
               |
120 | 5 | eleq2i 2541 |
. . . . . . 7
  
         |
121 | | difss 3549 |
. . . . . . . . . 10
   |
122 | | elpw2g 4564 |
. . . . . . . . . . 11
          |
123 | 45, 122 | syl 17 |
. . . . . . . . . 10
      
   |
124 | 121, 123 | mpbiri 241 |
. . . . . . . . 9
      |
125 | | difeq2 3534 |
. . . . . . . . . . 11
           |
126 | 125 | eleq1d 2533 |
. . . . . . . . . 10
     
       |
127 | 126 | elrab3 3185 |
. . . . . . . . 9
                   |
128 | 124, 127 | syl 17 |
. . . . . . . 8
                |
129 | 128 | adantr 472 |
. . . . . . 7
 
                 |
130 | 120, 129 | syl5bb 265 |
. . . . . 6
 
    
       |
131 | | elpwi 3951 |
. . . . . . . . 9
    |
132 | | dfss4 3668 |
. . . . . . . . 9

      |
133 | 131, 132 | sylib 201 |
. . . . . . . 8
        |
134 | 133 | adantl 473 |
. . . . . . 7
 
        |
135 | 134 | eleq1d 2533 |
. . . . . 6
 
      
   |
136 | 130, 135 | bitrd 261 |
. . . . 5
 
    
   |
137 | 136 | rabbidva 3021 |
. . . 4
  
  
     |
138 | | incom 3616 |
. . . . . 6
       |
139 | | dfin5 3398 |
. . . . . 6
       |
140 | 138, 139 | eqtri 2493 |
. . . . 5
       |
141 | | mresspw 15576 |
. . . . . . 7
 Moore 
   |
142 | 22, 141 | syl 17 |
. . . . . 6

   |
143 | | df-ss 3404 |
. . . . . 6
 
     |
144 | 142, 143 | sylib 201 |
. . . . 5
      |
145 | 140, 144 | syl5eqr 2519 |
. . . 4
  

  |
146 | 137, 145 | eqtrd 2505 |
. . 3
  
  
  |
147 | 115, 119,
146 | 3eqtrrd 2510 |
. 2
       |
148 | 112, 147 | jca 541 |
1
  TopOn         |