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	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
	estrres.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	estrres.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	estrres.x	⊢ ( 𝜑 → · ∈ 𝑌 )
	estrres.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	estrres.u	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	estrres	⊢ ( 𝜑 → ( ( 𝐶 ↾s 𝐴 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ ) = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		estrres.c	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
2		estrres.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		estrres.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
4		estrres.x	⊢ ( 𝜑 → · ∈ 𝑌 )
5		estrres.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
6		estrres.u	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
7		ovex	⊢ ( 𝐶 ↾s 𝐴 ) ∈ V
8		setsval	⊢ ( ( ( 𝐶 ↾s 𝐴 ) ∈ V ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐶 ↾s 𝐴 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ ) = ( ( ( 𝐶 ↾s 𝐴 ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) )
9	7 5 8	sylancr	⊢ ( 𝜑 → ( ( 𝐶 ↾s 𝐴 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ ) = ( ( ( 𝐶 ↾s 𝐴 ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) )
10		eqid	⊢ ( 𝐶 ↾s 𝐴 ) = ( 𝐶 ↾s 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12		eqid	⊢ ( Base ‘ ndx ) = ( Base ‘ ndx )
13		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
14	1 13	eqeltrdi	⊢ ( 𝜑 → 𝐶 ∈ 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 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐻 ∈ 𝑋 ∧ · ∈ 𝑌 ) ∧ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) ) → Fun { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
23	19 2 3 4 21 22	syl131anc	⊢ ( 𝜑 → Fun { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
24	1	funeqd	⊢ ( 𝜑 → ( Fun 𝐶 ↔ Fun { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ) )
25	23 24	mpbird	⊢ ( 𝜑 → Fun 𝐶 )
26	1 2 3 4	estrreslem2	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐶 )
27	1 2	estrreslem1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
28	6 27	sseqtrd	⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝐶 ) )
29	10 11 12 14 25 26 28	ressval3d	⊢ ( 𝜑 → ( 𝐶 ↾s 𝐴 ) = ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) )
30	29	reseq1d	⊢ ( 𝜑 → ( ( 𝐶 ↾s 𝐴 ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) = ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) )
31	30	uneq1d	⊢ ( 𝜑 → ( ( ( 𝐶 ↾s 𝐴 ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) = ( ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) )
32	2 6	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
33		setsval	⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) = ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) )
34	14 32 33	syl2anc	⊢ ( 𝜑 → ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) = ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) )
35	34	reseq1d	⊢ ( 𝜑 → ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) = ( ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) )
36		fvexd	⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ V )
37		fvexd	⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ V )
38	3	elexd	⊢ ( 𝜑 → 𝐻 ∈ 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	⊢ ( 𝜑 → ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) = { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
47	46	uneq1d	⊢ ( 𝜑 → ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) = ( { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) )
48		df-tp	⊢ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } = ( { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } )
49	47 48	eqtr4di	⊢ ( 𝜑 → ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) = { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } )
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	⊢ ( 𝜑 → ( ( ( 𝐶 ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) = { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } )
56	35 55	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) = { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } )
57	56	uneq1d	⊢ ( 𝜑 → ( ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) = ( { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) )
58		df-tp	⊢ { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } = ( { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } )
59		tprot	⊢ { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ }
60	58 59	eqtr3i	⊢ ( { ⟨ ( comp ‘ ndx ) , · ⟩ , ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ }
61	57 60	eqtrdi	⊢ ( 𝜑 → ( ( ( 𝐶 sSet ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ ) ↾ ( V ∖ { ( Hom ‘ ndx ) } ) ) ∪ { ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
62	9 31 61	3eqtrd	⊢ ( 𝜑 → ( ( 𝐶 ↾s 𝐴 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ ) = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐺 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )