Theorem rescco

Description: Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	rescbas.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
	rescbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	rescbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	rescbas.h	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	rescbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	rescco.o	⊢ · = ( comp ‘ 𝐶 )
Assertion	rescco	⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		rescbas.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2		rescbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rescbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		rescbas.h	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5		rescbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6		rescco.o	⊢ · = ( comp ‘ 𝐶 )
7		ccoid	⊢ comp = Slot ( comp ‘ ndx )
8		1nn0	⊢ 1 ∈ ℕ0
9		4nn	⊢ 4 ∈ ℕ
10	8 9	decnncl	⊢ ; 1 4 ∈ ℕ
11	10	nnrei	⊢ ; 1 4 ∈ ℝ
12		4nn0	⊢ 4 ∈ ℕ0
13		5nn	⊢ 5 ∈ ℕ
14		4lt5	⊢ 4 < 5
15	8 12 13 14	declt	⊢ ; 1 4 < ; 1 5
16	11 15	gtneii	⊢ ; 1 5 ≠ ; 1 4
17		ccondx	⊢ ( comp ‘ ndx ) = ; 1 5
18		homndx	⊢ ( Hom ‘ ndx ) = ; 1 4
19	17 18	neeq12i	⊢ ( ( comp ‘ ndx ) ≠ ( Hom ‘ ndx ) ↔ ; 1 5 ≠ ; 1 4 )
20	16 19	mpbir	⊢ ( comp ‘ ndx ) ≠ ( Hom ‘ ndx )
21	7 20	setsnid	⊢ ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) = ( comp ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
22	2	fvexi	⊢ 𝐵 ∈ V
23	22	ssex	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
24	5 23	syl	⊢ ( 𝜑 → 𝑆 ∈ V )
25		eqid	⊢ ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s 𝑆 )
26	25 6	ressco	⊢ ( 𝑆 ∈ V → · = ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) )
27	24 26	syl	⊢ ( 𝜑 → · = ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) )
28	1 3 24 4	rescval2	⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
29	28	fveq2d	⊢ ( 𝜑 → ( comp ‘ 𝐷 ) = ( comp ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
30	21 27 29	3eqtr4a	⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )