Theorem catstr

Description: A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Assertion	catstr	|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } Struct <. 1 , ; 1 5 >.

Proof

Step	Hyp	Ref	Expression
1		1nn	|- 1 e. NN
2		basendx	|- ( Base ` ndx ) = 1
3		4nn0	|- 4 e. NN0
4		1nn0	|- 1 e. NN0
5		1lt10	|- 1 < ; 1 0
6	1 3 4 5	declti	|- 1 < ; 1 4
7		4nn	|- 4 e. NN
8	4 7	decnncl	|- ; 1 4 e. NN
9		homndx	|- ( Hom ` ndx ) = ; 1 4
10		5nn	|- 5 e. NN
11		4lt5	|- 4 < 5
12	4 3 10 11	declt	|- ; 1 4 < ; 1 5
13	4 10	decnncl	|- ; 1 5 e. NN
14		ccondx	|- ( comp ` ndx ) = ; 1 5
15	1 2 6 8 9 12 13 14	strle3	|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } Struct <. 1 , ; 1 5 >.