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 𝐷 = ( 𝐶cat 𝐻 )
rescbas.b 𝐵 = ( Base ‘ 𝐶 )
rescbas.c ( 𝜑𝐶𝑉 )
rescbas.h ( 𝜑𝐻 Fn ( 𝑆 × 𝑆 ) )
rescbas.s ( 𝜑𝑆𝐵 )
rescco.o · = ( comp ‘ 𝐶 )
Assertion resccoOLD ( 𝜑· = ( comp ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 rescbas.d 𝐷 = ( 𝐶cat 𝐻 )
2 rescbas.b 𝐵 = ( Base ‘ 𝐶 )
3 rescbas.c ( 𝜑𝐶𝑉 )
4 rescbas.h ( 𝜑𝐻 Fn ( 𝑆 × 𝑆 ) )
5 rescbas.s ( 𝜑𝑆𝐵 )
6 rescco.o · = ( comp ‘ 𝐶 )
7 ccoid comp = Slot ( comp ‘ ndx )
8 1nn0 1 ∈ ℕ0
9 4nn 4 ∈ ℕ
10 8 9 decnncl 1 4 ∈ ℕ
11 10 nnrei 1 4 ∈ ℝ
12 4nn0 4 ∈ ℕ0
13 5nn 5 ∈ ℕ
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 ‘ ( 𝐶s 𝑆 ) ) = ( comp ‘ ( ( 𝐶s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
22 2 fvexi 𝐵 ∈ V
23 22 ssex ( 𝑆𝐵𝑆 ∈ V )
24 5 23 syl ( 𝜑𝑆 ∈ V )
25 eqid ( 𝐶s 𝑆 ) = ( 𝐶s 𝑆 )
26 25 6 ressco ( 𝑆 ∈ V → · = ( comp ‘ ( 𝐶s 𝑆 ) ) )
27 24 26 syl ( 𝜑· = ( comp ‘ ( 𝐶s 𝑆 ) ) )
28 1 3 24 4 rescval2 ( 𝜑𝐷 = ( ( 𝐶s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
29 28 fveq2d ( 𝜑 → ( comp ‘ 𝐷 ) = ( comp ‘ ( ( 𝐶s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
30 21 27 29 3eqtr4a ( 𝜑· = ( comp ‘ 𝐷 ) )