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 
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
estrres.b 
|- ( ph -> B e. V )
estrres.h 
|- ( ph -> H e. X )
estrres.x 
|- ( ph -> .x. e. Y )
estrres.g 
|- ( ph -> G e. W )
estrres.u 
|- ( ph -> A C_ B )
Assertion estrres 
|- ( ph -> ( ( C |`s A ) sSet <. ( Hom ` ndx ) , G >. ) = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. ( comp ` ndx ) , .x. >. } )

Proof

Step Hyp Ref Expression
1 estrres.c 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
2 estrres.b 
 |-  ( ph -> B e. V )
3 estrres.h 
 |-  ( ph -> H e. X )
4 estrres.x 
 |-  ( ph -> .x. e. Y )
5 estrres.g 
 |-  ( ph -> G e. W )
6 estrres.u 
 |-  ( ph -> A C_ B )
7 ovex 
 |-  ( C |`s A ) e. _V
8 setsval 
 |-  ( ( ( C |`s A ) e. _V /\ G e. W ) -> ( ( C |`s A ) sSet <. ( Hom ` ndx ) , G >. ) = ( ( ( C |`s A ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) )
9 7 5 8 sylancr 
 |-  ( ph -> ( ( C |`s A ) sSet <. ( Hom ` ndx ) , G >. ) = ( ( ( C |`s A ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) )
10 eqid 
 |-  ( C |`s A ) = ( C |`s A )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( Base ` ndx ) = ( Base ` ndx )
13 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
14 1 13 eqeltrdi 
 |-  ( ph -> C e. _V )
15 fvex 
 |-  ( Base ` ndx ) e. _V
16 fvex 
 |-  ( Hom ` ndx ) e. _V
17 fvex 
 |-  ( comp ` ndx ) e. _V
18 15 16 17 3pm3.2i 
 |-  ( ( Base ` ndx ) e. _V /\ ( Hom ` ndx ) e. _V /\ ( comp ` ndx ) e. _V )
19 18 a1i 
 |-  ( ph -> ( ( Base ` ndx ) e. _V /\ ( Hom ` ndx ) e. _V /\ ( comp ` ndx ) e. _V ) )
20 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
21 20 a1i 
 |-  ( ph -> ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) )
22 funtpg 
 |-  ( ( ( ( Base ` ndx ) e. _V /\ ( Hom ` ndx ) e. _V /\ ( comp ` ndx ) e. _V ) /\ ( B e. V /\ H e. X /\ .x. e. Y ) /\ ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) ) -> Fun { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
23 19 2 3 4 21 22 syl131anc 
 |-  ( ph -> Fun { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
24 1 funeqd 
 |-  ( ph -> ( Fun C <-> Fun { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } ) )
25 23 24 mpbird 
 |-  ( ph -> Fun C )
26 1 2 3 4 estrreslem2 
 |-  ( ph -> ( Base ` ndx ) e. dom C )
27 1 2 estrreslem1 
 |-  ( ph -> B = ( Base ` C ) )
28 6 27 sseqtrd 
 |-  ( ph -> A C_ ( Base ` C ) )
29 10 11 12 14 25 26 28 ressval3d 
 |-  ( ph -> ( C |`s A ) = ( C sSet <. ( Base ` ndx ) , A >. ) )
30 29 reseq1d 
 |-  ( ph -> ( ( C |`s A ) |` ( _V \ { ( Hom ` ndx ) } ) ) = ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) )
31 30 uneq1d 
 |-  ( ph -> ( ( ( C |`s A ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) = ( ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) )
32 2 6 ssexd 
 |-  ( ph -> A e. _V )
33 setsval 
 |-  ( ( C e. _V /\ A e. _V ) -> ( C sSet <. ( Base ` ndx ) , A >. ) = ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) )
34 14 32 33 syl2anc 
 |-  ( ph -> ( C sSet <. ( Base ` ndx ) , A >. ) = ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) )
35 34 reseq1d 
 |-  ( ph -> ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) = ( ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) |` ( _V \ { ( Hom ` ndx ) } ) ) )
36 fvexd 
 |-  ( ph -> ( Hom ` ndx ) e. _V )
37 fvexd 
 |-  ( ph -> ( comp ` ndx ) e. _V )
38 3 elexd 
 |-  ( ph -> H e. _V )
39 4 elexd 
 |-  ( ph -> .x. e. _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 
 |-  ( ph -> ( 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 
 |-  ( ph -> ( comp ` ndx ) =/= ( Base ` ndx ) )
46 1 36 37 38 39 42 45 tpres 
 |-  ( ph -> ( C |` ( _V \ { ( Base ` ndx ) } ) ) = { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
47 46 uneq1d 
 |-  ( ph -> ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) = ( { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } u. { <. ( Base ` ndx ) , A >. } ) )
48 df-tp 
 |-  { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } = ( { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } u. { <. ( Base ` ndx ) , A >. } )
49 47 48 eqtr4di 
 |-  ( ph -> ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) = { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } )
50 fvexd 
 |-  ( ph -> ( Base ` ndx ) e. _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 
 |-  ( ph -> ( comp ` ndx ) =/= ( Hom ` ndx ) )
54 20 40 mp1i 
 |-  ( ph -> ( Base ` ndx ) =/= ( Hom ` ndx ) )
55 49 37 50 39 32 53 54 tpres 
 |-  ( ph -> ( ( ( C |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , A >. } ) |` ( _V \ { ( Hom ` ndx ) } ) ) = { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } )
56 35 55 eqtrd 
 |-  ( ph -> ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) = { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } )
57 56 uneq1d 
 |-  ( ph -> ( ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) = ( { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } u. { <. ( Hom ` ndx ) , G >. } ) )
58 df-tp 
 |-  { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. } = ( { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } u. { <. ( Hom ` ndx ) , G >. } )
59 tprot 
 |-  { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. } = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. ( comp ` ndx ) , .x. >. }
60 58 59 eqtr3i 
 |-  ( { <. ( comp ` ndx ) , .x. >. , <. ( Base ` ndx ) , A >. } u. { <. ( Hom ` ndx ) , G >. } ) = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. ( comp ` ndx ) , .x. >. }
61 57 60 eqtrdi 
 |-  ( ph -> ( ( ( C sSet <. ( Base ` ndx ) , A >. ) |` ( _V \ { ( Hom ` ndx ) } ) ) u. { <. ( Hom ` ndx ) , G >. } ) = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. ( comp ` ndx ) , .x. >. } )
62 9 31 61 3eqtrd 
 |-  ( ph -> ( ( C |`s A ) sSet <. ( Hom ` ndx ) , G >. ) = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. ( comp ` ndx ) , .x. >. } )