This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐷 ) )