Metamath Proof Explorer


Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

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 1re
 |-  1 e. RR
8 1nn
 |-  1 e. NN
9 4nn0
 |-  4 e. NN0
10 1nn0
 |-  1 e. NN0
11 1lt10
 |-  1 < ; 1 0
12 8 9 10 11 declti
 |-  1 < ; 1 4
13 7 12 ltneii
 |-  1 =/= ; 1 4
14 basendx
 |-  ( Base ` ndx ) = 1
15 homndx
 |-  ( Hom ` ndx ) = ; 1 4
16 14 15 neeq12i
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) <-> 1 =/= ; 1 4 )
17 13 16 mpbir
 |-  ( Base ` ndx ) =/= ( Hom ` ndx )
18 6 17 setsnid
 |-  ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
19 eqid
 |-  ( C |`s S ) = ( C |`s S )
20 19 2 ressbas2
 |-  ( S C_ B -> S = ( Base ` ( C |`s S ) ) )
21 5 20 syl
 |-  ( ph -> S = ( Base ` ( C |`s S ) ) )
22 2 fvexi
 |-  B e. _V
23 22 ssex
 |-  ( S C_ B -> S e. _V )
24 5 23 syl
 |-  ( ph -> S e. _V )
25 1 3 24 4 rescval2
 |-  ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
26 25 fveq2d
 |-  ( ph -> ( Base ` D ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
27 18 21 26 3eqtr4a
 |-  ( ph -> S = ( Base ` D ) )