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 \in X \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		ressid.1	$⊢ B = {Base}_{W}$
2		elex	$⊢ A \in X \to A \in V$
3		eqid	$⊢ W ↾_{𝑠} A = W ↾_{𝑠} A$
4	3 1	ressid2	$⊢ (B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} A = W$
5		ssid	$⊢ B \subseteq B$
6		incom	$⊢ A \cap B = B \cap A$
7		df-ss	$⊢ B \subseteq A \leftrightarrow B \cap A = B$
8	7	biimpi	$⊢ B \subseteq A \to B \cap A = B$
9	6 8	syl5eq	$⊢ B \subseteq A \to A \cap B = B$
10	5 9	sseqtrrid	$⊢ B \subseteq A \to B \subseteq A \cap B$
11		elex	$⊢ W \in V \to W \in V$
12		inex1g	$⊢ A \in V \to A \cap B \in V$
13		eqid	$⊢ W ↾_{𝑠} (A \cap B) = W ↾_{𝑠} (A \cap B)$
14	13 1	ressid2	$⊢ (B \subseteq A \cap B \land W \in V \land A \cap B \in V) \to W ↾_{𝑠} (A \cap B) = W$
15	10 11 12 14	syl3an	$⊢ (B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} (A \cap B) = W$
16	4 15	eqtr4d	$⊢ (B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
17	16	3expb	$⊢ (B \subseteq A \land (W \in V \land A \in V)) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
18		inass	$⊢ (A \cap B) \cap B = A \cap (B \cap B)$
19		inidm	$⊢ B \cap B = B$
20	19	ineq2i	$⊢ A \cap (B \cap B) = A \cap B$
21	18 20	eqtr2i	$⊢ A \cap B = (A \cap B) \cap B$
22	21	opeq2i	$⊢ ⟨{Base}_{ndx}, A \cap B⟩ = ⟨{Base}_{ndx}, (A \cap B) \cap B⟩$
23	22	oveq2i	$⊢ W sSet ⟨{Base}_{ndx}, A \cap B⟩ = W sSet ⟨{Base}_{ndx}, (A \cap B) \cap B⟩$
24	3 1	ressval2	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} A = W sSet ⟨{Base}_{ndx}, A \cap B⟩$
25		inss1	$⊢ A \cap B \subseteq A$
26		sstr	$⊢ (B \subseteq A \cap B \land A \cap B \subseteq A) \to B \subseteq A$
27	25 26	mpan2	$⊢ B \subseteq A \cap B \to B \subseteq A$
28	27	con3i	$⊢ \neg B \subseteq A \to \neg B \subseteq A \cap B$
29	13 1	ressval2	$⊢ (\neg B \subseteq A \cap B \land W \in V \land A \cap B \in V) \to W ↾_{𝑠} (A \cap B) = W sSet ⟨{Base}_{ndx}, (A \cap B) \cap B⟩$
30	28 11 12 29	syl3an	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} (A \cap B) = W sSet ⟨{Base}_{ndx}, (A \cap B) \cap B⟩$
31	23 24 30	3eqtr4a	$⊢ (\neg B \subseteq A \land W \in V \land A \in V) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
32	31	3expb	$⊢ (\neg B \subseteq A \land (W \in V \land A \in V)) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
33	17 32	pm2.61ian	$⊢ (W \in V \land A \in V) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
34		reldmress	$⊢ Rel dom ↾_{𝑠}$
35	34	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑠} A = \emptyset$
36	34	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑠} (A \cap B) = \emptyset$
37	35 36	eqtr4d	$⊢ \neg W \in V \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
38	37	adantr	$⊢ (\neg W \in V \land A \in V) \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
39	33 38	pm2.61ian	$⊢ A \in V \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$
40	2 39	syl	$⊢ A \in X \to W ↾_{𝑠} A = W ↾_{𝑠} (A \cap B)$

Metamath Proof Explorer

Theorem ressinbas

Proof