Metamath Proof Explorer

Theorem resccoOLD

Description: Obsolete proof of rescco as of 14-Oct-2024. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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 )
rescco.o 
|- .x. = ( comp ` C )
Assertion resccoOLD 
|- ( ph -> .x. = ( comp ` 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 rescco.o 
 |-  .x. = ( comp ` C )
7 ccoid 
 |-  comp = Slot ( comp ` ndx )
8 1nn0 
 |-  1 e. NN0
9 4nn 
 |-  4 e. NN
10 8 9 decnncl 
 |-  ; 1 4 e. NN
11 10 nnrei 
 |-  ; 1 4 e. RR
12 4nn0 
 |-  4 e. NN0
13 5nn 
 |-  5 e. NN
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 ` ( C |`s S ) ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
22 2 fvexi 
 |-  B e. _V
23 22 ssex 
 |-  ( S C_ B -> S e. _V )
24 5 23 syl 
 |-  ( ph -> S e. _V )
25 eqid 
 |-  ( C |`s S ) = ( C |`s S )
26 25 6 ressco 
 |-  ( S e. _V -> .x. = ( comp ` ( C |`s S ) ) )
27 24 26 syl 
 |-  ( ph -> .x. = ( comp ` ( C |`s S ) ) )
28 1 3 24 4 rescval2 
 |-  ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
29 28 fveq2d 
 |-  ( ph -> ( comp ` D ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
30 21 27 29 3eqtr4a 
 |-  ( ph -> .x. = ( comp ` D ) )