Step | Hyp | Ref
| Expression |
1 | | ptunhmeo.g |
. . . . 5
 
    |
2 | | vex 3034 |
. . . . . . . 8
 |
3 | | vex 3034 |
. . . . . . . 8
 |
4 | 2, 3 | op1std 6822 |
. . . . . . 7
          |
5 | 2, 3 | op2ndd 6823 |
. . . . . . 7
          |
6 | 4, 5 | uneq12d 3580 |
. . . . . 6
                  |
7 | 6 | mpt2mpt 6407 |
. . . . 5
               
    |
8 | 1, 7 | eqtr4i 2496 |
. . . 4
               |
9 | | xp1st 6842 |
. . . . . . . . . 10
         |
10 | 9 | adantl 473 |
. . . . . . . . 9
 

        |
11 | | ixpeq2 7554 |
. . . . . . . . . . . . 13
 
                    
       |
12 | | fvres 5893 |
. . . . . . . . . . . . . 14
             |
13 | 12 | unieqd 4200 |
. . . . . . . . . . . . 13
               |
14 | 11, 13 | mprg 2770 |
. . . . . . . . . . . 12

              |
15 | | ptunhmeo.c |
. . . . . . . . . . . . . 14
   |
16 | | ssun1 3588 |
. . . . . . . . . . . . . . 15

  |
17 | | ptunhmeo.u |
. . . . . . . . . . . . . . 15
     |
18 | 16, 17 | syl5sseqr 3467 |
. . . . . . . . . . . . . 14

  |
19 | 15, 18 | ssexd 4543 |
. . . . . . . . . . . . 13
   |
20 | | ptunhmeo.f |
. . . . . . . . . . . . . 14
       |
21 | 20, 18 | fssresd 5762 |
. . . . . . . . . . . . 13
         |
22 | | ptunhmeo.k |
. . . . . . . . . . . . . 14
       |
23 | 22 | ptuni 20686 |
. . . . . . . . . . . . 13
  
                 |
24 | 19, 21, 23 | syl2anc 673 |
. . . . . . . . . . . 12
            |
25 | 14, 24 | syl5eqr 2519 |
. . . . . . . . . . 11
          |
26 | | ptunhmeo.x |
. . . . . . . . . . 11
  |
27 | 25, 26 | syl6eqr 2523 |
. . . . . . . . . 10
         |
28 | 27 | adantr 472 |
. . . . . . . . 9
 

  
       |
29 | 10, 28 | eleqtrrd 2552 |
. . . . . . . 8
 

      
       |
30 | | xp2nd 6843 |
. . . . . . . . . 10
         |
31 | 30 | adantl 473 |
. . . . . . . . 9
 

        |
32 | 17 | eqcomd 2477 |
. . . . . . . . . . . . 13
     |
33 | | ptunhmeo.i |
. . . . . . . . . . . . . 14
     |
34 | | uneqdifeq 3847 |
. . . . . . . . . . . . . 14
 

    
     |
35 | 18, 33, 34 | syl2anc 673 |
. . . . . . . . . . . . 13
         |
36 | 32, 35 | mpbid 215 |
. . . . . . . . . . . 12
     |
37 | 36 | ixpeq1d 7552 |
. . . . . . . . . . 11
          
       |
38 | | ixpeq2 7554 |
. . . . . . . . . . . . . 14
 
                    
       |
39 | | fvres 5893 |
. . . . . . . . . . . . . . 15
             |
40 | 39 | unieqd 4200 |
. . . . . . . . . . . . . 14
               |
41 | 38, 40 | mprg 2770 |
. . . . . . . . . . . . 13

              |
42 | | ssun2 3589 |
. . . . . . . . . . . . . . . 16

  |
43 | 42, 17 | syl5sseqr 3467 |
. . . . . . . . . . . . . . 15

  |
44 | 15, 43 | ssexd 4543 |
. . . . . . . . . . . . . 14
   |
45 | 20, 43 | fssresd 5762 |
. . . . . . . . . . . . . 14
         |
46 | | ptunhmeo.l |
. . . . . . . . . . . . . . 15
       |
47 | 46 | ptuni 20686 |
. . . . . . . . . . . . . 14
  
                 |
48 | 44, 45, 47 | syl2anc 673 |
. . . . . . . . . . . . 13
            |
49 | 41, 48 | syl5eqr 2519 |
. . . . . . . . . . . 12
          |
50 | | ptunhmeo.y |
. . . . . . . . . . . 12
  |
51 | 49, 50 | syl6eqr 2523 |
. . . . . . . . . . 11
         |
52 | 37, 51 | eqtrd 2505 |
. . . . . . . . . 10
            |
53 | 52 | adantr 472 |
. . . . . . . . 9
 

             |
54 | 31, 53 | eleqtrrd 2552 |
. . . . . . . 8
 

      
          |
55 | 18 | adantr 472 |
. . . . . . . 8
 

    |
56 | | undifixp 7576 |
. . . . . . . 8
      
                             
       |
57 | 29, 54, 55, 56 | syl3anc 1292 |
. . . . . . 7
 

            
       |
58 | | ixpfn 7546 |
. . . . . . 7
           
    
            |
59 | 57, 58 | syl 17 |
. . . . . 6
 

              |
60 | | dffn5 5924 |
. . . . . 6
                                       |
61 | 59, 60 | sylib 201 |
. . . . 5
 

                              |
62 | 61 | mpteq2dva 4482 |
. . . 4
                                     |
63 | 8, 62 | syl5eq 2517 |
. . 3
                       |
64 | | ptunhmeo.j |
. . . 4
     |
65 | | pttop 20674 |
. . . . . . . 8
  
              |
66 | 19, 21, 65 | syl2anc 673 |
. . . . . . 7
         |
67 | 22, 66 | syl5eqel 2553 |
. . . . . 6
   |
68 | 26 | toptopon 20025 |
. . . . . 6

TopOn    |
69 | 67, 68 | sylib 201 |
. . . . 5
 TopOn    |
70 | | pttop 20674 |
. . . . . . . 8
  
              |
71 | 44, 45, 70 | syl2anc 673 |
. . . . . . 7
         |
72 | 46, 71 | syl5eqel 2553 |
. . . . . 6
   |
73 | 50 | toptopon 20025 |
. . . . . 6

TopOn    |
74 | 72, 73 | sylib 201 |
. . . . 5
 TopOn    |
75 | | txtopon 20683 |
. . . . 5
  TopOn  TopOn  
  TopOn      |
76 | 69, 74, 75 | syl2anc 673 |
. . . 4
   TopOn 
    |
77 | 17 | eleq2d 2534 |
. . . . . . 7
       |
78 | 77 | biimpa 492 |
. . . . . 6
 
     |
79 | | elun 3565 |
. . . . . 6
  

   |
80 | 78, 79 | sylib 201 |
. . . . 5
 
 
   |
81 | | ixpfn 7546 |
. . . . . . . . . . 11
          
      |
82 | 29, 81 | syl 17 |
. . . . . . . . . 10
 

        |
83 | 82 | adantlr 729 |
. . . . . . . . 9
             |
84 | 51 | adantr 472 |
. . . . . . . . . . . 12
 

  
       |
85 | 31, 84 | eleqtrrd 2552 |
. . . . . . . . . . 11
 

      
       |
86 | | ixpfn 7546 |
. . . . . . . . . . 11
          
      |
87 | 85, 86 | syl 17 |
. . . . . . . . . 10
 

        |
88 | 87 | adantlr 729 |
. . . . . . . . 9
             |
89 | 33 | ad2antrr 740 |
. . . . . . . . 9
           |
90 | | simplr 770 |
. . . . . . . . 9
         |
91 | | fvun1 5951 |
. . . . . . . . 9
                                       |
92 | 83, 88, 89, 90, 91 | syl112anc 1296 |
. . . . . . . 8
                               |
93 | 92 | mpteq2dva 4482 |
. . . . . . 7
 
                                 |
94 | 76 | adantr 472 |
. . . . . . . 8
 
   TopOn      |
95 | 4 | mpt2mpt 6407 |
. . . . . . . . 9
         
  |
96 | 69 | adantr 472 |
. . . . . . . . . 10
 
 TopOn    |
97 | 74 | adantr 472 |
. . . . . . . . . 10
 
 TopOn    |
98 | 96, 97 | cnmpt1st 20760 |
. . . . . . . . 9
 
          |
99 | 95, 98 | syl5eqel 2553 |
. . . . . . . 8
 
               |
100 | 19 | adantr 472 |
. . . . . . . . . 10
 
   |
101 | 21 | adantr 472 |
. . . . . . . . . 10
 
         |
102 | | simpr 468 |
. . . . . . . . . 10
 
   |
103 | 26, 22 | ptpjcn 20703 |
. . . . . . . . . 10
  
    
         
       |
104 | 100, 101,
102, 103 | syl3anc 1292 |
. . . . . . . . 9
 
                 |
105 | | fvres 5893 |
. . . . . . . . . . 11
             |
106 | 105 | adantl 473 |
. . . . . . . . . 10
 
             |
107 | 106 | oveq2d 6324 |
. . . . . . . . 9
 
                 |
108 | 104, 107 | eleqtrd 2551 |
. . . . . . . 8
 
               |
109 | | fveq1 5878 |
. . . . . . . 8
    
              |
110 | 94, 99, 96, 108, 109 | cnmpt11 20755 |
. . . . . . 7
 
                       |
111 | 93, 110 | eqeltrd 2549 |
. . . . . 6
 
                             |
112 | 82 | adantlr 729 |
. . . . . . . . 9
             |
113 | 87 | adantlr 729 |
. . . . . . . . 9
             |
114 | 33 | ad2antrr 740 |
. . . . . . . . 9
           |
115 | | simplr 770 |
. . . . . . . . 9
         |
116 | | fvun2 5952 |
. . . . . . . . 9
                                       |
117 | 112, 113,
114, 115, 116 | syl112anc 1296 |
. . . . . . . 8
                               |
118 | 117 | mpteq2dva 4482 |
. . . . . . 7
 
                                 |
119 | 76 | adantr 472 |
. . . . . . . 8
 
   TopOn      |
120 | 5 | mpt2mpt 6407 |
. . . . . . . . 9
         
  |
121 | 69 | adantr 472 |
. . . . . . . . . 10
 
 TopOn    |
122 | 74 | adantr 472 |
. . . . . . . . . 10
 
 TopOn    |
123 | 121, 122 | cnmpt2nd 20761 |
. . . . . . . . 9
 
          |
124 | 120, 123 | syl5eqel 2553 |
. . . . . . . 8
 
               |
125 | 44 | adantr 472 |
. . . . . . . . . 10
 
   |
126 | 45 | adantr 472 |
. . . . . . . . . 10
 
         |
127 | | simpr 468 |
. . . . . . . . . 10
 
   |
128 | 50, 46 | ptpjcn 20703 |
. . . . . . . . . 10
  
    
         
       |
129 | 125, 126,
127, 128 | syl3anc 1292 |
. . . . . . . . 9
 
                 |
130 | | fvres 5893 |
. . . . . . . . . . 11
             |
131 | 130 | adantl 473 |
. . . . . . . . . 10
 
             |
132 | 131 | oveq2d 6324 |
. . . . . . . . 9
 
                 |
133 | 129, 132 | eleqtrd 2551 |
. . . . . . . 8
 
               |
134 | | fveq1 5878 |
. . . . . . . 8
    
              |
135 | 119, 124,
122, 133, 134 | cnmpt11 20755 |
. . . . . . 7
 
                       |
136 | 118, 135 | eqeltrd 2549 |
. . . . . 6
 
                             |
137 | 111, 136 | jaodan 802 |
. . . . 5
 

                              |
138 | 80, 137 | syldan 478 |
. . . 4
 
                             |
139 | 64, 76, 15, 20, 138 | ptcn 20719 |
. . 3
                           |
140 | 63, 139 | eqeltrd 2549 |
. 2
       |
141 | 26, 50, 64, 22, 46, 1, 15, 20, 17, 33 | ptuncnv 20899 |
. . 3
 
            |
142 | | pttop 20674 |
. . . . . . 7
             |
143 | 15, 20, 142 | syl2anc 673 |
. . . . . 6
       |
144 | 64, 143 | syl5eqel 2553 |
. . . . 5
   |
145 | | eqid 2471 |
. . . . . 6
   |
146 | 145 | toptopon 20025 |
. . . . 5

TopOn     |
147 | 144, 146 | sylib 201 |
. . . 4
 TopOn     |
148 | 145, 64, 22 | ptrescn 20731 |
. . . . 5
                |
149 | 15, 20, 18, 148 | syl3anc 1292 |
. . . 4
          |
150 | 145, 64, 46 | ptrescn 20731 |
. . . . 5
                |
151 | 15, 20, 43, 150 | syl3anc 1292 |
. . . 4
          |
152 | 147, 149,
151 | cnmpt1t 20757 |
. . 3
       
         |
153 | 141, 152 | eqeltrd 2549 |
. 2
 
      |
154 | | ishmeo 20851 |
. 2
           
        |
155 | 140, 153,
154 | sylanbrc 677 |
1
         |