MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  catciso Structured version   Unicode version

Theorem catciso 15945
Description: A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
catciso.c  |-  C  =  (CatCat `  U )
catciso.b  |-  B  =  ( Base `  C
)
catciso.r  |-  R  =  ( Base `  X
)
catciso.s  |-  S  =  ( Base `  Y
)
catciso.u  |-  ( ph  ->  U  e.  V )
catciso.x  |-  ( ph  ->  X  e.  B )
catciso.y  |-  ( ph  ->  Y  e.  B )
catciso.i  |-  I  =  (  Iso  `  C
)
Assertion
Ref Expression
catciso  |-  ( ph  ->  ( F  e.  ( X I Y )  <-> 
( F  e.  ( ( X Full  Y )  i^i  ( X Faith  Y
) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) ) )

Proof of Theorem catciso
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 15710 . . . . 5  |-  Rel  ( X  Func  Y )
2 catciso.b . . . . . . . . . . . . . 14  |-  B  =  ( Base `  C
)
3 eqid 2428 . . . . . . . . . . . . . 14  |-  (Inv `  C )  =  (Inv
`  C )
4 catciso.u . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  e.  V )
5 catciso.c . . . . . . . . . . . . . . . 16  |-  C  =  (CatCat `  U )
65catccat 15942 . . . . . . . . . . . . . . 15  |-  ( U  e.  V  ->  C  e.  Cat )
74, 6syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  Cat )
8 catciso.x . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  B )
9 catciso.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  B )
10 catciso.i . . . . . . . . . . . . . 14  |-  I  =  (  Iso  `  C
)
112, 3, 7, 8, 9, 10isoval 15613 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X I Y )  =  dom  ( X (Inv `  C ) Y ) )
1211eleq2d 2491 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  ( X I Y )  <-> 
F  e.  dom  ( X (Inv `  C ) Y ) ) )
1312biimpa 486 . . . . . . . . . . 11  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F  e.  dom  ( X (Inv `  C ) Y ) )
147adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  C  e.  Cat )
158adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  X  e.  B )
169adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  Y  e.  B )
172, 3, 14, 15, 16invfun 15612 . . . . . . . . . . . 12  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  Fun  ( X (Inv `  C ) Y ) )
18 funfvbrb 5954 . . . . . . . . . . . 12  |-  ( Fun  ( X (Inv `  C ) Y )  ->  ( F  e. 
dom  ( X (Inv
`  C ) Y )  <->  F ( X (Inv
`  C ) Y ) ( ( X (Inv `  C ) Y ) `  F
) ) )
1917, 18syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F  e.  dom  ( X (Inv
`  C ) Y )  <->  F ( X (Inv
`  C ) Y ) ( ( X (Inv `  C ) Y ) `  F
) ) )
2013, 19mpbid 213 . . . . . . . . . 10  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F ( X (Inv `  C ) Y ) ( ( X (Inv `  C
) Y ) `  F ) )
21 eqid 2428 . . . . . . . . . . 11  |-  (Sect `  C )  =  (Sect `  C )
222, 3, 14, 15, 16, 21isinv 15608 . . . . . . . . . 10  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F
( X (Inv `  C ) Y ) ( ( X (Inv
`  C ) Y ) `  F )  <-> 
( F ( X (Sect `  C ) Y ) ( ( X (Inv `  C
) Y ) `  F )  /\  (
( X (Inv `  C ) Y ) `
 F ) ( Y (Sect `  C
) X ) F ) ) )
2320, 22mpbid 213 . . . . . . . . 9  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F
( X (Sect `  C ) Y ) ( ( X (Inv
`  C ) Y ) `  F )  /\  ( ( X (Inv `  C ) Y ) `  F
) ( Y (Sect `  C ) X ) F ) )
2423simpld 460 . . . . . . . 8  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F ( X (Sect `  C ) Y ) ( ( X (Inv `  C
) Y ) `  F ) )
25 eqid 2428 . . . . . . . . 9  |-  ( Hom  `  C )  =  ( Hom  `  C )
26 eqid 2428 . . . . . . . . 9  |-  (comp `  C )  =  (comp `  C )
27 eqid 2428 . . . . . . . . 9  |-  ( Id
`  C )  =  ( Id `  C
)
282, 25, 26, 27, 21, 14, 15, 16issect 15601 . . . . . . . 8  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F
( X (Sect `  C ) Y ) ( ( X (Inv
`  C ) Y ) `  F )  <-> 
( F  e.  ( X ( Hom  `  C
) Y )  /\  ( ( X (Inv
`  C ) Y ) `  F )  e.  ( Y ( Hom  `  C ) X )  /\  (
( ( X (Inv
`  C ) Y ) `  F ) ( <. X ,  Y >. (comp `  C ) X ) F )  =  ( ( Id
`  C ) `  X ) ) ) )
2924, 28mpbid 213 . . . . . . 7  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F  e.  ( X ( Hom  `  C ) Y )  /\  ( ( X (Inv `  C ) Y ) `  F
)  e.  ( Y ( Hom  `  C
) X )  /\  ( ( ( X (Inv `  C ) Y ) `  F
) ( <. X ,  Y >. (comp `  C
) X ) F )  =  ( ( Id `  C ) `
 X ) ) )
3029simp1d 1017 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F  e.  ( X ( Hom  `  C
) Y ) )
315, 2, 4, 25, 8, 9catchom 15937 . . . . . . 7  |-  ( ph  ->  ( X ( Hom  `  C ) Y )  =  ( X  Func  Y ) )
3231adantr 466 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( X
( Hom  `  C ) Y )  =  ( X  Func  Y )
)
3330, 32eleqtrd 2508 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F  e.  ( X  Func  Y ) )
34 1st2nd 6797 . . . . 5  |-  ( ( Rel  ( X  Func  Y )  /\  F  e.  ( X  Func  Y
) )  ->  F  =  <. ( 1st `  F
) ,  ( 2nd `  F ) >. )
351, 33, 34sylancr 667 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F  =  <. ( 1st `  F
) ,  ( 2nd `  F ) >. )
36 1st2ndbr 6800 . . . . . . 7  |-  ( ( Rel  ( X  Func  Y )  /\  F  e.  ( X  Func  Y
) )  ->  ( 1st `  F ) ( X  Func  Y )
( 2nd `  F
) )
371, 33, 36sylancr 667 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  F ) ( X 
Func  Y ) ( 2nd `  F ) )
38 catciso.r . . . . . . . . 9  |-  R  =  ( Base `  X
)
39 eqid 2428 . . . . . . . . 9  |-  ( Hom  `  X )  =  ( Hom  `  X )
40 eqid 2428 . . . . . . . . 9  |-  ( Hom  `  Y )  =  ( Hom  `  Y )
4137adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 1st `  F ) ( X 
Func  Y ) ( 2nd `  F ) )
42 simprl 762 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  x  e.  R )
43 simprr 764 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  y  e.  R )
4438, 39, 40, 41, 42, 43funcf2 15716 . . . . . . . 8  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( x
( 2nd `  F
) y ) : ( x ( Hom  `  X ) y ) --> ( ( ( 1st `  F ) `  x
) ( Hom  `  Y
) ( ( 1st `  F ) `  y
) ) )
45 catciso.s . . . . . . . . . 10  |-  S  =  ( Base `  Y
)
46 relfunc 15710 . . . . . . . . . . . 12  |-  Rel  ( Y  Func  X )
4729simp2d 1018 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( X (Inv `  C ) Y ) `  F
)  e.  ( Y ( Hom  `  C
) X ) )
485, 2, 4, 25, 9, 8catchom 15937 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y ( Hom  `  C ) X )  =  ( Y  Func  X ) )
4948adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( Y
( Hom  `  C ) X )  =  ( Y  Func  X )
)
5047, 49eleqtrd 2508 . . . . . . . . . . . 12  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( X (Inv `  C ) Y ) `  F
)  e.  ( Y 
Func  X ) )
51 1st2ndbr 6800 . . . . . . . . . . . 12  |-  ( ( Rel  ( Y  Func  X )  /\  ( ( X (Inv `  C
) Y ) `  F )  e.  ( Y  Func  X )
)  ->  ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) ( Y  Func  X ) ( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) )
5246, 50, 51sylancr 667 . . . . . . . . . . 11  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) ( Y  Func  X ) ( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) )
5352adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) ( Y  Func  X ) ( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) )
5438, 45, 41funcf1 15714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 1st `  F ) : R --> S )
5554, 42ffvelrnd 5982 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  F ) `  x )  e.  S
)
5654, 43ffvelrnd 5982 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  F ) `  y )  e.  S
)
5745, 40, 39, 53, 55, 56funcf2 15716 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) : ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) --> ( ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  x )
) ( Hom  `  X
) ( ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) `  ( ( 1st `  F ) `
 y ) ) ) )
5829simp3d 1019 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( (
( X (Inv `  C ) Y ) `
 F ) (
<. X ,  Y >. (comp `  C ) X ) F )  =  ( ( Id `  C
) `  X )
)
594adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  U  e.  V )
605, 2, 59, 26, 15, 16, 15, 33, 50catcco 15939 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( (
( X (Inv `  C ) Y ) `
 F ) (
<. X ,  Y >. (comp `  C ) X ) F )  =  ( ( ( X (Inv
`  C ) Y ) `  F )  o.func 
F ) )
61 eqid 2428 . . . . . . . . . . . . . . . . . 18  |-  (idfunc `  X
)  =  (idfunc `  X
)
625, 2, 27, 61, 4, 8catcid 15941 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Id `  C ) `  X
)  =  (idfunc `  X
) )
6362adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( Id `  C ) `  X )  =  (idfunc `  X ) )
6458, 60, 633eqtr3d 2470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( (
( X (Inv `  C ) Y ) `
 F )  o.func  F
)  =  (idfunc `  X
) )
6564adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( X (Inv `  C ) Y ) `
 F )  o.func  F
)  =  (idfunc `  X
) )
6665fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 1st `  ( ( ( X (Inv `  C ) Y ) `  F
)  o.func 
F ) )  =  ( 1st `  (idfunc `  X
) ) )
6766fveq1d 5827 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( ( X (Inv `  C
) Y ) `  F )  o.func  F )
) `  x )  =  ( ( 1st `  (idfunc `  X ) ) `  x ) )
6833adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  F  e.  ( X  Func  Y ) )
6950adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( X (Inv `  C ) Y ) `  F
)  e.  ( Y 
Func  X ) )
7038, 68, 69, 42cofu1 15732 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( ( X (Inv `  C
) Y ) `  F )  o.func  F )
) `  x )  =  ( ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) `  ( ( 1st `  F ) `
 x ) ) )
715, 2, 4catcbas 15935 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
72 inss2 3626 . . . . . . . . . . . . . . . 16  |-  ( U  i^i  Cat )  C_  Cat
7371, 72syl6eqss 3457 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  C_  Cat )
7473, 8sseldd 3408 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  Cat )
7574ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  X  e.  Cat )
7661, 38, 75, 42idfu1 15728 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  (idfunc `  X ) ) `  x )  =  x )
7767, 70, 763eqtr3d 2470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( X (Inv `  C ) Y ) `  F
) ) `  (
( 1st `  F
) `  x )
)  =  x )
7866fveq1d 5827 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( ( X (Inv `  C
) Y ) `  F )  o.func  F )
) `  y )  =  ( ( 1st `  (idfunc `  X ) ) `  y ) )
7938, 68, 69, 43cofu1 15732 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( ( X (Inv `  C
) Y ) `  F )  o.func  F )
) `  y )  =  ( ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) `  ( ( 1st `  F ) `
 y ) ) )
8061, 38, 75, 43idfu1 15728 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  (idfunc `  X ) ) `  y )  =  y )
8178, 79, 803eqtr3d 2470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( ( 1st `  ( ( X (Inv `  C ) Y ) `  F
) ) `  (
( 1st `  F
) `  y )
)  =  y )
8277, 81oveq12d 6267 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  (
( X (Inv `  C ) Y ) `
 F ) ) `
 ( ( 1st `  F ) `  x
) ) ( Hom  `  X ) ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  y )
) )  =  ( x ( Hom  `  X
) y ) )
8382feq3d 5677 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( ( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) : ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) --> ( ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  x )
) ( Hom  `  X
) ( ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) `  ( ( 1st `  F ) `
 y ) ) )  <->  ( ( ( 1st `  F ) `
 x ) ( 2nd `  ( ( X (Inv `  C
) Y ) `  F ) ) ( ( 1st `  F
) `  y )
) : ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) --> ( x ( Hom  `  X )
y ) ) )
8457, 83mpbid 213 . . . . . . . 8  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) : ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) --> ( x ( Hom  `  X )
y ) )
8565fveq2d 5829 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 2nd `  ( ( ( X (Inv `  C ) Y ) `  F
)  o.func 
F ) )  =  ( 2nd `  (idfunc `  X
) ) )
8685oveqd 6266 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( x
( 2nd `  (
( ( X (Inv
`  C ) Y ) `  F )  o.func 
F ) ) y )  =  ( x ( 2nd `  (idfunc `  X
) ) y ) )
8738, 68, 69, 42, 43cofu2nd 15733 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( x
( 2nd `  (
( ( X (Inv
`  C ) Y ) `  F )  o.func 
F ) ) y )  =  ( ( ( ( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
)  o.  ( x ( 2nd `  F
) y ) ) )
8861, 38, 75, 39, 42, 43idfu2nd 15725 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( x
( 2nd `  (idfunc `  X
) ) y )  =  (  _I  |`  (
x ( Hom  `  X
) y ) ) )
8986, 87, 883eqtr3d 2470 . . . . . . . 8  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( ( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
)  o.  ( x ( 2nd `  F
) y ) )  =  (  _I  |`  (
x ( Hom  `  X
) y ) ) )
9023simprd 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( X (Inv `  C ) Y ) `  F
) ( Y (Sect `  C ) X ) F )
912, 25, 26, 27, 21, 14, 16, 15issect 15601 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( (
( X (Inv `  C ) Y ) `
 F ) ( Y (Sect `  C
) X ) F  <-> 
( ( ( X (Inv `  C ) Y ) `  F
)  e.  ( Y ( Hom  `  C
) X )  /\  F  e.  ( X
( Hom  `  C ) Y )  /\  ( F ( <. Y ,  X >. (comp `  C
) Y ) ( ( X (Inv `  C ) Y ) `
 F ) )  =  ( ( Id
`  C ) `  Y ) ) ) )
9290, 91mpbid 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( (
( X (Inv `  C ) Y ) `
 F )  e.  ( Y ( Hom  `  C ) X )  /\  F  e.  ( X ( Hom  `  C
) Y )  /\  ( F ( <. Y ,  X >. (comp `  C
) Y ) ( ( X (Inv `  C ) Y ) `
 F ) )  =  ( ( Id
`  C ) `  Y ) ) )
9392simp3d 1019 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F
( <. Y ,  X >. (comp `  C ) Y ) ( ( X (Inv `  C
) Y ) `  F ) )  =  ( ( Id `  C ) `  Y
) )
945, 2, 59, 26, 16, 15, 16, 50, 33catcco 15939 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F
( <. Y ,  X >. (comp `  C ) Y ) ( ( X (Inv `  C
) Y ) `  F ) )  =  ( F  o.func  ( ( X (Inv `  C ) Y ) `  F
) ) )
95 eqid 2428 . . . . . . . . . . . . . . 15  |-  (idfunc `  Y
)  =  (idfunc `  Y
)
965, 2, 27, 95, 4, 9catcid 15941 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Id `  C ) `  Y
)  =  (idfunc `  Y
) )
9796adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( Id `  C ) `  Y )  =  (idfunc `  Y ) )
9893, 94, 973eqtr3d 2470 . . . . . . . . . . . 12  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F  o.func  ( ( X (Inv
`  C ) Y ) `  F ) )  =  (idfunc `  Y
) )
9998adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( F  o.func  ( ( X (Inv
`  C ) Y ) `  F ) )  =  (idfunc `  Y
) )
10099fveq2d 5829 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( 2nd `  ( F  o.func  ( ( X (Inv `  C ) Y ) `  F
) ) )  =  ( 2nd `  (idfunc `  Y
) ) )
101100oveqd 6266 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  ( F  o.func  ( ( X (Inv
`  C ) Y ) `  F ) ) ) ( ( 1st `  F ) `
 y ) )  =  ( ( ( 1st `  F ) `
 x ) ( 2nd `  (idfunc `  Y
) ) ( ( 1st `  F ) `
 y ) ) )
10245, 69, 68, 55, 56cofu2nd 15733 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  ( F  o.func  ( ( X (Inv
`  C ) Y ) `  F ) ) ) ( ( 1st `  F ) `
 y ) )  =  ( ( ( ( 1st `  (
( X (Inv `  C ) Y ) `
 F ) ) `
 ( ( 1st `  F ) `  x
) ) ( 2nd `  F ) ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  y )
) )  o.  (
( ( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) ) )
10377, 81oveq12d 6267 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  (
( X (Inv `  C ) Y ) `
 F ) ) `
 ( ( 1st `  F ) `  x
) ) ( 2nd `  F ) ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  y )
) )  =  ( x ( 2nd `  F
) y ) )
104103coeq1d 4958 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( ( 1st `  (
( X (Inv `  C ) Y ) `
 F ) ) `
 ( ( 1st `  F ) `  x
) ) ( 2nd `  F ) ( ( 1st `  ( ( X (Inv `  C
) Y ) `  F ) ) `  ( ( 1st `  F
) `  y )
) )  o.  (
( ( 1st `  F
) `  x )
( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) )  =  ( ( x ( 2nd `  F ) y )  o.  ( ( ( 1st `  F ) `
 x ) ( 2nd `  ( ( X (Inv `  C
) Y ) `  F ) ) ( ( 1st `  F
) `  y )
) ) )
105102, 104eqtrd 2462 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  ( F  o.func  ( ( X (Inv
`  C ) Y ) `  F ) ) ) ( ( 1st `  F ) `
 y ) )  =  ( ( x ( 2nd `  F
) y )  o.  ( ( ( 1st `  F ) `  x
) ( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) ) )
10673ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  B  C_  Cat )
1079ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  Y  e.  B )
108106, 107sseldd 3408 . . . . . . . . . 10  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  Y  e.  Cat )
10995, 45, 108, 40, 55, 56idfu2nd 15725 . . . . . . . . 9  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
( 1st `  F
) `  x )
( 2nd `  (idfunc `  Y
) ) ( ( 1st `  F ) `
 y ) )  =  (  _I  |`  (
( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) ) )
110101, 105, 1093eqtr3d 2470 . . . . . . . 8  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( (
x ( 2nd `  F
) y )  o.  ( ( ( 1st `  F ) `  x
) ( 2nd `  (
( X (Inv `  C ) Y ) `
 F ) ) ( ( 1st `  F
) `  y )
) )  =  (  _I  |`  ( (
( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) ) )
11144, 84, 89, 110fcof1od 6151 . . . . . . 7  |-  ( ( ( ph  /\  F  e.  ( X I Y ) )  /\  (
x  e.  R  /\  y  e.  R )
)  ->  ( x
( 2nd `  F
) y ) : ( x ( Hom  `  X ) y ) -1-1-onto-> ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) )
112111ralrimivva 2786 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  A. x  e.  R  A. y  e.  R  ( x
( 2nd `  F
) y ) : ( x ( Hom  `  X ) y ) -1-1-onto-> ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) )
11338, 39, 40isffth2 15764 . . . . . 6  |-  ( ( 1st `  F ) ( ( X Full  Y
)  i^i  ( X Faith  Y ) ) ( 2nd `  F )  <->  ( ( 1st `  F ) ( X  Func  Y )
( 2nd `  F
)  /\  A. x  e.  R  A. y  e.  R  ( x
( 2nd `  F
) y ) : ( x ( Hom  `  X ) y ) -1-1-onto-> ( ( ( 1st `  F
) `  x )
( Hom  `  Y ) ( ( 1st `  F
) `  y )
) ) )
11437, 112, 113sylanbrc 668 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  F ) ( ( X Full  Y )  i^i  ( X Faith  Y ) ) ( 2nd `  F
) )
115 df-br 4367 . . . . 5  |-  ( ( 1st `  F ) ( ( X Full  Y
)  i^i  ( X Faith  Y ) ) ( 2nd `  F )  <->  <. ( 1st `  F ) ,  ( 2nd `  F )
>.  e.  ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) )
116114, 115sylib 199 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  <. ( 1st `  F ) ,  ( 2nd `  F )
>.  e.  ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) )
11735, 116eqeltrd 2506 . . 3  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) ) )
11838, 45, 37funcf1 15714 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  F ) : R --> S )
11945, 38, 52funcf1 15714 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) : S --> R )
12064fveq2d 5829 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( ( ( X (Inv `  C ) Y ) `  F
)  o.func 
F ) )  =  ( 1st `  (idfunc `  X
) ) )
12138, 33, 50cofu1st 15731 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( ( ( X (Inv `  C ) Y ) `  F
)  o.func 
F ) )  =  ( ( 1st `  (
( X (Inv `  C ) Y ) `
 F ) )  o.  ( 1st `  F
) ) )
12274adantr 466 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  X  e.  Cat )
12361, 38, 122idfu1st 15727 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  (idfunc `  X ) )  =  (  _I  |`  R ) )
124120, 121, 1233eqtr3d 2470 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( 1st `  ( ( X (Inv `  C ) Y ) `  F
) )  o.  ( 1st `  F ) )  =  (  _I  |`  R ) )
12598fveq2d 5829 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( F  o.func  ( ( X (Inv `  C ) Y ) `  F
) ) )  =  ( 1st `  (idfunc `  Y
) ) )
12645, 50, 33cofu1st 15731 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  ( F  o.func  ( ( X (Inv `  C ) Y ) `  F
) ) )  =  ( ( 1st `  F
)  o.  ( 1st `  ( ( X (Inv
`  C ) Y ) `  F ) ) ) )
12773, 9sseldd 3408 . . . . . . 7  |-  ( ph  ->  Y  e.  Cat )
128127adantr 466 . . . . . 6  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  Y  e.  Cat )
12995, 45, 128idfu1st 15727 . . . . 5  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  (idfunc `  Y ) )  =  (  _I  |`  S ) )
130125, 126, 1293eqtr3d 2470 . . . 4  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( ( 1st `  F )  o.  ( 1st `  (
( X (Inv `  C ) Y ) `
 F ) ) )  =  (  _I  |`  S ) )
131118, 119, 124, 130fcof1od 6151 . . 3  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( 1st `  F ) : R -1-1-onto-> S
)
132117, 131jca 534 . 2  |-  ( (
ph  /\  F  e.  ( X I Y ) )  ->  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )
1337adantr 466 . . 3  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  C  e.  Cat )
1348adantr 466 . . 3  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  X  e.  B )
1359adantr 466 . . 3  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  Y  e.  B )
136 inss1 3625 . . . . . . 7  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X Full  Y )
137 fullfunc 15754 . . . . . . 7  |-  ( X Full 
Y )  C_  ( X  Func  Y )
138136, 137sstri 3416 . . . . . 6  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X  Func  Y )
139 simprl 762 . . . . . 6  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  F  e.  ( ( X Full  Y )  i^i  ( X Faith  Y ) ) )
140138, 139sseldi 3405 . . . . 5  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  F  e.  ( X  Func  Y ) )
1411, 140, 34sylancr 667 . . . 4  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  F  =  <. ( 1st `  F ) ,  ( 2nd `  F )
>. )
1424adantr 466 . . . . 5  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  U  e.  V )
143 eqid 2428 . . . . 5  |-  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' ( 1st `  F ) `  x
) ( 2nd `  F
) ( `' ( 1st `  F ) `
 y ) ) )  =  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' ( 1st `  F ) `  x
) ( 2nd `  F
) ( `' ( 1st `  F ) `
 y ) ) )
144141, 139eqeltrrd 2507 . . . . . 6  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  <. ( 1st `  F
) ,  ( 2nd `  F ) >.  e.  ( ( X Full  Y )  i^i  ( X Faith  Y
) ) )
145144, 115sylibr 215 . . . . 5  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  -> 
( 1st `  F
) ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) ( 2nd `  F ) )
146 simprr 764 . . . . 5  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  -> 
( 1st `  F
) : R -1-1-onto-> S )
1475, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146catcisolem 15944 . . . 4  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  <. ( 1st `  F
) ,  ( 2nd `  F ) >. ( X (Inv `  C ) Y ) <. `' ( 1st `  F ) ,  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' ( 1st `  F
) `  x )
( 2nd `  F
) ( `' ( 1st `  F ) `
 y ) ) ) >. )
148141, 147eqbrtrd 4387 . . 3  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  F ( X (Inv
`  C ) Y ) <. `' ( 1st `  F ) ,  ( x  e.  S , 
y  e.  S  |->  `' ( ( `' ( 1st `  F ) `
 x ) ( 2nd `  F ) ( `' ( 1st `  F ) `  y
) ) ) >.
)
1492, 3, 133, 134, 135, 10, 148inviso1 15614 . 2  |-  ( (
ph  /\  ( F  e.  ( ( X Full  Y
)  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) )  ->  F  e.  ( X I Y ) )
150132, 149impbida 840 1  |-  ( ph  ->  ( F  e.  ( X I Y )  <-> 
( F  e.  ( ( X Full  Y )  i^i  ( X Faith  Y
) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   A.wral 2714    i^i cin 3378    C_ wss 3379   <.cop 3947   class class class wbr 4366    _I cid 4706   `'ccnv 4795   dom cdm 4796    |` cres 4798    o. ccom 4800   Rel wrel 4801   Fun wfun 5538   -->wf 5540   -1-1-onto->wf1o 5543   ` cfv 5544  (class class class)co 6249    |-> cmpt2 6251   1stc1st 6749   2ndc2nd 6750   Basecbs 15064   Hom chom 15144  compcco 15145   Catccat 15513   Idccid 15514  Sectcsect 15592  Invcinv 15593    Iso ciso 15594    Func cfunc 15702  idfunccidfu 15703    o.func ccofu 15704   Full cful 15750   Faith cfth 15751  CatCatccatc 15932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623  df-7 10624  df-8 10625  df-9 10626  df-10 10627  df-n0 10821  df-z 10889  df-dec 11003  df-uz 11111  df-fz 11736  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-hom 15157  df-cco 15158  df-cat 15517  df-cid 15518  df-sect 15595  df-inv 15596  df-iso 15597  df-func 15706  df-idfu 15707  df-cofu 15708  df-full 15752  df-fth 15753  df-catc 15933
This theorem is referenced by:  yoniso  16113
  Copyright terms: Public domain W3C validator