Step | Hyp | Ref
| Expression |
1 | | relfunc 16522 |
. . . . 5
|
2 | | catciso.b |
. . . . . . . . . . . . . 14
|
3 | | eqid 2622 |
. . . . . . . . . . . . . 14
Inv Inv |
4 | | catciso.u |
. . . . . . . . . . . . . . 15
|
5 | | catciso.c |
. . . . . . . . . . . . . . . 16
CatCat |
6 | 5 | catccat 16754 |
. . . . . . . . . . . . . . 15
|
7 | 4, 6 | syl 17 |
. . . . . . . . . . . . . 14
|
8 | | catciso.x |
. . . . . . . . . . . . . 14
|
9 | | catciso.y |
. . . . . . . . . . . . . 14
|
10 | | catciso.i |
. . . . . . . . . . . . . 14
|
11 | 2, 3, 7, 8, 9, 10 | isoval 16425 |
. . . . . . . . . . . . 13
Inv |
12 | 11 | eleq2d 2687 |
. . . . . . . . . . . 12
Inv |
13 | 12 | biimpa 501 |
. . . . . . . . . . 11
Inv |
14 | 7 | adantr 481 |
. . . . . . . . . . . . 13
|
15 | 8 | adantr 481 |
. . . . . . . . . . . . 13
|
16 | 9 | adantr 481 |
. . . . . . . . . . . . 13
|
17 | 2, 3, 14, 15, 16 | invfun 16424 |
. . . . . . . . . . . 12
Inv |
18 | | funfvbrb 6330 |
. . . . . . . . . . . 12
Inv Inv InvInv |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
Inv InvInv |
20 | 13, 19 | mpbid 222 |
. . . . . . . . . 10
InvInv |
21 | | eqid 2622 |
. . . . . . . . . . 11
Sect Sect |
22 | 2, 3, 14, 15, 16, 21 | isinv 16420 |
. . . . . . . . . 10
InvInv SectInv InvSect |
23 | 20, 22 | mpbid 222 |
. . . . . . . . 9
SectInv InvSect |
24 | 23 | simpld 475 |
. . . . . . . 8
SectInv |
25 | | eqid 2622 |
. . . . . . . . 9
|
26 | | eqid 2622 |
. . . . . . . . 9
comp comp |
27 | | eqid 2622 |
. . . . . . . . 9
|
28 | 2, 25, 26, 27, 21, 14, 15, 16 | issect 16413 |
. . . . . . . 8
SectInv Inv Inv comp |
29 | 24, 28 | mpbid 222 |
. . . . . . 7
Inv Inv comp |
30 | 29 | simp1d 1073 |
. . . . . 6
|
31 | 5, 2, 4, 25, 8, 9 | catchom 16749 |
. . . . . . 7
|
32 | 31 | adantr 481 |
. . . . . 6
|
33 | 30, 32 | eleqtrd 2703 |
. . . . 5
|
34 | | 1st2nd 7214 |
. . . . 5
|
35 | 1, 33, 34 | sylancr 695 |
. . . 4
|
36 | | 1st2ndbr 7217 |
. . . . . . 7
|
37 | 1, 33, 36 | sylancr 695 |
. . . . . 6
|
38 | | catciso.r |
. . . . . . . . 9
|
39 | | eqid 2622 |
. . . . . . . . 9
|
40 | | eqid 2622 |
. . . . . . . . 9
|
41 | 37 | adantr 481 |
. . . . . . . . 9
|
42 | | simprl 794 |
. . . . . . . . 9
|
43 | | simprr 796 |
. . . . . . . . 9
|
44 | 38, 39, 40, 41, 42, 43 | funcf2 16528 |
. . . . . . . 8
|
45 | | catciso.s |
. . . . . . . . . 10
|
46 | | relfunc 16522 |
. . . . . . . . . . . 12
|
47 | 29 | simp2d 1074 |
. . . . . . . . . . . . 13
Inv |
48 | 5, 2, 4, 25, 9, 8 | catchom 16749 |
. . . . . . . . . . . . . 14
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . 13
|
50 | 47, 49 | eleqtrd 2703 |
. . . . . . . . . . . 12
Inv |
51 | | 1st2ndbr 7217 |
. . . . . . . . . . . 12
Inv
Inv Inv |
52 | 46, 50, 51 | sylancr 695 |
. . . . . . . . . . 11
Inv Inv |
53 | 52 | adantr 481 |
. . . . . . . . . 10
Inv Inv |
54 | 38, 45, 41 | funcf1 16526 |
. . . . . . . . . . 11
|
55 | 54, 42 | ffvelrnd 6360 |
. . . . . . . . . 10
|
56 | 54, 43 | ffvelrnd 6360 |
. . . . . . . . . 10
|
57 | 45, 40, 39, 53, 55, 56 | funcf2 16528 |
. . . . . . . . 9
Inv
Inv Inv |
58 | 29 | simp3d 1075 |
. . . . . . . . . . . . . . . 16
Inv comp |
59 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
60 | 5, 2, 59, 26, 15, 16, 15, 33, 50 | catcco 16751 |
. . . . . . . . . . . . . . . 16
Inv comp Inv func |
61 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
idfunc idfunc |
62 | 5, 2, 27, 61, 4, 8 | catcid 16753 |
. . . . . . . . . . . . . . . . 17
idfunc |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
idfunc |
64 | 58, 60, 63 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
Inv func idfunc |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
Inv func idfunc |
66 | 65 | fveq2d 6195 |
. . . . . . . . . . . . 13
Inv func idfunc |
67 | 66 | fveq1d 6193 |
. . . . . . . . . . . 12
Inv func
idfunc |
68 | 33 | adantr 481 |
. . . . . . . . . . . . 13
|
69 | 50 | adantr 481 |
. . . . . . . . . . . . 13
Inv |
70 | 38, 68, 69, 42 | cofu1 16544 |
. . . . . . . . . . . 12
Inv func
Inv |
71 | 5, 2, 4 | catcbas 16747 |
. . . . . . . . . . . . . . . 16
|
72 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
|
73 | 71, 72 | syl6eqss 3655 |
. . . . . . . . . . . . . . 15
|
74 | 73, 8 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
76 | 61, 38, 75, 42 | idfu1 16540 |
. . . . . . . . . . . 12
idfunc |
77 | 67, 70, 76 | 3eqtr3d 2664 |
. . . . . . . . . . 11
Inv |
78 | 66 | fveq1d 6193 |
. . . . . . . . . . . 12
Inv func
idfunc |
79 | 38, 68, 69, 43 | cofu1 16544 |
. . . . . . . . . . . 12
Inv func
Inv |
80 | 61, 38, 75, 43 | idfu1 16540 |
. . . . . . . . . . . 12
idfunc |
81 | 78, 79, 80 | 3eqtr3d 2664 |
. . . . . . . . . . 11
Inv |
82 | 77, 81 | oveq12d 6668 |
. . . . . . . . . 10
Inv Inv |
83 | 82 | feq3d 6032 |
. . . . . . . . 9
Inv
Inv Inv Inv
|
84 | 57, 83 | mpbid 222 |
. . . . . . . 8
Inv
|
85 | 65 | fveq2d 6195 |
. . . . . . . . . 10
Inv func idfunc |
86 | 85 | oveqd 6667 |
. . . . . . . . 9
Inv func idfunc |
87 | 38, 68, 69, 42, 43 | cofu2nd 16545 |
. . . . . . . . 9
Inv func Inv |
88 | 61, 38, 75, 39, 42, 43 | idfu2nd 16537 |
. . . . . . . . 9
idfunc |
89 | 86, 87, 88 | 3eqtr3d 2664 |
. . . . . . . 8
Inv |
90 | 23 | simprd 479 |
. . . . . . . . . . . . . . 15
InvSect |
91 | 2, 25, 26, 27, 21, 14, 16, 15 | issect 16413 |
. . . . . . . . . . . . . . 15
InvSect Inv
compInv |
92 | 90, 91 | mpbid 222 |
. . . . . . . . . . . . . 14
Inv compInv |
93 | 92 | simp3d 1075 |
. . . . . . . . . . . . 13
compInv |
94 | 5, 2, 59, 26, 16, 15, 16, 50, 33 | catcco 16751 |
. . . . . . . . . . . . 13
compInv func
Inv |
95 | | eqid 2622 |
. . . . . . . . . . . . . . 15
idfunc idfunc |
96 | 5, 2, 27, 95, 4, 9 | catcid 16753 |
. . . . . . . . . . . . . 14
idfunc |
97 | 96 | adantr 481 |
. . . . . . . . . . . . 13
idfunc |
98 | 93, 94, 97 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
func Inv idfunc |
99 | 98 | adantr 481 |
. . . . . . . . . . 11
func Inv idfunc |
100 | 99 | fveq2d 6195 |
. . . . . . . . . 10
func
Inv idfunc |
101 | 100 | oveqd 6667 |
. . . . . . . . 9
func Inv idfunc |
102 | 45, 69, 68, 55, 56 | cofu2nd 16545 |
. . . . . . . . . 10
func Inv InvInv Inv |
103 | 77, 81 | oveq12d 6668 |
. . . . . . . . . . 11
InvInv |
104 | 103 | coeq1d 5283 |
. . . . . . . . . 10
InvInv Inv Inv |
105 | 102, 104 | eqtrd 2656 |
. . . . . . . . 9
func Inv Inv |
106 | 73 | ad2antrr 762 |
. . . . . . . . . . 11
|
107 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
|
108 | 106, 107 | sseldd 3604 |
. . . . . . . . . 10
|
109 | 95, 45, 108, 40, 55, 56 | idfu2nd 16537 |
. . . . . . . . 9
idfunc
|
110 | 101, 105,
109 | 3eqtr3d 2664 |
. . . . . . . 8
Inv
|
111 | 44, 84, 89, 110 | fcof1od 6549 |
. . . . . . 7
|
112 | 111 | ralrimivva 2971 |
. . . . . 6
|
113 | 38, 39, 40 | isffth2 16576 |
. . . . . 6
Full
Faith
|
114 | 37, 112, 113 | sylanbrc 698 |
. . . . 5
Full Faith |
115 | | df-br 4654 |
. . . . 5
Full
Faith
Full Faith |
116 | 114, 115 | sylib 208 |
. . . 4
Full Faith |
117 | 35, 116 | eqeltrd 2701 |
. . 3
Full
Faith |
118 | 38, 45, 37 | funcf1 16526 |
. . . 4
|
119 | 45, 38, 52 | funcf1 16526 |
. . . 4
Inv |
120 | 64 | fveq2d 6195 |
. . . . 5
Inv func idfunc |
121 | 38, 33, 50 | cofu1st 16543 |
. . . . 5
Inv func Inv |
122 | 74 | adantr 481 |
. . . . . 6
|
123 | 61, 38, 122 | idfu1st 16539 |
. . . . 5
idfunc |
124 | 120, 121,
123 | 3eqtr3d 2664 |
. . . 4
Inv |
125 | 98 | fveq2d 6195 |
. . . . 5
func
Inv idfunc |
126 | 45, 50, 33 | cofu1st 16543 |
. . . . 5
func
Inv Inv |
127 | 73, 9 | sseldd 3604 |
. . . . . . 7
|
128 | 127 | adantr 481 |
. . . . . 6
|
129 | 95, 45, 128 | idfu1st 16539 |
. . . . 5
idfunc |
130 | 125, 126,
129 | 3eqtr3d 2664 |
. . . 4
Inv |
131 | 118, 119,
124, 130 | fcof1od 6549 |
. . 3
|
132 | 117, 131 | jca 554 |
. 2
Full
Faith |
133 | 7 | adantr 481 |
. . 3
Full
Faith
|
134 | 8 | adantr 481 |
. . 3
Full
Faith
|
135 | 9 | adantr 481 |
. . 3
Full
Faith
|
136 | | inss1 3833 |
. . . . . . 7
Full Faith
Full |
137 | | fullfunc 16566 |
. . . . . . 7
Full |
138 | 136, 137 | sstri 3612 |
. . . . . 6
Full Faith
|
139 | | simprl 794 |
. . . . . 6
Full
Faith
Full Faith |
140 | 138, 139 | sseldi 3601 |
. . . . 5
Full
Faith
|
141 | 1, 140, 34 | sylancr 695 |
. . . 4
Full
Faith
|
142 | 4 | adantr 481 |
. . . . 5
Full
Faith
|
143 | | eqid 2622 |
. . . . 5
|
144 | 141, 139 | eqeltrrd 2702 |
. . . . . 6
Full
Faith Full Faith |
145 | 144, 115 | sylibr 224 |
. . . . 5
Full
Faith Full Faith |
146 | | simprr 796 |
. . . . 5
Full
Faith |
147 | 5, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146 | catcisolem 16756 |
. . . 4
Full
Faith Inv |
148 | 141, 147 | eqbrtrd 4675 |
. . 3
Full
Faith Inv |
149 | 2, 3, 133, 134, 135, 10, 148 | inviso1 16426 |
. 2
Full
Faith
|
150 | 132, 149 | impbida 877 |
1
Full Faith |