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 ⊢ ( 𝜑 → 𝐶 = { ⟨ ( 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 ) , · ⟩ } )