Metamath Proof Explorer


Theorem estrres

Description: Any restriction of a category (as an extensible structure which is an unordered triple of ordered pairs) is an unordered triple of ordered pairs. (Contributed by AV, 15-Mar-2020) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses estrres.c φ C = Base ndx B Hom ndx H comp ndx · ˙
estrres.b φ B V
estrres.h φ H X
estrres.x φ · ˙ Y
estrres.g φ G W
estrres.u φ A B
Assertion estrres φ C 𝑠 A sSet Hom ndx G = Base ndx A Hom ndx G comp ndx · ˙

Proof

Step Hyp Ref Expression
1 estrres.c φ C = Base ndx B Hom ndx H comp ndx · ˙
2 estrres.b φ B V
3 estrres.h φ H X
4 estrres.x φ · ˙ Y
5 estrres.g φ G W
6 estrres.u φ A B
7 ovex C 𝑠 A V
8 setsval C 𝑠 A V G W C 𝑠 A sSet Hom ndx G = C 𝑠 A V Hom ndx Hom ndx G
9 7 5 8 sylancr φ C 𝑠 A sSet Hom ndx G = C 𝑠 A V Hom ndx Hom ndx G
10 eqid C 𝑠 A = C 𝑠 A
11 eqid Base C = Base C
12 eqid Base ndx = Base ndx
13 tpex Base ndx B Hom ndx H comp ndx · ˙ V
14 1 13 eqeltrdi φ C V
15 fvex Base ndx V
16 fvex Hom ndx V
17 fvex comp ndx V
18 15 16 17 3pm3.2i Base ndx V Hom ndx V comp ndx V
19 18 a1i φ Base ndx V Hom ndx V comp ndx V
20 slotsbhcdif Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx
21 20 a1i φ Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx
22 funtpg Base ndx V Hom ndx V comp ndx V B V H X · ˙ Y Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx Fun Base ndx B Hom ndx H comp ndx · ˙
23 19 2 3 4 21 22 syl131anc φ Fun Base ndx B Hom ndx H comp ndx · ˙
24 1 funeqd φ Fun C Fun Base ndx B Hom ndx H comp ndx · ˙
25 23 24 mpbird φ Fun C
26 1 2 3 4 estrreslem2 φ Base ndx dom C
27 1 2 estrreslem1 φ B = Base C
28 6 27 sseqtrd φ A Base C
29 10 11 12 14 25 26 28 ressval3d φ C 𝑠 A = C sSet Base ndx A
30 29 reseq1d φ C 𝑠 A V Hom ndx = C sSet Base ndx A V Hom ndx
31 30 uneq1d φ C 𝑠 A V Hom ndx Hom ndx G = C sSet Base ndx A V Hom ndx Hom ndx G
32 2 6 ssexd φ A V
33 setsval C V A V C sSet Base ndx A = C V Base ndx Base ndx A
34 14 32 33 syl2anc φ C sSet Base ndx A = C V Base ndx Base ndx A
35 34 reseq1d φ C sSet Base ndx A V Hom ndx = C V Base ndx Base ndx A V Hom ndx
36 fvexd φ Hom ndx V
37 fvexd φ comp ndx V
38 3 elexd φ H V
39 4 elexd φ · ˙ V
40 simp1 Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx Base ndx Hom ndx
41 40 necomd Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx Hom ndx Base ndx
42 20 41 mp1i φ Hom ndx Base ndx
43 simp2 Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx Base ndx comp ndx
44 43 necomd Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx comp ndx Base ndx
45 20 44 mp1i φ comp ndx Base ndx
46 1 36 37 38 39 42 45 tpres φ C V Base ndx = Hom ndx H comp ndx · ˙
47 46 uneq1d φ C V Base ndx Base ndx A = Hom ndx H comp ndx · ˙ Base ndx A
48 df-tp Hom ndx H comp ndx · ˙ Base ndx A = Hom ndx H comp ndx · ˙ Base ndx A
49 47 48 eqtr4di φ C V Base ndx Base ndx A = Hom ndx H comp ndx · ˙ Base ndx A
50 fvexd φ Base ndx V
51 simp3 Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx Hom ndx comp ndx
52 51 necomd Base ndx Hom ndx Base ndx comp ndx Hom ndx comp ndx comp ndx Hom ndx
53 20 52 mp1i φ comp ndx Hom ndx
54 20 40 mp1i φ Base ndx Hom ndx
55 49 37 50 39 32 53 54 tpres φ C V Base ndx Base ndx A V Hom ndx = comp ndx · ˙ Base ndx A
56 35 55 eqtrd φ C sSet Base ndx A V Hom ndx = comp ndx · ˙ Base ndx A
57 56 uneq1d φ C sSet Base ndx A V Hom ndx Hom ndx G = comp ndx · ˙ Base ndx A Hom ndx G
58 df-tp comp ndx · ˙ Base ndx A Hom ndx G = comp ndx · ˙ Base ndx A Hom ndx G
59 tprot comp ndx · ˙ Base ndx A Hom ndx G = Base ndx A Hom ndx G comp ndx · ˙
60 58 59 eqtr3i comp ndx · ˙ Base ndx A Hom ndx G = Base ndx A Hom ndx G comp ndx · ˙
61 57 60 eqtrdi φ C sSet Base ndx A V Hom ndx Hom ndx G = Base ndx A Hom ndx G comp ndx · ˙
62 9 31 61 3eqtrd φ C 𝑠 A sSet Hom ndx G = Base ndx A Hom ndx G comp ndx · ˙