Theorem catstr

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

	Ref	Expression
Assertion	catstr	⊢ { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } Struct ⟨ 1 , ; 1 5 ⟩

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		basendx	⊢ ( Base ‘ ndx ) = 1
3		4nn0	⊢ 4 ∈ ℕ0
4		1nn0	⊢ 1 ∈ ℕ0
5		1lt10	⊢ 1 < ; 1 0
6	1 3 4 5	declti	⊢ 1 < ; 1 4
7		4nn	⊢ 4 ∈ ℕ
8	4 7	decnncl	⊢ ; 1 4 ∈ ℕ
9		homndx	⊢ ( Hom ‘ ndx ) = ; 1 4
10		5nn	⊢ 5 ∈ ℕ
11		4lt5	⊢ 4 < 5
12	4 3 10 11	declt	⊢ ; 1 4 < ; 1 5
13	4 10	decnncl	⊢ ; 1 5 ∈ ℕ
14		ccondx	⊢ ( comp ‘ ndx ) = ; 1 5
15	1 2 6 8 9 12 13 14	strle3	⊢ { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } Struct ⟨ 1 , ; 1 5 ⟩