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), \underset{˙}{\cdot}⟩\} Struct ⟨1, 15⟩$

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

Metamath Proof Explorer