# 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
estrres.b ${⊢}{\phi }\to {B}\in {V}$
estrres.h ${⊢}{\phi }\to {H}\in {X}$
estrres.x
estrres.g ${⊢}{\phi }\to {G}\in {W}$
estrres.u ${⊢}{\phi }\to {A}\subseteq {B}$
Assertion estrres

### Proof

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