Step | Hyp | Ref
| Expression |
1 | | catcfuccl.o |
. . . . 5
FuncCat
|
2 | | eqid 2622 |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
Nat Nat |
4 | | eqid 2622 |
. . . . 5
|
5 | | eqid 2622 |
. . . . 5
comp comp |
6 | | inss2 3834 |
. . . . . 6
|
7 | | catcfuccl.x |
. . . . . . 7
|
8 | | catcfuccl.c |
. . . . . . . 8
CatCat |
9 | | catcfuccl.b |
. . . . . . . 8
|
10 | | catcfuccl.u |
. . . . . . . 8
WUni |
11 | 8, 9, 10 | catcbas 16747 |
. . . . . . 7
|
12 | 7, 11 | eleqtrd 2703 |
. . . . . 6
|
13 | 6, 12 | sseldi 3601 |
. . . . 5
|
14 | | catcfuccl.y |
. . . . . . 7
|
15 | 14, 11 | eleqtrd 2703 |
. . . . . 6
|
16 | 6, 15 | sseldi 3601 |
. . . . 5
|
17 | | eqidd 2623 |
. . . . 5
Nat Nat comp Nat Nat comp |
18 | 1, 2, 3, 4, 5, 13,
16, 17 | fucval 16618 |
. . . 4
Nat
comp
Nat Nat comp |
19 | | df-base 15863 |
. . . . . . 7
Slot |
20 | | catcfuccl.1 |
. . . . . . . 8
|
21 | 10, 20 | wunndx 15878 |
. . . . . . 7
|
22 | 19, 10, 21 | wunstr 15881 |
. . . . . 6
|
23 | | inss1 3833 |
. . . . . . . 8
|
24 | 23, 12 | sseldi 3601 |
. . . . . . 7
|
25 | 23, 15 | sseldi 3601 |
. . . . . . 7
|
26 | 10, 24, 25 | wunfunc 16559 |
. . . . . 6
|
27 | 10, 22, 26 | wunop 9544 |
. . . . 5
|
28 | | df-hom 15966 |
. . . . . . 7
Slot ; |
29 | 28, 10, 21 | wunstr 15881 |
. . . . . 6
|
30 | 10, 24, 25 | wunnat 16616 |
. . . . . 6
Nat |
31 | 10, 29, 30 | wunop 9544 |
. . . . 5
Nat
|
32 | | df-cco 15967 |
. . . . . . 7
comp Slot ; |
33 | 32, 10, 21 | wunstr 15881 |
. . . . . 6
comp |
34 | 10, 26, 26 | wunxp 9546 |
. . . . . . . 8
|
35 | 10, 34, 26 | wunxp 9546 |
. . . . . . 7
|
36 | 32, 10, 25 | wunstr 15881 |
. . . . . . . . . . . . . 14
comp |
37 | 10, 36 | wunrn 9551 |
. . . . . . . . . . . . 13
comp |
38 | 10, 37 | wununi 9528 |
. . . . . . . . . . . 12
comp |
39 | 10, 38 | wunrn 9551 |
. . . . . . . . . . 11
comp |
40 | 10, 39 | wununi 9528 |
. . . . . . . . . 10
comp |
41 | 10, 40 | wunpw 9529 |
. . . . . . . . 9
comp |
42 | 19, 10, 24 | wunstr 15881 |
. . . . . . . . 9
|
43 | 10, 41, 42 | wunmap 9548 |
. . . . . . . 8
comp |
44 | 10, 30 | wunrn 9551 |
. . . . . . . . . 10
Nat |
45 | 10, 44 | wununi 9528 |
. . . . . . . . 9
Nat |
46 | 10, 45, 45 | wunxp 9546 |
. . . . . . . 8
Nat Nat |
47 | 10, 43, 46 | wunpm 9547 |
. . . . . . 7
comp
Nat Nat |
48 | | fvex 6201 |
. . . . . . . . . . 11
|
49 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
50 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
comp |
51 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
Nat |
52 | 51 | rnex 7100 |
. . . . . . . . . . . . . . . . . . 19
Nat |
53 | 52 | uniex 6953 |
. . . . . . . . . . . . . . . . . 18
Nat |
54 | 53, 53 | xpex 6962 |
. . . . . . . . . . . . . . . . 17
Nat Nat |
55 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
comp comp |
56 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . 24
comp comp |
57 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
comp comp |
58 | | rnss 5354 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
comp comp comp
comp |
59 | | uniss 4458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
comp
comp comp comp |
60 | 57, 58, 59 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
comp
comp |
61 | 56, 60 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . 23
comp comp |
62 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
comp |
63 | 62 | elpw 4164 |
. . . . . . . . . . . . . . . . . . . . . . 23
comp comp comp comp |
64 | 61, 63 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . 22
comp comp |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
comp comp |
66 | 55, 65 | fmpti 6383 |
. . . . . . . . . . . . . . . . . . . 20
comp comp |
67 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
comp |
68 | 67 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
comp |
69 | 68 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
comp |
70 | 69 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . 23
comp |
71 | 70 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
comp |
72 | 71 | pwex 4848 |
. . . . . . . . . . . . . . . . . . . . 21
comp |
73 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | 72, 73 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . 20
comp comp comp comp |
75 | 66, 74 | mpbir 221 |
. . . . . . . . . . . . . . . . . . 19
comp
comp |
76 | 75 | rgen2w 2925 |
. . . . . . . . . . . . . . . . . 18
Nat Nat comp comp |
77 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
Nat Nat comp Nat Nat comp |
78 | 77 | fmpt2 7237 |
. . . . . . . . . . . . . . . . . 18
Nat Nat comp
comp Nat Nat comp Nat Nat
comp |
79 | 76, 78 | mpbi 220 |
. . . . . . . . . . . . . . . . 17
Nat Nat comp Nat Nat
comp |
80 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
Nat
Nat |
81 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
Nat
Nat |
82 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . 18
Nat Nat Nat Nat Nat Nat Nat
Nat |
83 | 80, 81, 82 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
Nat Nat
Nat Nat |
84 | | elpm2r 7875 |
. . . . . . . . . . . . . . . . 17
comp Nat
Nat Nat Nat comp Nat Nat comp Nat Nat
Nat Nat
Nat Nat comp comp Nat
Nat |
85 | 50, 54, 79, 83, 84 | mp4an 709 |
. . . . . . . . . . . . . . . 16
Nat Nat comp comp Nat
Nat |
86 | 85 | sbcth 3450 |
. . . . . . . . . . . . . . 15
Nat Nat comp comp Nat
Nat |
87 | | sbcel1g 3987 |
. . . . . . . . . . . . . . 15
Nat Nat comp comp Nat
Nat
Nat Nat comp comp Nat
Nat |
88 | 86, 87 | mpbid 222 |
. . . . . . . . . . . . . 14
Nat Nat comp comp Nat
Nat |
89 | 49, 88 | ax-mp 5 |
. . . . . . . . . . . . 13
Nat Nat comp comp Nat
Nat |
90 | 89 | sbcth 3450 |
. . . . . . . . . . . 12
Nat Nat comp comp Nat
Nat |
91 | | sbcel1g 3987 |
. . . . . . . . . . . 12
Nat Nat comp comp Nat
Nat
Nat Nat comp comp Nat
Nat |
92 | 90, 91 | mpbid 222 |
. . . . . . . . . . 11
Nat Nat comp comp Nat
Nat |
93 | 48, 92 | ax-mp 5 |
. . . . . . . . . 10
Nat Nat comp comp Nat
Nat |
94 | 93 | rgen2w 2925 |
. . . . . . . . 9
Nat Nat comp comp Nat
Nat |
95 | | eqid 2622 |
. . . . . . . . . 10
Nat Nat comp Nat Nat comp |
96 | 95 | fmpt2 7237 |
. . . . . . . . 9
Nat Nat comp comp Nat
Nat
Nat Nat comp comp Nat
Nat |
97 | 94, 96 | mpbi 220 |
. . . . . . . 8
Nat Nat comp comp Nat
Nat |
98 | 97 | a1i 11 |
. . . . . . 7
Nat Nat comp comp Nat
Nat |
99 | 10, 35, 47, 98 | wunf 9549 |
. . . . . 6
Nat Nat comp |
100 | 10, 33, 99 | wunop 9544 |
. . . . 5
comp Nat Nat comp |
101 | 10, 27, 31, 100 | wuntp 9533 |
. . . 4
Nat
comp
Nat Nat comp
|
102 | 18, 101 | eqeltrd 2701 |
. . 3
|
103 | 1, 13, 16 | fuccat 16630 |
. . 3
|
104 | 102, 103 | elind 3798 |
. 2
|
105 | 104, 11 | eleqtrrd 2704 |
1
|