Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 18-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		rescbas.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2		rescbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rescbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		rescbas.h	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5		rescbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6		baseid	⊢ Base = Slot ( Base ‘ ndx )
7		slotsbhcdif	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
8	7	simp1i	⊢ ( Base ‘ ndx ) ≠ ( Hom ‘ ndx )
9	6 8	setsnid	⊢ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) = ( Base ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
10		eqid	⊢ ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s 𝑆 )
11	10 2	ressbas2	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) )
12	5 11	syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) )
13	2	fvexi	⊢ 𝐵 ∈ V
14	13	ssex	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
15	5 14	syl	⊢ ( 𝜑 → 𝑆 ∈ V )
16	1 3 15 4	rescval2	⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
17	16	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
18	9 12 17	3eqtr4a	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )