Step | Hyp | Ref
| Expression |
1 | | catcoppccl.3 |
. . . . 5
   |
2 | | eqid 2462 |
. . . . . 6
         |
3 | | eqid 2462 |
. . . . . 6
       |
4 | | eqid 2462 |
. . . . . 6
comp  comp   |
5 | | catcoppccl.o |
. . . . . 6
oppCat   |
6 | 2, 3, 4, 5 | oppcval 15667 |
. . . . 5
   sSet     
tpos      sSet  comp                   tpos          comp             |
7 | 1, 6 | syl 17 |
. . . 4
   sSet     
tpos      sSet  comp                   tpos          comp             |
8 | | catcoppccl.1 |
. . . . 5
 WUni |
9 | | inss1 3664 |
. . . . . . 7
   |
10 | | catcoppccl.c |
. . . . . . . . 9
CatCat   |
11 | | catcoppccl.b |
. . . . . . . . 9
     |
12 | 10, 11, 8 | catcbas 16041 |
. . . . . . . 8
     |
13 | 1, 12 | eleqtrd 2542 |
. . . . . . 7
     |
14 | 9, 13 | sseldi 3442 |
. . . . . 6
   |
15 | | df-hom 15263 |
. . . . . . . 8
Slot ;  |
16 | | catcoppccl.2 |
. . . . . . . . 9
   |
17 | 8, 16 | wunndx 15186 |
. . . . . . . 8
   |
18 | 15, 8, 17 | wunstr 15189 |
. . . . . . 7
   
  |
19 | 15, 8, 14 | wunstr 15189 |
. . . . . . . 8
      |
20 | 8, 19 | wuntpos 9185 |
. . . . . . 7
 tpos      |
21 | 8, 18, 20 | wunop 9173 |
. . . . . 6
     
tpos       |
22 | 8, 14, 21 | wunsets 15199 |
. . . . 5
  sSet      tpos        |
23 | | df-cco 15264 |
. . . . . . 7
comp Slot ;  |
24 | 23, 8, 17 | wunstr 15189 |
. . . . . 6
 comp    |
25 | | df-base 15175 |
. . . . . . . . . 10
Slot  |
26 | 25, 8, 14 | wunstr 15189 |
. . . . . . . . 9
       |
27 | 8, 26, 26 | wunxp 9175 |
. . . . . . . 8
             |
28 | 8, 27, 26 | wunxp 9175 |
. . . . . . 7
                   |
29 | 23, 8, 14 | wunstr 15189 |
. . . . . . . . . . . . . 14
 comp    |
30 | 8, 29 | wunrn 9180 |
. . . . . . . . . . . . 13
 comp    |
31 | 8, 30 | wununi 9157 |
. . . . . . . . . . . 12
  comp    |
32 | 8, 31 | wundm 9179 |
. . . . . . . . . . 11
  comp    |
33 | 8, 32 | wuncnv 9181 |
. . . . . . . . . 10
   comp    |
34 | 8 | wun0 9169 |
. . . . . . . . . . 11

  |
35 | 8, 34 | wunsn 9167 |
. . . . . . . . . 10
     |
36 | 8, 33, 35 | wunun 9161 |
. . . . . . . . 9
    comp       |
37 | 8, 31 | wunrn 9180 |
. . . . . . . . 9
  comp    |
38 | 8, 36, 37 | wunxp 9175 |
. . . . . . . 8
     comp      comp     |
39 | 8, 38 | wunpw 9158 |
. . . . . . 7
      comp      comp     |
40 | | tposssxp 7003 |
. . . . . . . . . . . 12
tpos          comp                    comp                    comp          |
41 | | ovssunirn 6344 |
. . . . . . . . . . . . . . 15
         comp         comp   |
42 | | dmss 5053 |
. . . . . . . . . . . . . . 15
          comp         comp           comp         comp    |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . 14
         comp         comp   |
44 | | cnvss 5026 |
. . . . . . . . . . . . . 14
          comp         comp            comp          comp    |
45 | | unss1 3615 |
. . . . . . . . . . . . . 14
           comp          comp             comp              comp       |
46 | 43, 44, 45 | mp2b 10 |
. . . . . . . . . . . . 13
           comp              comp      |
47 | | rnss 5082 |
. . . . . . . . . . . . . 14
          comp         comp           comp         comp    |
48 | 41, 47 | ax-mp 5 |
. . . . . . . . . . . . 13
         comp         comp   |
49 | | xpss12 4959 |
. . . . . . . . . . . . 13
             comp              comp              comp         comp  
            comp                    comp             comp      comp     |
50 | 46, 48, 49 | mp2an 683 |
. . . . . . . . . . . 12
            comp                    comp             comp      comp    |
51 | 40, 50 | sstri 3453 |
. . . . . . . . . . 11
tpos          comp            comp      comp    |
52 | | elpw2g 4580 |
. . . . . . . . . . . 12
     comp      comp  
tpos          comp             comp      comp   tpos          comp            comp      comp      |
53 | 38, 52 | syl 17 |
. . . . . . . . . . 11
 tpos          comp             comp      comp  
tpos          comp            comp      comp      |
54 | 51, 53 | mpbiri 241 |
. . . . . . . . . 10
 tpos          comp             comp      comp     |
55 | 54 | ralrimivw 2815 |
. . . . . . . . 9
      tpos          comp             comp      comp     |
56 | 55 | ralrimivw 2815 |
. . . . . . . 8
             
    tpos          comp             comp      comp     |
57 | | eqid 2462 |
. . . . . . . . 9
                tpos          comp                         tpos          comp          |
58 | 57 | fmpt2 6887 |
. . . . . . . 8
 
                tpos          comp             comp      comp  
                tpos          comp                                  comp      comp     |
59 | 56, 58 | sylib 201 |
. . . . . . 7
                 tpos          comp                                  comp      comp     |
60 | 8, 28, 39, 59 | wunf 9178 |
. . . . . 6
                 tpos          comp           |
61 | 8, 24, 60 | wunop 9173 |
. . . . 5
  comp                   tpos          comp            |
62 | 8, 22, 61 | wunsets 15199 |
. . . 4
   sSet      tpos      sSet  comp                   tpos          comp             |
63 | 7, 62 | eqeltrd 2540 |
. . 3
   |
64 | | inss2 3665 |
. . . . 5
   |
65 | 64, 13 | sseldi 3442 |
. . . 4
   |
66 | 5 | oppccat 15676 |
. . . 4
   |
67 | 65, 66 | syl 17 |
. . 3
   |
68 | 63, 67 | elind 3630 |
. 2
     |
69 | 68, 12 | eleqtrrd 2543 |
1
   |