Step | Hyp | Ref
| Expression |
1 | | invfuc.u |
. 2
|
2 | | invfuc.v |
. . . . . . . 8
|
3 | | eqid 2622 |
. . . . . . . . . 10
|
4 | | fucinv.j |
. . . . . . . . . 10
Inv |
5 | | fuciso.f |
. . . . . . . . . . . . 13
|
6 | | funcrcl 16523 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
|
8 | 7 | simprd 479 |
. . . . . . . . . . 11
|
9 | 8 | adantr 481 |
. . . . . . . . . 10
|
10 | | fuciso.b |
. . . . . . . . . . . 12
|
11 | | relfunc 16522 |
. . . . . . . . . . . . 13
|
12 | | 1st2ndbr 7217 |
. . . . . . . . . . . . 13
|
13 | 11, 5, 12 | sylancr 695 |
. . . . . . . . . . . 12
|
14 | 10, 3, 13 | funcf1 16526 |
. . . . . . . . . . 11
|
15 | 14 | ffvelrnda 6359 |
. . . . . . . . . 10
|
16 | | fuciso.g |
. . . . . . . . . . . . 13
|
17 | | 1st2ndbr 7217 |
. . . . . . . . . . . . 13
|
18 | 11, 16, 17 | sylancr 695 |
. . . . . . . . . . . 12
|
19 | 10, 3, 18 | funcf1 16526 |
. . . . . . . . . . 11
|
20 | 19 | ffvelrnda 6359 |
. . . . . . . . . 10
|
21 | | eqid 2622 |
. . . . . . . . . 10
|
22 | 3, 4, 9, 15, 20, 21 | invss 16421 |
. . . . . . . . 9
|
23 | 22 | ssbrd 4696 |
. . . . . . . 8
|
24 | 2, 23 | mpd 15 |
. . . . . . 7
|
25 | | brxp 5147 |
. . . . . . . 8
|
26 | 25 | simprbi 480 |
. . . . . . 7
|
27 | 24, 26 | syl 17 |
. . . . . 6
|
28 | 27 | ralrimiva 2966 |
. . . . 5
|
29 | | fvex 6201 |
. . . . . . 7
|
30 | 10, 29 | eqeltri 2697 |
. . . . . 6
|
31 | | mptelixpg 7945 |
. . . . . 6
|
32 | 30, 31 | ax-mp 5 |
. . . . 5
|
33 | 28, 32 | sylibr 224 |
. . . 4
|
34 | | fveq2 6191 |
. . . . . 6
|
35 | | fveq2 6191 |
. . . . . 6
|
36 | 34, 35 | oveq12d 6668 |
. . . . 5
|
37 | 36 | cbvixpv 7926 |
. . . 4
|
38 | 33, 37 | syl6eleq 2711 |
. . 3
|
39 | | simpr2 1068 |
. . . . . . . . . . . . . 14
|
40 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
41 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . 18
|
43 | 40, 27, 42 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
44 | 2, 43 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
|
46 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
|
47 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
48 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
49 | | nffvmpt1 6199 |
. . . . . . . . . . . . . . . 16
|
50 | 47, 48, 49 | nfbr 4699 |
. . . . . . . . . . . . . . 15
|
51 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
52 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
53 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
54 | 52, 53 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
55 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
56 | 51, 54, 55 | breq123d 4667 |
. . . . . . . . . . . . . . 15
|
57 | 50, 56 | rspc 3303 |
. . . . . . . . . . . . . 14
|
58 | 39, 46, 57 | sylc 65 |
. . . . . . . . . . . . 13
|
59 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
|
60 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
|
61 | 60, 39 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
62 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
|
63 | 62, 39 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
64 | | eqid 2622 |
. . . . . . . . . . . . . 14
Sect Sect |
65 | 3, 4, 59, 61, 63, 64 | isinv 16420 |
. . . . . . . . . . . . 13
Sect Sect |
66 | 58, 65 | mpbid 222 |
. . . . . . . . . . . 12
Sect Sect |
67 | 66 | simpld 475 |
. . . . . . . . . . 11
Sect |
68 | | eqid 2622 |
. . . . . . . . . . . 12
comp comp |
69 | | eqid 2622 |
. . . . . . . . . . . 12
|
70 | 3, 21, 68, 69, 64, 59, 61, 63 | issect 16413 |
. . . . . . . . . . 11
Sect
comp |
71 | 67, 70 | mpbid 222 |
. . . . . . . . . 10
comp |
72 | 71 | simp3d 1075 |
. . . . . . . . 9
comp |
73 | 72 | oveq1d 6665 |
. . . . . . . 8
comp comp comp |
74 | | simpr1 1067 |
. . . . . . . . . 10
|
75 | 60, 74 | ffvelrnd 6360 |
. . . . . . . . 9
|
76 | | eqid 2622 |
. . . . . . . . . . 11
|
77 | 13 | adantr 481 |
. . . . . . . . . . 11
|
78 | 10, 76, 21, 77, 74, 39 | funcf2 16528 |
. . . . . . . . . 10
|
79 | | simpr3 1069 |
. . . . . . . . . 10
|
80 | 78, 79 | ffvelrnd 6360 |
. . . . . . . . 9
|
81 | 3, 21, 69, 59, 75, 68, 61, 80 | catlid 16344 |
. . . . . . . 8
comp |
82 | 73, 81 | eqtr2d 2657 |
. . . . . . 7
comp comp |
83 | | fuciso.n |
. . . . . . . . 9
Nat |
84 | 1 | adantr 481 |
. . . . . . . . . 10
|
85 | 83, 84 | nat1st2nd 16611 |
. . . . . . . . 9
|
86 | 83, 85, 10, 21, 39 | natcl 16613 |
. . . . . . . 8
|
87 | 71 | simp2d 1074 |
. . . . . . . 8
|
88 | 3, 21, 68, 59, 75, 61, 63, 80, 86, 61, 87 | catass 16347 |
. . . . . . 7
comp comp comp comp |
89 | 83, 85, 10, 76, 68, 74, 39, 79 | nati 16615 |
. . . . . . . 8
comp comp |
90 | 89 | oveq2d 6666 |
. . . . . . 7
comp comp comp comp |
91 | 82, 88, 90 | 3eqtrd 2660 |
. . . . . 6
comp comp |
92 | 91 | oveq1d 6665 |
. . . . 5
comp comp comp comp |
93 | 62, 74 | ffvelrnd 6360 |
. . . . . 6
|
94 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
95 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
96 | | nffvmpt1 6199 |
. . . . . . . . . . . . 13
|
97 | 94, 95, 96 | nfbr 4699 |
. . . . . . . . . . . 12
|
98 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
99 | 35, 34 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
100 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
101 | 98, 99, 100 | breq123d 4667 |
. . . . . . . . . . . 12
|
102 | 97, 101 | rspc 3303 |
. . . . . . . . . . 11
|
103 | 74, 46, 102 | sylc 65 |
. . . . . . . . . 10
|
104 | 3, 4, 59, 75, 93, 64 | isinv 16420 |
. . . . . . . . . 10
Sect Sect |
105 | 103, 104 | mpbid 222 |
. . . . . . . . 9
Sect Sect |
106 | 105 | simprd 479 |
. . . . . . . 8
Sect |
107 | 3, 21, 68, 69, 64, 59, 93, 75 | issect 16413 |
. . . . . . . 8
Sect
comp |
108 | 106, 107 | mpbid 222 |
. . . . . . 7
comp |
109 | 108 | simp1d 1073 |
. . . . . 6
|
110 | 108 | simp2d 1074 |
. . . . . . 7
|
111 | 18 | adantr 481 |
. . . . . . . . 9
|
112 | 10, 76, 21, 111, 74, 39 | funcf2 16528 |
. . . . . . . 8
|
113 | 112, 79 | ffvelrnd 6360 |
. . . . . . 7
|
114 | 3, 21, 68, 59, 75, 93, 63, 110, 113 | catcocl 16346 |
. . . . . 6
comp |
115 | 3, 21, 68, 59, 93, 75, 63, 109, 114, 61, 87 | catass 16347 |
. . . . 5
comp comp comp comp comp comp |
116 | 83, 85, 10, 21, 74 | natcl 16613 |
. . . . . . . 8
|
117 | 3, 21, 68, 59, 93, 75, 93, 109, 116, 63, 113 | catass 16347 |
. . . . . . 7
comp comp comp comp |
118 | 108 | simp3d 1075 |
. . . . . . . 8
comp |
119 | 118 | oveq2d 6666 |
. . . . . . 7
comp comp comp |
120 | 3, 21, 69, 59, 93, 68, 63, 113 | catrid 16345 |
. . . . . . 7
comp |
121 | 117, 119,
120 | 3eqtrd 2660 |
. . . . . 6
comp comp |
122 | 121 | oveq2d 6666 |
. . . . 5
comp comp comp comp |
123 | 92, 115, 122 | 3eqtrrd 2661 |
. . . 4
comp comp |
124 | 123 | ralrimivvva 2972 |
. . 3
comp comp |
125 | 83, 10, 76, 21, 68, 16, 5 | isnat2 16608 |
. . 3
comp comp |
126 | 38, 124, 125 | mpbir2and 957 |
. 2
|
127 | | nfv 1843 |
. . . 4
|
128 | 127, 97, 101 | cbvral 3167 |
. . 3
|
129 | 45, 128 | sylib 208 |
. 2
|
130 | | fuciso.q |
. . 3
FuncCat
|
131 | | fucinv.i |
. . 3
Inv |
132 | 130, 10, 83, 5, 16, 131, 4 | fucinv 16633 |
. 2
|
133 | 1, 126, 129, 132 | mpbir3and 1245 |
1
|