Theorem catstr

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

	Ref	Expression
Assertion	catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\mathrm{Struct}⟨1,15⟩$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		1lt10	$$⊢1<10$$
6	1 3 4 5	declti	$$⊢1<14$$
7		4nn	$$⊢4\in \mathbb{N}$$
8	4 7	decnncl	$$⊢14\in \mathbb{N}$$
9		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
10		5nn	$$⊢5\in \mathbb{N}$$
11		4lt5	$$⊢4<5$$
12	4 3 10 11	declt	$$⊢14<15$$
13	4 10	decnncl	$$⊢15\in \mathbb{N}$$
14		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
15	1 2 6 8 9 12 13 14	strle3	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\mathrm{Struct}⟨1,15⟩$$