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	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
	estrres.b	$⊢ φ \to B \in V$
	estrres.h	$⊢ φ \to H \in X$
	estrres.x	$⊢ φ \to \underset{˙}{\cdot} \in Y$
	estrres.g	$⊢ φ \to G \in W$
	estrres.u	$⊢ φ \to A \subseteq B$
Assertion	estrres	$⊢ φ \to (C ↾_{𝑠} A) sSet ⟨Hom (ndx), G⟩ = \{⟨{Base}_{ndx}, A⟩, ⟨Hom (ndx), G⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

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

Metamath Proof Explorer

Theorem estrres

Proof