Step |
Hyp |
Ref |
Expression |
1 |
|
fuciso.q |
|- Q = ( C FuncCat D ) |
2 |
|
fuciso.b |
|- B = ( Base ` C ) |
3 |
|
fuciso.n |
|- N = ( C Nat D ) |
4 |
|
fuciso.f |
|- ( ph -> F e. ( C Func D ) ) |
5 |
|
fuciso.g |
|- ( ph -> G e. ( C Func D ) ) |
6 |
|
fucinv.i |
|- I = ( Inv ` Q ) |
7 |
|
fucinv.j |
|- J = ( Inv ` D ) |
8 |
|
eqid |
|- ( Sect ` Q ) = ( Sect ` Q ) |
9 |
|
eqid |
|- ( Sect ` D ) = ( Sect ` D ) |
10 |
1 2 3 4 5 8 9
|
fucsect |
|- ( ph -> ( U ( F ( Sect ` Q ) G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) ) |
11 |
1 2 3 5 4 8 9
|
fucsect |
|- ( ph -> ( V ( G ( Sect ` Q ) F ) U <-> ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
12 |
10 11
|
anbi12d |
|- ( ph -> ( ( U ( F ( Sect ` Q ) G ) V /\ V ( G ( Sect ` Q ) F ) U ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) ) |
13 |
1
|
fucbas |
|- ( C Func D ) = ( Base ` Q ) |
14 |
|
funcrcl |
|- ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) ) |
15 |
4 14
|
syl |
|- ( ph -> ( C e. Cat /\ D e. Cat ) ) |
16 |
15
|
simpld |
|- ( ph -> C e. Cat ) |
17 |
15
|
simprd |
|- ( ph -> D e. Cat ) |
18 |
1 16 17
|
fuccat |
|- ( ph -> Q e. Cat ) |
19 |
13 6 18 4 5 8
|
isinv |
|- ( ph -> ( U ( F I G ) V <-> ( U ( F ( Sect ` Q ) G ) V /\ V ( G ( Sect ` Q ) F ) U ) ) ) |
20 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
21 |
17
|
adantr |
|- ( ( ph /\ x e. B ) -> D e. Cat ) |
22 |
|
relfunc |
|- Rel ( C Func D ) |
23 |
|
1st2ndbr |
|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
24 |
22 4 23
|
sylancr |
|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
25 |
2 20 24
|
funcf1 |
|- ( ph -> ( 1st ` F ) : B --> ( Base ` D ) ) |
26 |
25
|
ffvelrnda |
|- ( ( ph /\ x e. B ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) ) |
27 |
|
1st2ndbr |
|- ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) ) |
28 |
22 5 27
|
sylancr |
|- ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) ) |
29 |
2 20 28
|
funcf1 |
|- ( ph -> ( 1st ` G ) : B --> ( Base ` D ) ) |
30 |
29
|
ffvelrnda |
|- ( ( ph /\ x e. B ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) ) |
31 |
20 7 21 26 30 9
|
isinv |
|- ( ( ph /\ x e. B ) -> ( ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
32 |
31
|
ralbidva |
|- ( ph -> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> A. x e. B ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
33 |
|
r19.26 |
|- ( A. x e. B ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) |
34 |
32 33
|
bitrdi |
|- ( ph -> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
35 |
34
|
anbi2d |
|- ( ph -> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) ) |
36 |
|
df-3an |
|- ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) |
37 |
|
df-3an |
|- ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) |
38 |
|
3ancoma |
|- ( ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) |
39 |
|
df-3an |
|- ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) |
40 |
38 39
|
bitri |
|- ( ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) |
41 |
37 40
|
anbi12i |
|- ( ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
42 |
|
anandi |
|- ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
43 |
41 42
|
bitr4i |
|- ( ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) |
44 |
35 36 43
|
3bitr4g |
|- ( ph -> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) ) |
45 |
12 19 44
|
3bitr4d |
|- ( ph -> ( U ( F I G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) ) |