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 
|- D = ( C |`cat H )
rescbas.b 
|- B = ( Base ` C )
rescbas.c 
|- ( ph -> C e. V )
rescbas.h 
|- ( ph -> H Fn ( S X. S ) )
rescbas.s 
|- ( ph -> S C_ B )
Assertion rescbas 
|- ( ph -> S = ( Base ` D ) )

Proof

Step Hyp Ref Expression
1 rescbas.d 
 |-  D = ( C |`cat H )
2 rescbas.b 
 |-  B = ( Base ` C )
3 rescbas.c 
 |-  ( ph -> C e. V )
4 rescbas.h 
 |-  ( ph -> H Fn ( S X. S ) )
5 rescbas.s 
 |-  ( ph -> S C_ B )
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 ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
10 eqid 
 |-  ( C |`s S ) = ( C |`s S )
11 10 2 ressbas2 
 |-  ( S C_ B -> S = ( Base ` ( C |`s S ) ) )
12 5 11 syl 
 |-  ( ph -> S = ( Base ` ( C |`s S ) ) )
13 2 fvexi 
 |-  B e. _V
14 13 ssex 
 |-  ( S C_ B -> S e. _V )
15 5 14 syl 
 |-  ( ph -> S e. _V )
16 1 3 15 4 rescval2 
 |-  ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
17 16 fveq2d 
 |-  ( ph -> ( Base ` D ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
18 9 12 17 3eqtr4a 
 |-  ( ph -> S = ( Base ` D ) )