Metamath Proof Explorer

Theorem ressress

Description: Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014) (Proof shortened by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion ressress 
|- ( ( A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> -. ( Base ` W ) C_ A )
2 simpr1 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> W e. _V )
3 simpr2 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> A e. X )
4 eqid 
 |-  ( W |`s A ) = ( W |`s A )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 4 5 ressval2 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. X ) -> ( W |`s A ) = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
7 1 2 3 6 syl3anc 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s A ) = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
8 inass 
 |-  ( ( A i^i B ) i^i ( Base ` W ) ) = ( A i^i ( B i^i ( Base ` W ) ) )
9 in12 
 |-  ( A i^i ( B i^i ( Base ` W ) ) ) = ( B i^i ( A i^i ( Base ` W ) ) )
10 8 9 eqtri 
 |-  ( ( A i^i B ) i^i ( Base ` W ) ) = ( B i^i ( A i^i ( Base ` W ) ) )
11 4 5 ressbas 
 |-  ( A e. X -> ( A i^i ( Base ` W ) ) = ( Base ` ( W |`s A ) ) )
12 3 11 syl 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i ( Base ` W ) ) = ( Base ` ( W |`s A ) ) )
13 12 ineq2d 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( B i^i ( A i^i ( Base ` W ) ) ) = ( B i^i ( Base ` ( W |`s A ) ) ) )
14 10 13 eqtr2id 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( B i^i ( Base ` ( W |`s A ) ) ) = ( ( A i^i B ) i^i ( Base ` W ) ) )
15 14 opeq2d 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> <. ( Base ` ndx ) , ( B i^i ( Base ` ( W |`s A ) ) ) >. = <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. )
16 7 15 oveq12d 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( W |`s A ) ) ) >. ) = ( ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
17 fvex 
 |-  ( Base ` W ) e. _V
18 17 inex2 
 |-  ( ( A i^i B ) i^i ( Base ` W ) ) e. _V
19 setsabs 
 |-  ( ( W e. _V /\ ( ( A i^i B ) i^i ( Base ` W ) ) e. _V ) -> ( ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
20 2 18 19 sylancl 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
21 16 20 eqtrd 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( W |`s A ) ) ) >. ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
22 simpll 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> -. ( Base ` ( W |`s A ) ) C_ B )
23 ovexd 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s A ) e. _V )
24 simpr3 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> B e. Y )
25 eqid 
 |-  ( ( W |`s A ) |`s B ) = ( ( W |`s A ) |`s B )
26 eqid 
 |-  ( Base ` ( W |`s A ) ) = ( Base ` ( W |`s A ) )
27 25 26 ressval2 
 |-  ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ ( W |`s A ) e. _V /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( ( W |`s A ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( W |`s A ) ) ) >. ) )
28 22 23 24 27 syl3anc 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( ( W |`s A ) sSet <. ( Base ` ndx ) , ( B i^i ( Base ` ( W |`s A ) ) ) >. ) )
29 inss1 
 |-  ( A i^i B ) C_ A
30 sstr 
 |-  ( ( ( Base ` W ) C_ ( A i^i B ) /\ ( A i^i B ) C_ A ) -> ( Base ` W ) C_ A )
31 29 30 mpan2 
 |-  ( ( Base ` W ) C_ ( A i^i B ) -> ( Base ` W ) C_ A )
32 1 31 nsyl 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> -. ( Base ` W ) C_ ( A i^i B ) )
33 inex1g 
 |-  ( A e. X -> ( A i^i B ) e. _V )
34 3 33 syl 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i B ) e. _V )
35 eqid 
 |-  ( W |`s ( A i^i B ) ) = ( W |`s ( A i^i B ) )
36 35 5 ressval2 
 |-  ( ( -. ( Base ` W ) C_ ( A i^i B ) /\ W e. _V /\ ( A i^i B ) e. _V ) -> ( W |`s ( A i^i B ) ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
37 32 2 34 36 syl3anc 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s ( A i^i B ) ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i ( Base ` W ) ) >. ) )
38 21 28 37 3eqtr4d 
 |-  ( ( ( -. ( Base ` ( W |`s A ) ) C_ B /\ -. ( Base ` W ) C_ A ) /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
39 38 exp31 
 |-  ( -. ( Base ` ( W |`s A ) ) C_ B -> ( -. ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) ) ) )
40 ovex 
 |-  ( W |`s A ) e. _V
41 25 26 ressid2 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W |`s A ) e. _V /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s A ) )
42 40 41 mp3an2 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s A ) )
43 42 3ad2antr3 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( W |`s A ) )
44 in32 
 |-  ( ( A i^i B ) i^i ( Base ` W ) ) = ( ( A i^i ( Base ` W ) ) i^i B )
45 simpr2 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> A e. X )
46 45 11 syl 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i ( Base ` W ) ) = ( Base ` ( W |`s A ) ) )
47 simpl 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( Base ` ( W |`s A ) ) C_ B )
48 46 47 eqsstrd 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i ( Base ` W ) ) C_ B )
49 df-ss 
 |-  ( ( A i^i ( Base ` W ) ) C_ B <-> ( ( A i^i ( Base ` W ) ) i^i B ) = ( A i^i ( Base ` W ) ) )
50 48 49 sylib 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( A i^i ( Base ` W ) ) i^i B ) = ( A i^i ( Base ` W ) ) )
51 44 50 eqtr2id 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i ( Base ` W ) ) = ( ( A i^i B ) i^i ( Base ` W ) ) )
52 51 oveq2d 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s ( A i^i ( Base ` W ) ) ) = ( W |`s ( ( A i^i B ) i^i ( Base ` W ) ) ) )
53 5 ressinbas 
 |-  ( A e. X -> ( W |`s A ) = ( W |`s ( A i^i ( Base ` W ) ) ) )
54 45 53 syl 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s A ) = ( W |`s ( A i^i ( Base ` W ) ) ) )
55 5 ressinbas 
 |-  ( ( A i^i B ) e. _V -> ( W |`s ( A i^i B ) ) = ( W |`s ( ( A i^i B ) i^i ( Base ` W ) ) ) )
56 45 33 55 3syl 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s ( A i^i B ) ) = ( W |`s ( ( A i^i B ) i^i ( Base ` W ) ) ) )
57 52 54 56 3eqtr4d 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
58 43 57 eqtrd 
 |-  ( ( ( Base ` ( W |`s A ) ) C_ B /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
59 58 ex 
 |-  ( ( Base ` ( W |`s A ) ) C_ B -> ( ( W e. _V /\ A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) ) )
60 4 5 ressid2 
 |-  ( ( ( Base ` W ) C_ A /\ W e. _V /\ A e. X ) -> ( W |`s A ) = W )
61 60 3adant3r3 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s A ) = W )
62 61 oveq1d 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( W |`s B ) )
63 inss2 
 |-  ( B i^i ( Base ` W ) ) C_ ( Base ` W )
64 simpl 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( Base ` W ) C_ A )
65 63 64 sstrid 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( B i^i ( Base ` W ) ) C_ A )
66 sseqin2 
 |-  ( ( B i^i ( Base ` W ) ) C_ A <-> ( A i^i ( B i^i ( Base ` W ) ) ) = ( B i^i ( Base ` W ) ) )
67 65 66 sylib 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( A i^i ( B i^i ( Base ` W ) ) ) = ( B i^i ( Base ` W ) ) )
68 8 67 eqtr2id 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( B i^i ( Base ` W ) ) = ( ( A i^i B ) i^i ( Base ` W ) ) )
69 68 oveq2d 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s ( B i^i ( Base ` W ) ) ) = ( W |`s ( ( A i^i B ) i^i ( Base ` W ) ) ) )
70 simpr3 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> B e. Y )
71 5 ressinbas 
 |-  ( B e. Y -> ( W |`s B ) = ( W |`s ( B i^i ( Base ` W ) ) ) )
72 70 71 syl 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s B ) = ( W |`s ( B i^i ( Base ` W ) ) ) )
73 simpr2 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> A e. X )
74 73 33 55 3syl 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s ( A i^i B ) ) = ( W |`s ( ( A i^i B ) i^i ( Base ` W ) ) ) )
75 69 72 74 3eqtr4d 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( W |`s B ) = ( W |`s ( A i^i B ) ) )
76 62 75 eqtrd 
 |-  ( ( ( Base ` W ) C_ A /\ ( W e. _V /\ A e. X /\ B e. Y ) ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
77 76 ex 
 |-  ( ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) ) )
78 39 59 77 pm2.61ii 
 |-  ( ( W e. _V /\ A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
79 78 3expib 
 |-  ( W e. _V -> ( ( A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) ) )
80 ress0 
 |-  ( (/) |`s B ) = (/)
81 reldmress 
 |-  Rel dom |`s
82 81 ovprc1 
 |-  ( -. W e. _V -> ( W |`s A ) = (/) )
83 82 oveq1d 
 |-  ( -. W e. _V -> ( ( W |`s A ) |`s B ) = ( (/) |`s B ) )
84 81 ovprc1 
 |-  ( -. W e. _V -> ( W |`s ( A i^i B ) ) = (/) )
85 80 83 84 3eqtr4a 
 |-  ( -. W e. _V -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
86 85 a1d 
 |-  ( -. W e. _V -> ( ( A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) ) )
87 79 86 pm2.61i 
 |-  ( ( A e. X /\ B e. Y ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )