Step | Hyp | Ref
| Expression |
1 | | xpccat.t |
. . . . 5
 c   |
2 | | xpccat.x |
. . . . 5
     |
3 | | xpccat.y |
. . . . 5
     |
4 | 1, 2, 3 | xpcbas 15102 |
. . . 4
       |
5 | 4 | a1i 11 |
. . 3
         |
6 | | eqidd 2453 |
. . 3
         |
7 | | eqidd 2453 |
. . 3
 comp  comp    |
8 | | ovex 6220 |
. . . . 5
 c   |
9 | 1, 8 | eqeltri 2536 |
. . . 4
 |
10 | 9 | a1i 11 |
. . 3
   |
11 | | biid 236 |
. . 3
                     
  
            
   
   
 
          
  
               |
12 | | eqid 2452 |
. . . . . 6
       |
13 | | xpccat.i |
. . . . . 6
     |
14 | | xpccat.c |
. . . . . . 7
   |
15 | 14 | adantr 465 |
. . . . . 6
 

    |
16 | | xp1st 6711 |
. . . . . . 7
         |
17 | 16 | adantl 466 |
. . . . . 6
 

        |
18 | 2, 12, 13, 15, 17 | catidcl 14734 |
. . . . 5
 

                           |
19 | | eqid 2452 |
. . . . . 6
       |
20 | | xpccat.j |
. . . . . 6
     |
21 | | xpccat.d |
. . . . . . 7
   |
22 | 21 | adantr 465 |
. . . . . 6
 

    |
23 | | xp2nd 6712 |
. . . . . . 7
         |
24 | 23 | adantl 466 |
. . . . . 6
 

        |
25 | 3, 19, 20, 22, 24 | catidcl 14734 |
. . . . 5
 

                           |
26 | | opelxpi 4974 |
. . . . 5
                                                                   
                                  |
27 | 18, 25, 26 | syl2anc 661 |
. . . 4
 

                                                       |
28 | | eqid 2452 |
. . . . 5
       |
29 | | simpr 461 |
. . . . 5
 

      |
30 | 1, 4, 12, 19, 28, 29, 29 | xpchom 15104 |
. . . 4
 

                                           |
31 | 27, 30 | eleqtrrd 2543 |
. . 3
 

                              |
32 | | fvex 5804 |
. . . . . . . 8
         |
33 | | fvex 5804 |
. . . . . . . 8
         |
34 | 32, 33 | op1st 6690 |
. . . . . . 7
                                |
35 | 34 | oveq1i 6205 |
. . . . . 6
                                      comp                                     comp               |
36 | 14 | adantr 465 |
. . . . . . 7
 
   
   
 
          
  
             
  |
37 | | simpr1l 1045 |
. . . . . . . 8
 
   
   
 
          
  
                  |
38 | | xp1st 6711 |
. . . . . . . 8
         |
39 | 37, 38 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
40 | | eqid 2452 |
. . . . . . 7
comp  comp   |
41 | | simpr1r 1046 |
. . . . . . . 8
 
   
   
 
          
  
                  |
42 | 41, 16 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
43 | | simpr31 1078 |
. . . . . . . . 9
 
   
   
 
          
  
                       |
44 | 1, 4, 12, 19, 28, 37, 41 | xpchom 15104 |
. . . . . . . . 9
 
   
   
 
          
  
                                                       |
45 | 43, 44 | eleqtrd 2542 |
. . . . . . . 8
 
   
   
 
          
  
                                                |
46 | | xp1st 6711 |
. . . . . . . 8
                                                      |
47 | 45, 46 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
48 | 2, 12, 13, 36, 39, 40, 42, 47 | catlid 14735 |
. . . . . 6
 
   
   
 
          
  
                                     comp                    |
49 | 35, 48 | syl5eq 2505 |
. . . . 5
 
   
   
 
          
  
                                                    comp                    |
50 | 32, 33 | op2nd 6691 |
. . . . . . 7
                                |
51 | 50 | oveq1i 6205 |
. . . . . 6
                                      comp                                     comp               |
52 | 21 | adantr 465 |
. . . . . . 7
 
   
   
 
          
  
             
  |
53 | | xp2nd 6712 |
. . . . . . . 8
         |
54 | 37, 53 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
55 | | eqid 2452 |
. . . . . . 7
comp  comp   |
56 | 41, 23 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
57 | | xp2nd 6712 |
. . . . . . . 8
                                                      |
58 | 45, 57 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
59 | 3, 19, 20, 52, 54, 55, 56, 58 | catlid 14735 |
. . . . . 6
 
   
   
 
          
  
                                     comp                    |
60 | 51, 59 | syl5eq 2505 |
. . . . 5
 
   
   
 
          
  
                                                    comp                    |
61 | 49, 60 | opeq12d 4170 |
. . . 4
 
   
   
 
          
  
                                                     comp                                                     comp                            |
62 | | eqid 2452 |
. . . . 5
comp  comp   |
63 | 41, 31 | syldan 470 |
. . . . 5
 
   
   
 
          
  
                                
         |
64 | 1, 4, 28, 40, 55, 62, 37, 41, 41, 43, 63 | xpcco 15107 |
. . . 4
 
   
   
 
          
  
                                        comp                                             comp                                                     comp                 |
65 | | 1st2nd2 6718 |
. . . . 5
                                              |
66 | 45, 65 | syl 16 |
. . . 4
 
   
   
 
          
  
                           |
67 | 61, 64, 66 | 3eqtr4d 2503 |
. . 3
 
   
   
 
          
  
                                        comp        |
68 | 34 | oveq2i 6206 |
. . . . . 6
                   comp                                                    comp                   |
69 | | simpr2l 1047 |
. . . . . . . 8
 
   
   
 
          
  
             
    |
70 | | xp1st 6711 |
. . . . . . . 8
         |
71 | 69, 70 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
72 | | simpr32 1079 |
. . . . . . . . 9
 
   
   
 
          
  
                       |
73 | 1, 4, 12, 19, 28, 41, 69 | xpchom 15104 |
. . . . . . . . 9
 
   
   
 
          
  
                                                       |
74 | 72, 73 | eleqtrd 2542 |
. . . . . . . 8
 
   
   
 
          
  
                                                |
75 | | xp1st 6711 |
. . . . . . . 8
                                                      |
76 | 74, 75 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
77 | 2, 12, 13, 36, 42, 40, 71, 76 | catrid 14736 |
. . . . . 6
 
   
   
 
          
  
                                 comp                        |
78 | 68, 77 | syl5eq 2505 |
. . . . 5
 
   
   
 
          
  
                                 comp                                       |
79 | 50 | oveq2i 6206 |
. . . . . 6
                   comp                                                    comp                   |
80 | | xp2nd 6712 |
. . . . . . . 8
         |
81 | 69, 80 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
82 | | xp2nd 6712 |
. . . . . . . 8
                                                      |
83 | 74, 82 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
84 | 3, 19, 20, 52, 56, 55, 81, 83 | catrid 14736 |
. . . . . 6
 
   
   
 
          
  
                                 comp                        |
85 | 79, 84 | syl5eq 2505 |
. . . . 5
 
   
   
 
          
  
                                 comp                                       |
86 | 78, 85 | opeq12d 4170 |
. . . 4
 
   
   
 
          
  
                                  comp                                                     comp                                               |
87 | 1, 4, 28, 40, 55, 62, 41, 41, 69, 63, 72 | xpcco 15107 |
. . . 4
 
   
   
 
          
  
                     comp                        
                    comp                                                     comp                                    |
88 | | 1st2nd2 6718 |
. . . . 5
                                              |
89 | 74, 88 | syl 16 |
. . . 4
 
   
   
 
          
  
                           |
90 | 86, 87, 89 | 3eqtr4d 2503 |
. . 3
 
   
   
 
          
  
                     comp                        
  |
91 | 2, 12, 40, 36, 39, 42, 71, 47, 76 | catcocl 14737 |
. . . . 5
 
   
   
 
          
  
                                 comp                               |
92 | 3, 19, 55, 52, 54, 56, 81, 58, 83 | catcocl 14737 |
. . . . 5
 
   
   
 
          
  
                                 comp                               |
93 | | opelxpi 4974 |
. . . . 5
                     comp                                                comp                                                  comp                                  comp                                                 |
94 | 91, 92, 93 | syl2anc 661 |
. . . 4
 
   
   
 
          
  
                                  comp                                  comp                                                 |
95 | 1, 4, 28, 40, 55, 62, 37, 41, 69, 43, 72 | xpcco 15107 |
. . . 4
 
   
   
 
          
  
                     comp                          comp                                  comp                 |
96 | 1, 4, 12, 19, 28, 37, 69 | xpchom 15104 |
. . . 4
 
   
   
 
          
  
                                                       |
97 | 94, 95, 96 | 3eltr4d 2555 |
. . 3
 
   
   
 
          
  
                     comp               |
98 | | simpr2r 1048 |
. . . . . . . 8
 
   
   
 
          
  
                  |
99 | | xp1st 6711 |
. . . . . . . 8
         |
100 | 98, 99 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
101 | | simpr33 1080 |
. . . . . . . . 9
 
   
   
 
          
  
             
  
      |
102 | 1, 4, 12, 19, 28, 69, 98 | xpchom 15104 |
. . . . . . . . 9
 
   
   
 
          
  
                                                       |
103 | 101, 102 | eleqtrd 2542 |
. . . . . . . 8
 
   
   
 
          
  
             
                                  |
104 | | xp1st 6711 |
. . . . . . . 8
                                                      |
105 | 103, 104 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
106 | 2, 12, 40, 36, 39, 42, 71, 47, 76, 100, 105 | catass 14738 |
. . . . . 6
 
   
   
 
          
  
                                  comp                            comp                                 comp                            comp                 |
107 | 1, 4, 28, 40, 55, 62, 41, 69, 98, 72, 101 | xpcco 15107 |
. . . . . . . . 9
 
   
   
 
          
  
                     comp                          comp                                  comp                 |
108 | 107 | fveq2d 5798 |
. . . . . . . 8
 
   
   
 
          
  
                        comp                              comp                                  comp                  |
109 | | ovex 6220 |
. . . . . . . . 9
                   comp               |
110 | | ovex 6220 |
. . . . . . . . 9
                   comp               |
111 | 109, 110 | op1st 6690 |
. . . . . . . 8
                       comp                                  comp                                   comp               |
112 | 108, 111 | syl6eq 2509 |
. . . . . . 7
 
   
   
 
          
  
                        comp                          comp                |
113 | 112 | oveq1d 6210 |
. . . . . 6
 
   
   
 
          
  
                         comp                     comp                                  comp                            comp                |
114 | 95 | fveq2d 5798 |
. . . . . . . 8
 
   
   
 
          
  
                        comp                              comp                                  comp                  |
115 | | ovex 6220 |
. . . . . . . . 9
                   comp               |
116 | | ovex 6220 |
. . . . . . . . 9
                   comp               |
117 | 115, 116 | op1st 6690 |
. . . . . . . 8
                       comp                                  comp                                   comp               |
118 | 114, 117 | syl6eq 2509 |
. . . . . . 7
 
   
   
 
          
  
                        comp                          comp                |
119 | 118 | oveq2d 6211 |
. . . . . 6
 
   
   
 
          
  
                                 comp                   comp                           comp                            comp                 |
120 | 106, 113,
119 | 3eqtr4d 2503 |
. . . . 5
 
   
   
 
          
  
                         comp                     comp                                 comp                   comp          |
121 | | xp2nd 6712 |
. . . . . . . 8
         |
122 | 98, 121 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                    |
123 | | xp2nd 6712 |
. . . . . . . 8
                                                      |
124 | 103, 123 | syl 16 |
. . . . . . 7
 
   
   
 
          
  
                                   |
125 | 3, 19, 55, 52, 54, 56, 81, 58, 83, 122, 124 | catass 14738 |
. . . . . 6
 
   
   
 
          
  
                                  comp                            comp                                 comp                            comp                 |
126 | 107 | fveq2d 5798 |
. . . . . . . 8
 
   
   
 
          
  
                        comp                              comp                                  comp                  |
127 | 109, 110 | op2nd 6691 |
. . . . . . . 8
                       comp                                  comp                                   comp               |
128 | 126, 127 | syl6eq 2509 |
. . . . . . 7
 
   
   
 
          
  
                        comp                          comp                |
129 | 128 | oveq1d 6210 |
. . . . . 6
 
   
   
 
          
  
                         comp                     comp                                  comp                            comp                |
130 | 95 | fveq2d 5798 |
. . . . . . . 8
 
   
   
 
          
  
                        comp                              comp                                  comp                  |
131 | 115, 116 | op2nd 6691 |
. . . . . . . 8
                       comp                                  comp                                   comp               |
132 | 130, 131 | syl6eq 2509 |
. . . . . . 7
 
   
   
 
          
  
                        comp                          comp                |
133 | 132 | oveq2d 6211 |
. . . . . 6
 
   
   
 
          
  
                                 comp                   comp                           comp                            comp                 |
134 | 125, 129,
133 | 3eqtr4d 2503 |
. . . . 5
 
   
   
 
          
  
                         comp                     comp                                 comp                   comp          |
135 | 120, 134 | opeq12d 4170 |
. . . 4
 
   
   
 
          
  
                          comp                     comp                          comp                     comp                                   comp                   comp                            comp                   comp           |
136 | 2, 12, 40, 36, 42, 71, 100, 76, 105 | catcocl 14737 |
. . . . . . 7
 
   
   
 
          
  
                                 comp                               |
137 | 3, 19, 55, 52, 56, 81, 122, 83, 124 | catcocl 14737 |
. . . . . . 7
 
   
   
 
          
  
                                 comp                               |
138 | | opelxpi 4974 |
. . . . . . 7
                     comp                                                comp                                                  comp                                  comp                                                 |
139 | 136, 137,
138 | syl2anc 661 |
. . . . . 6
 
   
   
 
          
  
                                  comp                                  comp                                                 |
140 | 1, 4, 12, 19, 28, 41, 98 | xpchom 15104 |
. . . . . 6
 
   
   
 
          
  
                                                       |
141 | 139, 107,
140 | 3eltr4d 2555 |
. . . . 5
 
   
   
 
          
  
                     comp               |
142 | 1, 4, 28, 40, 55, 62, 37, 41, 98, 43, 141 | xpcco 15107 |
. . . 4
 
   
   
 
          
  
                      comp            comp                  comp                     comp                          comp                     comp                 |
143 | 1, 4, 28, 40, 55, 62, 37, 69, 98, 97, 101 | xpcco 15107 |
. . . 4
 
   
   
 
          
  
                     comp            comp                           comp                   comp                            comp                   comp           |
144 | 135, 142,
143 | 3eqtr4d 2503 |
. . 3
 
   
   
 
          
  
                      comp            comp             comp            comp         |
145 | 5, 6, 7, 10, 11, 31, 67, 90, 97, 144 | iscatd2 14733 |
. 2
                                |
146 | | vex 3075 |
. . . . . . . 8
 |
147 | | vex 3075 |
. . . . . . . 8
 |
148 | 146, 147 | op1std 6692 |
. . . . . . 7
          |
149 | 148 | fveq2d 5798 |
. . . . . 6
                  |
150 | 146, 147 | op2ndd 6693 |
. . . . . . 7
          |
151 | 150 | fveq2d 5798 |
. . . . . 6
                  |
152 | 149, 151 | opeq12d 4170 |
. . . . 5
                                    |
153 | 152 | mpt2mpt 6287 |
. . . 4
                      
               |
154 | 153 | eqeq2i 2470 |
. . 3
                                                |
155 | 154 | anbi2i 694 |
. 2
                              
                     |
156 | 145, 155 | sylib 196 |
1
                       |