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		df-ss	|- ( B C_ A <-> ( B i^i A ) = B )
8	7	biimpi	|- ( B C_ A -> ( B i^i A ) = B )
9	6 8	syl5eq	|- ( 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 ) ) )