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

Metamath Proof Explorer

Theorem ressinbas

Description: Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 
|- B = ( Base ` W )
Assertion ressinbas 
|- ( A e. X -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 ressid.1 
 |-  B = ( Base ` W )
2 elex 
 |-  ( A e. X -> A e. _V )
3 eqid 
 |-  ( W |`s A ) = ( W |`s A )
4 3 1 ressid2 
 |-  ( ( B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s A ) = W )
5 ssid 
 |-  B C_ B
6 incom 
 |-  ( A i^i B ) = ( B i^i A )
7 dfss2 
 |-  ( B C_ A <-> ( B i^i A ) = B )
8 7 biimpi 
 |-  ( B C_ A -> ( B i^i A ) = B )
9 6 8 eqtrid 
 |-  ( B C_ A -> ( A i^i B ) = B )
10 5 9 sseqtrrid 
 |-  ( B C_ A -> B C_ ( A i^i B ) )
11 elex 
 |-  ( W e. _V -> W e. _V )
12 inex1g 
 |-  ( A e. _V -> ( A i^i B ) e. _V )
13 eqid 
 |-  ( W |`s ( A i^i B ) ) = ( W |`s ( A i^i B ) )
14 13 1 ressid2 
 |-  ( ( B C_ ( A i^i B ) /\ W e. _V /\ ( A i^i B ) e. _V ) -> ( W |`s ( A i^i B ) ) = W )
15 10 11 12 14 syl3an 
 |-  ( ( B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s ( A i^i B ) ) = W )
16 4 15 eqtr4d 
 |-  ( ( B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
17 16 3expb 
 |-  ( ( B C_ A /\ ( W e. _V /\ A e. _V ) ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
18 inass 
 |-  ( ( A i^i B ) i^i B ) = ( A i^i ( B i^i B ) )
19 inidm 
 |-  ( B i^i B ) = B
20 19 ineq2i 
 |-  ( A i^i ( B i^i B ) ) = ( A i^i B )
21 18 20 eqtr2i 
 |-  ( A i^i B ) = ( ( A i^i B ) i^i B )
22 21 opeq2i 
 |-  <. ( Base ` ndx ) , ( A i^i B ) >. = <. ( Base ` ndx ) , ( ( A i^i B ) i^i B ) >.
23 22 oveq2i 
 |-  ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i B ) >. )
24 3 1 ressval2 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s A ) = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
25 inss1 
 |-  ( A i^i B ) C_ A
26 sstr 
 |-  ( ( B C_ ( A i^i B ) /\ ( A i^i B ) C_ A ) -> B C_ A )
27 25 26 mpan2 
 |-  ( B C_ ( A i^i B ) -> B C_ A )
28 27 con3i 
 |-  ( -. B C_ A -> -. B C_ ( A i^i B ) )
29 13 1 ressval2 
 |-  ( ( -. B 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 B ) >. ) )
30 28 11 12 29 syl3an 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s ( A i^i B ) ) = ( W sSet <. ( Base ` ndx ) , ( ( A i^i B ) i^i B ) >. ) )
31 23 24 30 3eqtr4a 
 |-  ( ( -. B C_ A /\ W e. _V /\ A e. _V ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
32 31 3expb 
 |-  ( ( -. B C_ A /\ ( W e. _V /\ A e. _V ) ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
33 17 32 pm2.61ian 
 |-  ( ( W e. _V /\ A e. _V ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
34 reldmress 
 |-  Rel dom |`s
35 34 ovprc1 
 |-  ( -. W e. _V -> ( W |`s A ) = (/) )
36 34 ovprc1 
 |-  ( -. W e. _V -> ( W |`s ( A i^i B ) ) = (/) )
37 35 36 eqtr4d 
 |-  ( -. W e. _V -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
38 37 adantr 
 |-  ( ( -. W e. _V /\ A e. _V ) -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
39 33 38 pm2.61ian 
 |-  ( A e. _V -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )
40 2 39 syl 
 |-  ( A e. X -> ( W |`s A ) = ( W |`s ( A i^i B ) ) )