:: {U}-Small and {U}-Locally Small Categories
:: by Roland Coghetto
::
:: Received November 8, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users


theorem Th1: :: CLASSES5:1
for X being non empty set holds { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } = [:X,X:] \ [:(X \ {{}}),{{}}:]
proof end;

theorem Th2: :: CLASSES5:2
for X being non empty set st {{}} is Element of X holds
not {{}} in Funcs X
proof end;

theorem Th3: :: CLASSES5:3
EvenNAT is denumerable
proof end;

theorem Th4: :: CLASSES5:4
OddNAT is denumerable
proof end;

theorem Th5: :: CLASSES5:5
for X, Y being non empty set
for y being Element of Y holds [:X,{y}:] c= union (Funcs (X,Y))
proof end;

theorem Th6: :: CLASSES5:6
for X being non empty set
for n being non zero Nat st n -tuples_on X is finite holds
X is finite
proof end;

theorem Th7: :: CLASSES5:7
for X being non empty set holds union (SmallestPartition X) = X
proof end;

theorem :: CLASSES5:8
for X being non empty set holds X, SmallestPartition X are_equipotent
proof end;

theorem :: CLASSES5:9
for C being strict Category holds (C opp) opp = C
proof end;

definition
let x1, x2, x3, x4, x5 be object ;
func [x1,x2,x3,x4,x5] -> object equals :: CLASSES5:def 1
[[x1,x2,x3,x4],x5];
coherence
[[x1,x2,x3,x4],x5] is object ;
end;

:: deftheorem defines [ CLASSES5:def 1 :
for x1, x2, x3, x4, x5 being object holds [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5];

definition
let x be object ;
attr x is quintuple means :Def3: :: CLASSES5:def 2
 ex x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5];
end;

:: deftheorem Def3 defines quintuple CLASSES5:def 2 :
for x being object holds
( x is quintuple iff ex x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5] );

registration
let x1, x2, x3, x4, x5 be object ;
cluster [x1,x2,x3,x4,x5] -> quintuple ;
coherence
[x1,x2,x3,x4,x5] is quintuple ;
end;

theorem Th10: :: CLASSES5:10
for x1, x2, x3, x4, x5, y1, y2, y3, y4, y5 being object st [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 )
proof end;

registration
cluster quintuple for object ;
existence
ex b1 being object st b1 is quintuple
proof end;
end;

registration
cluster quintuple for set ;
existence
ex b1 being set st b1 is quintuple
proof end;
end;

definition
let x be object ;
assume x is quintuple ;
then consider y1, y2, y3, y4, y5 being object such that
A1: x = [y1,y2,y3,y4,y5] ;
func x `1 -> object means :Def4: :: CLASSES5:def 3
 for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
it = y1;
existence
ex b1 being object st
for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being object st ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y1 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines `1 CLASSES5:def 3 :
for x being object st x is quintuple holds
for b2 being object holds
( b2 = x `1 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y1 );

definition
let x be object ;
assume x is quintuple ;
then consider y1, y2, y3, y4, y5 being object such that
A1: x = [y1,y2,y3,y4,y5] ;
func x `2 -> object means :Def5: :: CLASSES5:def 4
 for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
it = y2;
existence
ex b1 being object st
for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being object st ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y2 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines `2 CLASSES5:def 4 :
for x being object st x is quintuple holds
for b2 being object holds
( b2 = x `2 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y2 );

definition
let x be object ;
assume x is quintuple ;
then consider y1, y2, y3, y4, y5 being object such that
A1: x = [y1,y2,y3,y4,y5] ;
func x `3 -> object means :Def6: :: CLASSES5:def 5
 for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
it = y3;
existence
ex b1 being object st
for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y3
proof end;
uniqueness
for b1, b2 being object st ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y3 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines `3 CLASSES5:def 5 :
for x being object st x is quintuple holds
for b2 being object holds
( b2 = x `3 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y3 );

definition
let x be object ;
assume x is quintuple ;
then consider y1, y2, y3, y4, y5 being object such that
A1: x = [y1,y2,y3,y4,y5] ;
func x `4 -> object means :Def7: :: CLASSES5:def 6
 for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
it = y4;
existence
ex b1 being object st
for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y4
proof end;
uniqueness
for b1, b2 being object st ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y4 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines `4 CLASSES5:def 6 :
for x being object st x is quintuple holds
for b2 being object holds
( b2 = x `4 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y4 );

definition
let x be object ;
assume x is quintuple ;
then consider y1, y2, y3, y4, y5 being object such that
A1: x = [y1,y2,y3,y4,y5] ;
func x `5 -> object means :Def8: :: CLASSES5:def 7
 for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
it = y5;
existence
ex b1 being object st
for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y5
proof end;
uniqueness
for b1, b2 being object st ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b1 = y5 ) & ( for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `5 CLASSES5:def 7 :
for x being object st x is quintuple holds
for b2 being object holds
( b2 = x `5 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b2 = y5 );

registration
let x1, x2, x3, x4, x5 be object ;
reduce [x1,x2,x3,x4,x5] `1 to x1;
reducibility
[x1,x2,x3,x4,x5] `1 = x1 by Def4;
reduce [x1,x2,x3,x4,x5] `2 to x2;
reducibility
[x1,x2,x3,x4,x5] `2 = x2 by Def5;
reduce [x1,x2,x3,x4,x5] `3 to x3;
reducibility
[x1,x2,x3,x4,x5] `3 = x3 by Def6;
reduce [x1,x2,x3,x4,x5] `4 to x4;
reducibility
[x1,x2,x3,x4,x5] `4 = x4 by Def7;
reduce [x1,x2,x3,x4,x5] `5 to x5;
reducibility
[x1,x2,x3,x4,x5] `5 = x5 by Def8;
end;

registration
let x be quintuple object ;
reduce [(x `1),(x `2),(x `3),(x `4),(x `5)] to x;
reducibility
[(x `1),(x `2),(x `3),(x `4),(x `5)] = x
proof end;
end;

theorem Th11: :: CLASSES5:11
for U being Universe
for x being Element of U
for x1, x2, x3 being object st x = [x1,x2,x3] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U )
proof end;

theorem Th12: :: CLASSES5:12
for U being Universe
for x being Element of U
for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U )
proof end;

theorem Th13: :: CLASSES5:13
for U being Universe
for x1, x2, x3, x4, x5 being Element of U holds [x1,x2,x3,x4,x5] is Element of U
proof end;

theorem Th14: :: CLASSES5:14
for U being Universe
for x being Element of U
for x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U )
proof end;

definition
let U be Universe;
let u1, u2, u3 be Element of U;
:: original: [
redefine func [u1,u2,u3] -> Element of U;
coherence
[u1,u2,u3] is Element of U by GRCAT_1:1;
let u4 be Element of U;
:: original: [
redefine func [u1,u2,u3,u4] -> Element of U;
coherence
[u1,u2,u3,u4] is Element of U by GRCAT_1:1;
let u5 be Element of U;
:: original: [
redefine func [u1,u2,u3,u4,u5] -> Element of U;
coherence
[u1,u2,u3,u4,u5] is Element of U by Th13;
end;

theorem Th15: :: CLASSES5:15
for x being Subset of FinSETS st x is finite holds
x is Element of FinSETS
proof end;

theorem :: CLASSES5:16
for X being finite set st X c= FinSETS holds
X in FinSETS
proof end;

theorem Th17: :: CLASSES5:17
( union {NAT} c= FinSETS & not union {NAT} in FinSETS & not {NAT} c= FinSETS & not {NAT} in FinSETS )
proof end;

theorem Th18: :: CLASSES5:18
for U being Universe
for x being object holds
( x in U iff {x} in U )
proof end;

theorem Th19: :: CLASSES5:19
for U being Universe
for X being set
for n being non zero Nat st Funcs ((Seg n),{X}) is Element of U holds
X is Element of U
proof end;

theorem :: CLASSES5:20
for U being Universe
for X being set
for n being non zero Nat st n -tuples_on {X} is Element of U holds
X is Element of U
proof end;

theorem Th21: :: CLASSES5:21
for U being Universe
for X being set st union X in U holds
X in U
proof end;

definition
let X be non empty set ;
let x be object ;
attr x is X -set means :: CLASSES5:def 8
x in X;
end;

:: deftheorem defines -set CLASSES5:def 8 :
for X being non empty set
for x being object holds
( x is X -set iff x in X );

definition
let X be non empty set ;
mode Set of X -> set means :Def10: :: CLASSES5:def 9
it is X -set ;
existence
ex b1 being set st b1 is X -set
proof end;
end;

:: deftheorem Def10 defines Set CLASSES5:def 9 :
for X being non empty set
for b2 being set holds
( b2 is Set of X iff b2 is X -set );

theorem :: CLASSES5:22
for U1, U2 being Universe st U1 in U2 holds
for x being object st x is U1 -set holds
x is U2 -set by CLASSES4:def 1;

theorem :: CLASSES5:23
for U1, U2 being Universe st U1 in U2 holds
for x being Set of U1 holds x is Set of U2
proof end;

theorem :: CLASSES5:24
for x being Set of FinSETS holds x is finite
proof end;

theorem :: CLASSES5:25
for x being Subset of FinSETS st x is finite holds
x is Set of FinSETS
proof end;

theorem :: CLASSES5:26
for x being object holds
( x is Set of FinSETS iff x is FinSet )
proof end;

definition
let U be Universe;
let x be object ;
attr x is U -Class means :: CLASSES5:def 10
( x in bool U & not x in U );
end;

:: deftheorem defines -Class CLASSES5:def 10 :
for U being Universe
for x being object holds
( x is U -Class iff ( x in bool U & not x in U ) );

theorem :: CLASSES5:27
for U being Universe
for x being set st x is U -Class holds
not x is empty by CLASSES4:13;

definition
let U be Universe;
mode class of U -> non empty set means :Def12: :: CLASSES5:def 11
it is U -Class ;
existence
ex b1 being non empty set st b1 is U -Class
proof end;
end;

:: deftheorem Def12 defines class CLASSES5:def 11 :
for U being Universe
for b2 being non empty set holds
( b2 is class of U iff b2 is U -Class );

theorem Th28: :: CLASSES5:28
for U being Universe
for X being finite Subset of U holds X in U
proof end;

theorem :: CLASSES5:29
for U being Universe
for C being class of U holds not C is finite
proof end;

theorem :: CLASSES5:30
for U being Universe
for X being Set of U holds U \ X is class of U
proof end;

theorem Th31: :: CLASSES5:31
for X being non finite Subset of FinSETS holds X is class of FinSETS
proof end;

theorem :: CLASSES5:32
NAT is class of FinSETS by Th31, CLASSES4:43;

theorem :: CLASSES5:33
EvenNAT is class of FinSETS
proof end;

theorem :: CLASSES5:34
OddNAT is class of FinSETS
proof end;

theorem :: CLASSES5:35
for U being Universe
for x being object holds
( not x is U -Class or not x is U -set ) ;

theorem :: CLASSES5:36
for U1, U2 being Universe st U1 in U2 holds
for x being object st x is U1 -Class holds
x is U2 -set
proof end;

theorem :: CLASSES5:37
( union {NAT} is FinSETS -Class & not {NAT} is FinSETS -Class & not {NAT} is FinSETS -set ) by Th17;

theorem :: CLASSES5:38
for x being object ex U being Universe st x is U -set
proof end;

theorem :: CLASSES5:39
for x being set holds x is GrothendieckUniverse x -set by CLASSES3:def 4;

definition
let U1, U2 be Universe;
func sup (U1,U2) -> Universe equals :Def13: :: CLASSES5:def 12
U1 if U2 in U1
otherwise U2;
correctness
coherence
( ( U2 in U1 implies U1 is Universe ) & ( not U2 in U1 implies U2 is Universe ) );
consistency
for b1 being Universe holds verum;
;
end;

:: deftheorem Def13 defines sup CLASSES5:def 12 :
for U1, U2 being Universe holds
( ( U2 in U1 implies sup (U1,U2) = U1 ) & ( not U2 in U1 implies sup (U1,U2) = U2 ) );

theorem :: CLASSES5:40
for U1, U2 being Universe
for x being Set of U1
for y being Set of U2 ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )
proof end;

theorem :: CLASSES5:41
for U being Universe
for X being Set of U holds union X is Set of U
proof end;

theorem :: CLASSES5:42
for U being Universe
for X being set st union X is Set of U holds
X is Set of U
proof end;

theorem Th45: :: CLASSES5:43
for U being Universe
for X being set st union X is empty holds
X is U -set
proof end;

theorem :: CLASSES5:44
for U being Universe
for X being class of U holds union X is class of U
proof end;

theorem :: CLASSES5:45
ex X being set st
( union X is class of FinSETS & X is not class of FinSETS & X is not Set of FinSETS & X is Set of SETS )
proof end;

theorem :: CLASSES5:46
for U being Universe
for X being Set of U
for Y being set st Y in X holds
Y is Set of U
proof end;

theorem :: CLASSES5:47
for U being Universe
for X being class of U
for Y being set st Y in X holds
Y is Set of U
proof end;

definition
let U be Universe;
let x be set ;
attr x is U -petit means :: CLASSES5:def 13
 ex u being Element of U st u,x are_equipotent ;
end;

:: deftheorem defines -petit CLASSES5:def 13 :
for U being Universe
for x being set holds
( x is U -petit iff ex u being Element of U st u,x are_equipotent );

theorem :: CLASSES5:48
for U being Universe
for X being Element of U holds X is U -petit ;

theorem :: CLASSES5:49
for U being Universe
for x being set holds
( x is U -petit iff card x in card U )
proof end;

theorem :: CLASSES5:50
for U being Universe
for x being set holds {x} is U -petit
proof end;

definition
let U be Universe;
let G be Group;
attr G is U -element means :: CLASSES5:def 14
 the carrier of G is Element of U;
end;

:: deftheorem defines -element CLASSES5:def 14 :
for U being Universe
for G being Group holds
( G is U -element iff the carrier of G is Element of U );

theorem :: CLASSES5:51
for U being Universe
for G being Group st G is U -element holds
the multF of G is Element of U
proof end;

definition
let U be Universe;
let G be Group;
attr G is U -petit means :: CLASSES5:def 15
 ex g being Group st
( g is U -element & G,g are_isomorphic );
end;

:: deftheorem defines -petit CLASSES5:def 15 :
for U being Universe
for G being Group holds
( G is U -petit iff ex g being Group st
( g is U -element & G,g are_isomorphic ) );

definition
let U be Universe;
let C be Category;
attr C is U -element means :Def17: :: CLASSES5:def 16
( the carrier of C is Element of U & the carrier' of C is Element of U );
end;

:: deftheorem Def17 defines -element CLASSES5:def 16 :
for U being Universe
for C being Category holds
( C is U -element iff ( the carrier of C is Element of U & the carrier' of C is Element of U ) );

theorem Th54: :: CLASSES5:52
for U being Universe
for C being Category st C is U -element holds
( the Source of C is Element of U & the Target of C is Element of U & the Comp of C is Element of U )
proof end;

theorem Th55: :: CLASSES5:53
for U being Universe
for o, m being Element of U holds 1Cat (o,m) is U -element
proof end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -element for CatStr ;
existence
ex b1 being Category st b1 is U -element
proof end;
end;

definition
let U be Universe;
let C be Category;
attr C is U -petit means :: CLASSES5:def 17
 ex c being strict Category st
( c is U -element & C ~= c );
end;

:: deftheorem defines -petit CLASSES5:def 17 :
for U being Universe
for C being Category holds
( C is U -petit iff ex c being strict Category st
( c is U -element & C ~= c ) );

theorem Th56: :: CLASSES5:54
for A being Category
for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A
proof end;

theorem :: CLASSES5:55
for o, m being object holds the Comp of (1Cat (o,m)) = {[[m,m],m]}
proof end;

theorem :: CLASSES5:56
for o, m being object
for c being Object of (1Cat (o,m)) holds c = o
proof end;

theorem Th59: :: CLASSES5:57
for o, m being object
for c being Element of (1Cat (o,m)) holds
( c is Object of (1Cat (o,m)) & c = o & id c = m )
proof end;

theorem Th60: :: CLASSES5:58
for o1, o2, m1, m2 being object holds 1Cat (o1,m1) ~= 1Cat (o2,m2)
proof end;

theorem Th61: :: CLASSES5:59
for U being Universe
for o, m being object holds 1Cat (o,m) is U -petit
proof end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -petit for CatStr ;
existence
ex b1 being Category st b1 is U -petit
proof end;
end;

theorem :: CLASSES5:60
for U being Universe ex C being b1 -petit Category st
( the carrier of C is not Element of U & the carrier' of C is Element of U )
proof end;

theorem :: CLASSES5:61
for U being Universe ex C being b1 -petit Category st
( the carrier of C is not Element of U & the carrier' of C is not Element of U )
proof end;

theorem Th64: :: CLASSES5:62
for U being Universe ex C being b1 -petit Category st
( the carrier of C is Element of U & the carrier' of C is not Element of U )
proof end;

theorem :: CLASSES5:63
for U being Universe holds
not for C being b1 -petit Category holds C is U -element
proof end;

theorem :: CLASSES5:64
for U being Universe
for C being strict Category st C is U -element holds
C is U -petit ;

definition
let U be Universe;
let C be Category;
attr C is U -Category means :: CLASSES5:def 18
 for x, y being Object of C holds Hom (x,y) is U -petit ;
end;

:: deftheorem defines -Category CLASSES5:def 18 :
for U being Universe
for C being Category holds
( C is U -Category iff for x, y being Object of C holds Hom (x,y) is U -petit );

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -Category for CatStr ;
existence
ex b1 being Category st b1 is U -Category
proof end;
end;

theorem :: CLASSES5:65
for C, D being Category
for F being Functor of C,D holds F c= [: the carrier' of C, the carrier' of D:] ;

theorem Th68: :: CLASSES5:66
for C, D being Category holds Funct (C,D) c= bool [: the carrier' of C, the carrier' of D:]
proof end;

theorem Th69: :: CLASSES5:67
for C, D being Category holds NatTrans (C,D) c= [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):]
proof end;

theorem :: CLASSES5:68
for U being Universe
for X, Y, Z being set st X in U & Y in U & Z in U holds
bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U
proof end;

theorem :: CLASSES5:69
for U being Universe
for X, Y being non empty set st Funcs (X,Y) is Element of U holds
X is Element of U
proof end;

:: WP: PROP 1.1.1 a) SGA4
theorem Th72: :: CLASSES5:70
for U being Universe
for C, D being Category st C is U -element & D is U -element holds
Functors (C,D) is U -element
proof end;

theorem :: CLASSES5:71
for U being Universe
for c being set st c in card U holds
card (bool c) in U
proof end;

theorem :: CLASSES5:72
for U being Universe
for c1, c2 being Cardinal st c1 in card U & c2 in card U holds
card (bool [:c1,c2:]) in U
proof end;

definition
let x be object ;
func op0 x -> Element of {x} equals :: CLASSES5:def 19
x;
coherence
x is Element of {x} by TARSKI:def 1;
func op1 x -> UnOp of {x} equals :: CLASSES5:def 20
x .--> x;
coherence
x .--> x is UnOp of {x} ;
func op2 x -> BinOp of {x} equals :: CLASSES5:def 21
(x,x) :-> x;
coherence
(x,x) :-> x is BinOp of {x} ;
end;

:: deftheorem defines op0 CLASSES5:def 19 :
for x being object holds op0 x = x;

:: deftheorem defines op1 CLASSES5:def 20 :
for x being object holds op1 x = x .--> x;

:: deftheorem defines op2 CLASSES5:def 21 :
for x being object holds op2 x = (x,x) :-> x;

theorem :: CLASSES5:73
( op0 0 = op0 & op1 0 = op1 & op2 0 = op2 ) by FUNCT_5:def 5, FUNCT_5:def 6;

definition
let x be object ;
func Trivial-addLoopStr x -> non empty addLoopStr equals :: CLASSES5:def 22
 addLoopStr(# {x},(op2 x),(op0 x) #);
coherence
addLoopStr(# {x},(op2 x),(op0 x) #) is non empty addLoopStr ;
end;

:: deftheorem defines Trivial-addLoopStr CLASSES5:def 22 :
for x being object holds Trivial-addLoopStr x = addLoopStr(# {x},(op2 x),(op0 x) #);

theorem :: CLASSES5:74
Trivial-addLoopStr = Trivial-addLoopStr 0 by FUNCT_5:def 6, ALGSTR_0:def 9;

theorem :: CLASSES5:75
for x being object holds Trivial-addLoopStr x is strict AddGroup ;

theorem Th78: :: CLASSES5:76
for U being Universe
for x being Element of U holds
( op0 x is Element of U & op1 x is Element of U & op2 x is Element of U )
proof end;

theorem Th79: :: CLASSES5:77
for U being Universe
for x being Element of U holds comp (Trivial-addLoopStr x) is Element of U
proof end;

theorem Th80: :: CLASSES5:78
for U being Universe
for x being Element of U ex y being Element of U st GO y, Trivial-addLoopStr x
proof end;

theorem :: CLASSES5:79
for U being Universe holds union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } = U
proof end;

theorem Th82: :: CLASSES5:80
for U being Universe
for x being Element of U holds Trivial-addLoopStr x in GroupObjects U
proof end;

theorem Th83: :: CLASSES5:81
for U being Universe holds GroupObjects U,U are_equipotent
proof end;

theorem :: CLASSES5:82
for U being Universe holds not GroupObjects U is U -petit
proof end;

definition
let C be Category;
func CatToSet C -> set equals :: CLASSES5:def 23
[ the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C];
coherence
[ the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C] is set ;
end;

:: deftheorem defines CatToSet CLASSES5:def 23 :
for C being Category holds CatToSet C = [ the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C];

definition
let C be quintuple set ;
attr C is StrCategory-like means :Def25: :: CLASSES5:def 24
 ex y1, y2, y3, y4, y5 being set st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & y3 is Function of y2,y1 & y4 is Function of y2,y1 & y5 is PartFunc of [:y2,y2:],y2 );
end;

:: deftheorem Def25 defines StrCategory-like CLASSES5:def 24 :
for C being quintuple set holds
( C is StrCategory-like iff ex y1, y2, y3, y4, y5 being set st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & y3 is Function of y2,y1 & y4 is Function of y2,y1 & y5 is PartFunc of [:y2,y2:],y2 ) );

registration
cluster quintuple StrCategory-like for set ;
existence
ex b1 being quintuple set st b1 is StrCategory-like
proof end;
end;

definition
let C be quintuple StrCategory-like set ;
func SetToCat C -> strict CatStr means :: CLASSES5:def 25
 ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & it = CatStr(# y1,y2,y3,y4,y5 #) );
existence
ex b1 being strict CatStr ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b1 = CatStr(# y1,y2,y3,y4,y5 #) )
proof end;
uniqueness
for b1, b2 being strict CatStr st ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b1 = CatStr(# y1,y2,y3,y4,y5 #) ) & ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b2 = CatStr(# y1,y2,y3,y4,y5 #) ) holds
b1 = b2 ;
end;

:: deftheorem defines SetToCat CLASSES5:def 25 :
for C being quintuple StrCategory-like set
for b2 being strict CatStr holds
( b2 = SetToCat C iff ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b2 = CatStr(# y1,y2,y3,y4,y5 #) ) );

definition
let C be quintuple StrCategory-like set ;
attr C is Category-like means :Def27: :: CLASSES5:def 26
 ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & CatStr(# y1,y2,y3,y4,y5 #) is Category );
end;

:: deftheorem Def27 defines Category-like CLASSES5:def 26 :
for C being quintuple StrCategory-like set holds
( C is Category-like iff ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & CatStr(# y1,y2,y3,y4,y5 #) is Category ) );

registration
cluster quintuple StrCategory-like Category-like for set ;
existence
ex b1 being quintuple StrCategory-like set st b1 is Category-like
proof end;
end;

registration
cluster non empty quintuple StrCategory-like Category-like for set ;
existence
ex b1 being quintuple StrCategory-like set st
( not b1 is empty & b1 is Category-like )
proof end;
end;

definition
let C be quintuple StrCategory-like Category-like set ;
func Obj C -> set equals :: CLASSES5:def 27
C `1 ;
coherence
C `1 is set by TARSKI:1;
end;

:: deftheorem defines Obj CLASSES5:def 27 :
for C being quintuple StrCategory-like Category-like set holds Obj C = C `1 ;

definition
let C be quintuple StrCategory-like Category-like set ;
func Mor C -> set equals :: CLASSES5:def 28
C `2 ;
coherence
C `2 is set by TARSKI:1;
end;

:: deftheorem defines Mor CLASSES5:def 28 :
for C being quintuple StrCategory-like Category-like set holds Mor C = C `2 ;

definition
let C be quintuple StrCategory-like Category-like set ;
attr C is non-empty means :: CLASSES5:def 29
 not Obj C is empty ;
end;

:: deftheorem defines non-empty CLASSES5:def 29 :
for C being quintuple StrCategory-like Category-like set holds
( C is non-empty iff not Obj C is empty );

registration
cluster quintuple StrCategory-like Category-like non-empty for set ;
existence
ex b1 being quintuple StrCategory-like Category-like set st b1 is non-empty
proof end;
end;

definition
mode CategorySet is quintuple StrCategory-like Category-like non-empty set ;
end;

theorem Th85: :: CLASSES5:83
for C being CategorySet holds not C is empty
proof end;

registration
cluster quintuple StrCategory-like Category-like non-empty -> non empty for set ;
correctness
coherence
for b1 being CategorySet holds not b1 is empty ;
by Th85;
end;

definition
let C be CategorySet;
func SetToCat C -> strict Category means :Def31: :: CLASSES5:def 30
 ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & it = CatStr(# y1,y2,y3,y4,y5 #) );
existence
ex b1 being strict Category ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b1 = CatStr(# y1,y2,y3,y4,y5 #) )
proof end;
uniqueness
for b1, b2 being strict Category st ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b1 = CatStr(# y1,y2,y3,y4,y5 #) ) & ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b2 = CatStr(# y1,y2,y3,y4,y5 #) ) holds
b1 = b2 ;
end;

:: deftheorem Def31 defines SetToCat CLASSES5:def 30 :
for C being CategorySet
for b2 being strict Category holds
( b2 = SetToCat C iff ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b2 = CatStr(# y1,y2,y3,y4,y5 #) ) );

definition
let C be strict Category;
:: original: CatToSet
redefine func CatToSet C -> CategorySet;
coherence
CatToSet C is CategorySet
proof end;
end;

theorem Th86: :: CLASSES5:84
for C being CategorySet holds CatToSet (SetToCat C) = C
proof end;

theorem Th87: :: CLASSES5:85
for C being strict Category holds SetToCat (CatToSet C) = C
proof end;

theorem Th88: :: CLASSES5:86
for U being Universe
for C being Category holds
( C is U -element iff CatToSet C is U -set )
proof end;

theorem Th89: :: CLASSES5:87
for U being Universe
for C being CategorySet holds
( C is U -set iff SetToCat C is U -element )
proof end;

definition
let C, D be CategorySet;
pred C ~= D means :: CLASSES5:def 31
 SetToCat C ~= SetToCat D;
end;

:: deftheorem defines ~= CLASSES5:def 31 :
for C, D being CategorySet holds
( C ~= D iff SetToCat C ~= SetToCat D );

theorem Th90: :: CLASSES5:88
for C, D being strict Category st C ~= D holds
CatToSet C ~= CatToSet D
proof end;

definition
let U be Universe;
let C be CategorySet;
attr C is U -petit means :: CLASSES5:def 32
 ex c being CategorySet st
( c is U -set & C ~= c );
end;

:: deftheorem defines -petit CLASSES5:def 32 :
for U being Universe
for C being CategorySet holds
( C is U -petit iff ex c being CategorySet st
( c is U -set & C ~= c ) );

theorem :: CLASSES5:89
for U being Universe
for C being strict Category holds
( C is U -petit iff CatToSet C is U -petit )
proof end;

definition
let C, D be CategorySet;
func Funct (C,D) -> set equals :: CLASSES5:def 33
 Funct ((SetToCat C),(SetToCat D));
coherence
Funct ((SetToCat C),(SetToCat D)) is set ;
end;

:: deftheorem defines Funct CLASSES5:def 33 :
for C, D being CategorySet holds Funct (C,D) = Funct ((SetToCat C),(SetToCat D));

definition
let C, D be CategorySet;
func Functors (C,D) -> CategorySet equals :: CLASSES5:def 34
 CatToSet (Functors ((SetToCat C),(SetToCat D)));
coherence
CatToSet (Functors ((SetToCat C),(SetToCat D))) is CategorySet ;
end;

:: deftheorem defines Functors CLASSES5:def 34 :
for C, D being CategorySet holds Functors (C,D) = CatToSet (Functors ((SetToCat C),(SetToCat D)));

theorem :: CLASSES5:90
for C, D being CategorySet holds
( Obj (Functors (C,D)) = Funct ((SetToCat C),(SetToCat D)) & Mor (Functors (C,D)) = NatTrans ((SetToCat C),(SetToCat D)) ) by NATTRA_1:def 17;

:: WP: PROP 1.1.1 a) SGA4
theorem :: CLASSES5:91
for U being Universe
for C, D being CategorySet st C is U -set & D is U -set holds
Functors (C,D) is U -set
proof end;

notation
let U be Universe;
let C be Category;
synonym U -small C for U -element ;
end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -small for CatStr ;
existence
ex b1 being Category st b1 is U -small
proof end;
end;

theorem Th94: :: CLASSES5:92
for U being Universe
for o, m being set st ( not m is U -set or not o is U -set ) holds
not 1Cat (o,m) is U -small
proof end;

theorem :: CLASSES5:93
for U being Universe
for o, m being object st 1Cat (o,m) is U -small holds
( m is U -set & o is U -set )
proof end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities non U -small for CatStr ;
existence
not for b1 being Category holds b1 is U -small
proof end;
end;

definition
let U be Universe;
let C be Category;
attr C is U -locally_small means :Def36: :: CLASSES5:def 35
 for x, y being Object of C holds Hom (x,y) is U -set ;
end;

:: deftheorem Def36 defines -locally_small CLASSES5:def 35 :
for U being Universe
for C being Category holds
( C is U -locally_small iff for x, y being Object of C holds Hom (x,y) is U -set );

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -locally_small for CatStr ;
existence
ex b1 being Category st b1 is U -locally_small
proof end;
end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities U -locally_small for CatStr ;
existence
ex b1 being Category st b1 is U -locally_small
proof end;
end;

theorem Th96: :: CLASSES5:94
for U being Universe
for C being b1 -small Category holds C is U -locally_small
proof end;

theorem Th97: :: CLASSES5:95
for U being Universe
for o being object holds not 1Cat (o,U) is U -locally_small
proof end;

registration
let U be Universe;
cluster non empty non void feasible Category-like transitive associative reflexive with_identities non U -locally_small for CatStr ;
existence
not for b1 being Category holds b1 is U -locally_small
proof end;
end;

theorem Th98: :: CLASSES5:96
for U being Universe
for C being b1 -locally_small Category st the carrier of C is U -set holds
union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U
proof end;

::https://ncatlab.org/nlab/show/locally+small+category
theorem :: CLASSES5:97
for U being Universe
for C being b1 -locally_small Category st the carrier of C is U -set holds
C is U -small
proof end;

theorem :: CLASSES5:98
for U being Universe
for C, D being b1 -small Category holds
( Functors (C,D) is U -small & NatTrans (C,D) is U -set )
proof end;

theorem :: CLASSES5:99
for U being Universe
for C being b1 -small Category holds C opp is b1 -small Category
proof end;

theorem :: CLASSES5:100
for U being Universe
for C being b1 -locally_small Category holds C opp is b1 -locally_small Category
proof end;

definition
let X be set ;
:: original: id
redefine func id X -> Element of Funcs (X,X);
coherence
id X is Element of Funcs (X,X)
proof end;
end;

theorem Th103: :: CLASSES5:101
for U being Universe holds Funcs U c< U
proof end;

theorem Th104: :: CLASSES5:102
for U being Universe holds Funcs U is U -Class
proof end;

theorem :: CLASSES5:103
for U being Universe holds [:U,U:] \ [:(U \ {{}}),{{}}:] is not Element of U
proof end;

theorem Th106: :: CLASSES5:104
for U being Universe holds
( proj1 (Maps U) c= [:U,U:] & [:U,U:] \ [:(U \ {{}}),{{}}:] c= proj1 (Maps U) & proj2 (Maps U) = Funcs U )
proof end;

theorem Th107: :: CLASSES5:105
for U being Universe holds Maps U c= U
proof end;

theorem Th108: :: CLASSES5:106
for U being Universe holds the carrier' of (Ens U) is U -Class
proof end;

theorem Th109: :: CLASSES5:107
for U being Universe holds
( Ens U is non b1 -small Category & the carrier of (Ens U) is U -Class & the carrier' of (Ens U) is U -Class )
proof end;

theorem :: CLASSES5:108
for U, V being Universe st U in V holds
Ens U is b2 -small Category
proof end;

definition
let AbG be AbGroup;
func # AbG -> Function of [: the carrier of AbG, the carrier of AbG:], the carrier of AbG equals :: CLASSES5:def 36
 the addF of AbG;
coherence
the addF of AbG is Function of [: the carrier of AbG, the carrier of AbG:], the carrier of AbG ;
end;

:: deftheorem defines # CLASSES5:def 36 :
for AbG being AbGroup holds # AbG = the addF of AbG;

definition
let K be Field;
let o be object ;
let n be Nat;
func nMatrixFieldCat (K,o,n) -> non empty non void strict CatStr equals :: CLASSES5:def 37
 CatStr(# {o}, the carrier of (n -G_Matrix_over K),( the carrier of (n -G_Matrix_over K) --> o),( the carrier of (n -G_Matrix_over K) --> o),(# (n -G_Matrix_over K)) #);
coherence
CatStr(# {o}, the carrier of (n -G_Matrix_over K),( the carrier of (n -G_Matrix_over K) --> o),( the carrier of (n -G_Matrix_over K) --> o),(# (n -G_Matrix_over K)) #) is non empty non void strict CatStr ;
end;

:: deftheorem defines nMatrixFieldCat CLASSES5:def 37 :
for K being Field
for o being object
for n being Nat holds nMatrixFieldCat (K,o,n) = CatStr(# {o}, the carrier of (n -G_Matrix_over K),( the carrier of (n -G_Matrix_over K) --> o),( the carrier of (n -G_Matrix_over K) --> o),(# (n -G_Matrix_over K)) #);

registration
let K be Field;
let o be object ;
let n be Nat;
cluster nMatrixFieldCat (K,o,n) -> non empty non void strict Category-like ;
coherence
nMatrixFieldCat (K,o,n) is Category-like
proof end;
end;

registration
let K be Field;
let o be object ;
let n be Nat;
cluster nMatrixFieldCat (K,o,n) -> non empty non void strict transitive ;
coherence
nMatrixFieldCat (K,o,n) is transitive
proof end;
end;

registration
let K be Field;
let o be object ;
let n be Nat;
cluster nMatrixFieldCat (K,o,n) -> non empty non void strict associative ;
coherence
nMatrixFieldCat (K,o,n) is associative
proof end;
end;

registration
let K be Field;
let o be object ;
let n be Nat;
cluster nMatrixFieldCat (K,o,n) -> non empty non void strict reflexive ;
coherence
nMatrixFieldCat (K,o,n) is reflexive
proof end;
end;

registration
let K be Field;
let o be object ;
let n be Nat;
cluster nMatrixFieldCat (K,o,n) -> non empty non void strict with_identities ;
coherence
nMatrixFieldCat (K,o,n) is with_identities
proof end;
end;

theorem Th111: :: CLASSES5:109
for U being Universe
for K being Field
for o being Element of U
for n being non zero Nat st the carrier of K is Element of U holds
( the carrier of (nMatrixFieldCat (K,o,n)) is trivial & nMatrixFieldCat (K,o,n) is b1 -small Category & nMatrixFieldCat (K,o,n) is b1 -locally_small Category )
proof end;

theorem :: CLASSES5:110
for o being Element of FinSETS
for n being non zero Nat holds
( the carrier of (nMatrixFieldCat (F_Real,o,n)) is trivial & the carrier of (nMatrixFieldCat (F_Real,o,n)) is FinSETS -set & nMatrixFieldCat (F_Real,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Real,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Real,o,n) is SETS -small Category & nMatrixFieldCat (F_Real,o,n) is SETS -locally_small Category )
proof end;

theorem :: CLASSES5:111
for o being Element of FinSETS
for n being non zero Nat holds
( the carrier of (nMatrixFieldCat (F_Complex,o,n)) is trivial & the carrier of (nMatrixFieldCat (F_Complex,o,n)) is FinSETS -set & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
proof end;