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

Proof

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

Metamath Proof Explorer

Theorem ressress

Proof