Step | Hyp | Ref
| Expression |
1 | | catcxpccl.o |
. . . . 5
c |
2 | | eqid 2622 |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
|
4 | | eqid 2622 |
. . . . 5
|
5 | | eqid 2622 |
. . . . 5
|
6 | | eqid 2622 |
. . . . 5
comp comp |
7 | | eqid 2622 |
. . . . 5
comp comp |
8 | | catcxpccl.x |
. . . . 5
|
9 | | catcxpccl.y |
. . . . 5
|
10 | | eqidd 2623 |
. . . . 5
|
11 | 1, 2, 3 | xpcbas 16818 |
. . . . . . 7
|
12 | | eqid 2622 |
. . . . . . 7
|
13 | 1, 11, 4, 5, 12 | xpchomfval 16819 |
. . . . . 6
|
14 | 13 | a1i 11 |
. . . . 5
|
15 | | eqidd 2623 |
. . . . 5
comp comp comp comp |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
14, 15 | xpcval 16817 |
. . . 4
comp comp comp |
17 | | catcxpccl.u |
. . . . 5
WUni |
18 | | df-base 15863 |
. . . . . . 7
Slot |
19 | | catcxpccl.1 |
. . . . . . . 8
|
20 | 17, 19 | wunndx 15878 |
. . . . . . 7
|
21 | 18, 17, 20 | wunstr 15881 |
. . . . . 6
|
22 | | inss1 3833 |
. . . . . . . . 9
|
23 | | catcxpccl.c |
. . . . . . . . . . 11
CatCat |
24 | | catcxpccl.b |
. . . . . . . . . . 11
|
25 | 23, 24, 17 | catcbas 16747 |
. . . . . . . . . 10
|
26 | 8, 25 | eleqtrd 2703 |
. . . . . . . . 9
|
27 | 22, 26 | sseldi 3601 |
. . . . . . . 8
|
28 | 18, 17, 27 | wunstr 15881 |
. . . . . . 7
|
29 | 9, 25 | eleqtrd 2703 |
. . . . . . . . 9
|
30 | 22, 29 | sseldi 3601 |
. . . . . . . 8
|
31 | 18, 17, 30 | wunstr 15881 |
. . . . . . 7
|
32 | 17, 28, 31 | wunxp 9546 |
. . . . . 6
|
33 | 17, 21, 32 | wunop 9544 |
. . . . 5
|
34 | | df-hom 15966 |
. . . . . . 7
Slot ; |
35 | 34, 17, 20 | wunstr 15881 |
. . . . . 6
|
36 | 17, 32, 32 | wunxp 9546 |
. . . . . . . 8
|
37 | 34, 17, 27 | wunstr 15881 |
. . . . . . . . . . . 12
|
38 | 17, 37 | wunrn 9551 |
. . . . . . . . . . 11
|
39 | 17, 38 | wununi 9528 |
. . . . . . . . . 10
|
40 | 34, 17, 30 | wunstr 15881 |
. . . . . . . . . . . 12
|
41 | 17, 40 | wunrn 9551 |
. . . . . . . . . . 11
|
42 | 17, 41 | wununi 9528 |
. . . . . . . . . 10
|
43 | 17, 39, 42 | wunxp 9546 |
. . . . . . . . 9
|
44 | 17, 43 | wunpw 9529 |
. . . . . . . 8
|
45 | | ovssunirn 6681 |
. . . . . . . . . . . . 13
|
46 | | ovssunirn 6681 |
. . . . . . . . . . . . 13
|
47 | | xpss12 5225 |
. . . . . . . . . . . . 13
|
48 | 45, 46, 47 | mp2an 708 |
. . . . . . . . . . . 12
|
49 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
50 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
51 | 49, 50 | xpex 6962 |
. . . . . . . . . . . . 13
|
52 | 51 | elpw 4164 |
. . . . . . . . . . . 12
|
53 | 48, 52 | mpbir 221 |
. . . . . . . . . . 11
|
54 | 53 | rgen2w 2925 |
. . . . . . . . . 10
|
55 | | eqid 2622 |
. . . . . . . . . . 11
|
56 | 55 | fmpt2 7237 |
. . . . . . . . . 10
|
57 | 54, 56 | mpbi 220 |
. . . . . . . . 9
|
58 | 57 | a1i 11 |
. . . . . . . 8
|
59 | 17, 36, 44, 58 | wunf 9549 |
. . . . . . 7
|
60 | 13, 59 | syl5eqel 2705 |
. . . . . 6
|
61 | 17, 35, 60 | wunop 9544 |
. . . . 5
|
62 | | df-cco 15967 |
. . . . . . 7
comp Slot ; |
63 | 62, 17, 20 | wunstr 15881 |
. . . . . 6
comp |
64 | 17, 36, 32 | wunxp 9546 |
. . . . . . 7
|
65 | 62, 17, 27 | wunstr 15881 |
. . . . . . . . . . . . . 14
comp |
66 | 17, 65 | wunrn 9551 |
. . . . . . . . . . . . 13
comp |
67 | 17, 66 | wununi 9528 |
. . . . . . . . . . . 12
comp |
68 | 17, 67 | wunrn 9551 |
. . . . . . . . . . 11
comp |
69 | 17, 68 | wununi 9528 |
. . . . . . . . . 10
comp |
70 | 17, 69 | wunpw 9529 |
. . . . . . . . 9
comp |
71 | 62, 17, 30 | wunstr 15881 |
. . . . . . . . . . . . . 14
comp |
72 | 17, 71 | wunrn 9551 |
. . . . . . . . . . . . 13
comp |
73 | 17, 72 | wununi 9528 |
. . . . . . . . . . . 12
comp |
74 | 17, 73 | wunrn 9551 |
. . . . . . . . . . 11
comp |
75 | 17, 74 | wununi 9528 |
. . . . . . . . . 10
comp |
76 | 17, 75 | wunpw 9529 |
. . . . . . . . 9
comp |
77 | 17, 70, 76 | wunxp 9546 |
. . . . . . . 8
comp comp |
78 | 17, 60 | wunrn 9551 |
. . . . . . . . . 10
|
79 | 17, 78 | wununi 9528 |
. . . . . . . . 9
|
80 | 17, 79, 79 | wunxp 9546 |
. . . . . . . 8
|
81 | 17, 77, 80 | wunpm 9547 |
. . . . . . 7
comp comp |
82 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
comp |
83 | 82 | rnex 7100 |
. . . . . . . . . . . . . . . 16
comp |
84 | 83 | uniex 6953 |
. . . . . . . . . . . . . . 15
comp |
85 | 84 | rnex 7100 |
. . . . . . . . . . . . . 14
comp |
86 | 85 | uniex 6953 |
. . . . . . . . . . . . 13
comp |
87 | 86 | pwex 4848 |
. . . . . . . . . . . 12
comp |
88 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
comp |
89 | 88 | rnex 7100 |
. . . . . . . . . . . . . . . 16
comp |
90 | 89 | uniex 6953 |
. . . . . . . . . . . . . . 15
comp |
91 | 90 | rnex 7100 |
. . . . . . . . . . . . . 14
comp |
92 | 91 | uniex 6953 |
. . . . . . . . . . . . 13
comp |
93 | 92 | pwex 4848 |
. . . . . . . . . . . 12
comp |
94 | 87, 93 | xpex 6962 |
. . . . . . . . . . 11
comp comp |
95 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
96 | 95 | rnex 7100 |
. . . . . . . . . . . . 13
|
97 | 96 | uniex 6953 |
. . . . . . . . . . . 12
|
98 | 97, 97 | xpex 6962 |
. . . . . . . . . . 11
|
99 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . 16
comp comp |
100 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . 17
comp comp |
101 | | rnss 5354 |
. . . . . . . . . . . . . . . . 17
comp comp comp comp |
102 | | uniss 4458 |
. . . . . . . . . . . . . . . . 17
comp comp comp comp |
103 | 100, 101,
102 | mp2b 10 |
. . . . . . . . . . . . . . . 16
comp comp |
104 | 99, 103 | sstri 3612 |
. . . . . . . . . . . . . . 15
comp comp |
105 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
comp |
106 | 105 | elpw 4164 |
. . . . . . . . . . . . . . 15
comp comp
comp comp |
107 | 104, 106 | mpbir 221 |
. . . . . . . . . . . . . 14
comp comp |
108 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . 16
comp comp |
109 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . 17
comp comp |
110 | | rnss 5354 |
. . . . . . . . . . . . . . . . 17
comp comp comp comp |
111 | | uniss 4458 |
. . . . . . . . . . . . . . . . 17
comp comp comp comp |
112 | 109, 110,
111 | mp2b 10 |
. . . . . . . . . . . . . . . 16
comp comp |
113 | 108, 112 | sstri 3612 |
. . . . . . . . . . . . . . 15
comp comp |
114 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
comp |
115 | 114 | elpw 4164 |
. . . . . . . . . . . . . . 15
comp comp
comp comp |
116 | 113, 115 | mpbir 221 |
. . . . . . . . . . . . . 14
comp comp |
117 | | opelxpi 5148 |
. . . . . . . . . . . . . 14
comp comp comp comp comp comp comp comp |
118 | 107, 116,
117 | mp2an 708 |
. . . . . . . . . . . . 13
comp comp comp comp |
119 | 118 | rgen2w 2925 |
. . . . . . . . . . . 12
comp comp comp comp |
120 | | eqid 2622 |
. . . . . . . . . . . . 13
comp comp comp comp |
121 | 120 | fmpt2 7237 |
. . . . . . . . . . . 12
comp comp comp comp comp comp comp comp |
122 | 119, 121 | mpbi 220 |
. . . . . . . . . . 11
comp comp comp comp |
123 | | ovssunirn 6681 |
. . . . . . . . . . . 12
|
124 | | fvssunirn 6217 |
. . . . . . . . . . . 12
|
125 | | xpss12 5225 |
. . . . . . . . . . . 12
|
126 | 123, 124,
125 | mp2an 708 |
. . . . . . . . . . 11
|
127 | | elpm2r 7875 |
. . . . . . . . . . 11
comp comp
comp comp comp comp comp comp comp comp
|
128 | 94, 98, 122, 126, 127 | mp4an 709 |
. . . . . . . . . 10
comp comp comp comp
|
129 | 128 | rgen2w 2925 |
. . . . . . . . 9
comp comp comp comp
|
130 | | eqid 2622 |
. . . . . . . . . 10
comp comp comp comp |
131 | 130 | fmpt2 7237 |
. . . . . . . . 9
comp comp comp comp
comp comp comp comp
|
132 | 129, 131 | mpbi 220 |
. . . . . . . 8
comp comp comp comp
|
133 | 132 | a1i 11 |
. . . . . . 7
comp comp comp comp
|
134 | 17, 64, 81, 133 | wunf 9549 |
. . . . . 6
comp comp |
135 | 17, 63, 134 | wunop 9544 |
. . . . 5
comp comp comp |
136 | 17, 33, 61, 135 | wuntp 9533 |
. . . 4
comp comp comp |
137 | 16, 136 | eqeltrd 2701 |
. . 3
|
138 | | inss2 3834 |
. . . . 5
|
139 | 138, 26 | sseldi 3601 |
. . . 4
|
140 | 138, 29 | sseldi 3601 |
. . . 4
|
141 | 1, 139, 140 | xpccat 16830 |
. . 3
|
142 | 137, 141 | elind 3798 |
. 2
|
143 | 142, 25 | eleqtrrd 2704 |
1
|