This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 9-Nov-2024)

Ref Expression
Hypotheses rescabs.c 
|- ( ph -> C e. V )
rescabs.h 
|- ( ph -> H Fn ( S X. S ) )
rescabs.j 
|- ( ph -> J Fn ( T X. T ) )
rescabs.s 
|- ( ph -> S e. W )
rescabs.t 
|- ( ph -> T C_ S )
Assertion rescabs 
|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )

Proof

Step Hyp Ref Expression
1 rescabs.c 
 |-  ( ph -> C e. V )
2 rescabs.h 
 |-  ( ph -> H Fn ( S X. S ) )
3 rescabs.j 
 |-  ( ph -> J Fn ( T X. T ) )
4 rescabs.s 
 |-  ( ph -> S e. W )
5 rescabs.t 
 |-  ( ph -> T C_ S )
6 eqid 
 |-  ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J )
7 ovexd 
 |-  ( ph -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
8 4 5 ssexd 
 |-  ( ph -> T e. _V )
9 6 7 8 3 rescval2 
 |-  ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
10 simpr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( Base ` ( C |`s S ) ) C_ T )
11 ovexd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
12 8 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
13 eqid 
 |-  ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T )
14 baseid 
 |-  Base = Slot ( Base ` ndx )
15 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
16 15 simp1i 
 |-  ( Base ` ndx ) =/= ( Hom ` ndx )
17 14 16 setsnid 
 |-  ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
18 13 17 ressid2 
 |-  ( ( ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
19 10 11 12 18 syl3anc 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
20 19 oveq1d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
21 ovex 
 |-  ( C |`s S ) e. _V
22 8 8 xpexd 
 |-  ( ph -> ( T X. T ) e. _V )
23 3 22 fnexd 
 |-  ( ph -> J e. _V )
24 23 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
25 setsabs 
 |-  ( ( ( C |`s S ) e. _V /\ J e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
26 21 24 25 sylancr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
27 eqid 
 |-  ( C |`s S ) = ( C |`s S )
28 eqid 
 |-  ( Base ` C ) = ( Base ` C )
29 27 28 ressbas 
 |-  ( S e. W -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
30 4 29 syl 
 |-  ( ph -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
31 30 sseq1d 
 |-  ( ph -> ( ( S i^i ( Base ` C ) ) C_ T <-> ( Base ` ( C |`s S ) ) C_ T ) )
32 31 biimpar 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ T )
33 inss2 
 |-  ( S i^i ( Base ` C ) ) C_ ( Base ` C )
34 33 a1i 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( Base ` C ) )
35 32 34 ssind 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( T i^i ( Base ` C ) ) )
36 5 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
37 36 ssrind 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` C ) ) C_ ( S i^i ( Base ` C ) ) )
38 35 37 eqssd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) = ( T i^i ( Base ` C ) ) )
39 38 oveq2d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s ( S i^i ( Base ` C ) ) ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
40 4 adantr 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
41 28 ressinbas 
 |-  ( S e. W -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
42 40 41 syl 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
43 28 ressinbas 
 |-  ( T e. _V -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
44 12 43 syl 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
45 39 42 44 3eqtr4d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s T ) )
46 45 oveq1d 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
47 20 26 46 3eqtrd 
 |-  ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
48 simpr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> -. ( Base ` ( C |`s S ) ) C_ T )
49 ovexd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
50 8 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
51 13 17 ressval2 
 |-  ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
52 48 49 50 51 syl3anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
53 ovexd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) e. _V )
54 16 necomi 
 |-  ( Hom ` ndx ) =/= ( Base ` ndx )
55 54 a1i 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( Hom ` ndx ) =/= ( Base ` ndx ) )
56 4 4 xpexd 
 |-  ( ph -> ( S X. S ) e. _V )
57 2 56 fnexd 
 |-  ( ph -> H e. _V )
58 57 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> H e. _V )
59 fvex 
 |-  ( Base ` ( C |`s S ) ) e. _V
60 59 inex2 
 |-  ( T i^i ( Base ` ( C |`s S ) ) ) e. _V
61 60 a1i 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` ( C |`s S ) ) ) e. _V )
62 fvex 
 |-  ( Hom ` ndx ) e. _V
63 fvex 
 |-  ( Base ` ndx ) e. _V
64 62 63 setscom 
 |-  ( ( ( ( C |`s S ) e. _V /\ ( Hom ` ndx ) =/= ( Base ` ndx ) ) /\ ( H e. _V /\ ( T i^i ( Base ` ( C |`s S ) ) ) e. _V ) ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
65 53 55 58 61 64 syl22anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
66 eqid 
 |-  ( ( C |`s S ) |`s T ) = ( ( C |`s S ) |`s T )
67 eqid 
 |-  ( Base ` ( C |`s S ) ) = ( Base ` ( C |`s S ) )
68 66 67 ressval2 
 |-  ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( C |`s S ) e. _V /\ T e. _V ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
69 48 53 50 68 syl3anc 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
70 5 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
71 ressabs 
 |-  ( ( S e. W /\ T C_ S ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
72 4 70 71 syl2an2r 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
73 69 72 eqtr3d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( C |`s T ) )
74 73 oveq1d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
75 52 65 74 3eqtrd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
76 75 oveq1d 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
77 ovex 
 |-  ( C |`s T ) e. _V
78 23 adantr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
79 setsabs 
 |-  ( ( ( C |`s T ) e. _V /\ J e. _V ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
80 77 78 79 sylancr 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
81 76 80 eqtrd 
 |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
82 47 81 pm2.61dan 
 |-  ( ph -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
83 9 82 eqtrd 
 |-  ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
84 eqid 
 |-  ( C |`cat H ) = ( C |`cat H )
85 84 1 4 2 rescval2 
 |-  ( ph -> ( C |`cat H ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
86 85 oveq1d 
 |-  ( ph -> ( ( C |`cat H ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) )
87 eqid 
 |-  ( C |`cat J ) = ( C |`cat J )
88 87 1 8 3 rescval2 
 |-  ( ph -> ( C |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
89 83 86 88 3eqtr4d 
 |-  ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )