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 φ C V
rescbas.h φ H Fn S × S
rescbas.s φ S B
rescco.o · ˙ = comp C
Assertion resccoOLD φ · ˙ = comp D

Proof

Step Hyp Ref Expression
1 rescbas.d D = C cat H
2 rescbas.b B = Base C
3 rescbas.c φ C V
4 rescbas.h φ H Fn S × S
5 rescbas.s φ S B
6 rescco.o · ˙ = comp C
7 ccoid comp = Slot comp ndx
8 1nn0 1 0
9 4nn 4
10 8 9 decnncl 14
11 10 nnrei 14
12 4nn0 4 0
13 5nn 5
14 4lt5 4 < 5
15 8 12 13 14 declt 14 < 15
16 11 15 gtneii 15 14
17 ccondx comp ndx = 15
18 homndx Hom ndx = 14
19 17 18 neeq12i comp ndx Hom ndx 15 14
20 16 19 mpbir comp ndx Hom ndx
21 7 20 setsnid comp C 𝑠 S = comp C 𝑠 S sSet Hom ndx H
22 2 fvexi B V
23 22 ssex S B S V
24 5 23 syl φ S V
25 eqid C 𝑠 S = C 𝑠 S
26 25 6 ressco S V · ˙ = comp C 𝑠 S
27 24 26 syl φ · ˙ = comp C 𝑠 S
28 1 3 24 4 rescval2 φ D = C 𝑠 S sSet Hom ndx H
29 28 fveq2d φ comp D = comp C 𝑠 S sSet Hom ndx H
30 21 27 29 3eqtr4a φ · ˙ = comp D