rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	rescabs.c	$⊢ φ \to C \in V$
	rescabs.h	$⊢ φ \to H Fn (S \times S)$
	rescabs.j	$⊢ φ \to J Fn (T \times T)$
	rescabs.s	$⊢ φ \to S \in W$
	rescabs.t	$⊢ φ \to T \subseteq S$
Assertion	rescabs	$⊢ φ \to (C ↾_{cat} H) ↾_{cat} J = C ↾_{cat} J$

Proof

Step	Hyp	Ref	Expression
1		rescabs.c	$⊢ φ \to C \in V$
2		rescabs.h	$⊢ φ \to H Fn (S \times S)$
3		rescabs.j	$⊢ φ \to J Fn (T \times T)$
4		rescabs.s	$⊢ φ \to S \in W$
5		rescabs.t	$⊢ φ \to T \subseteq S$
6		eqid	$⊢ ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J$
7		ovexd	$⊢ φ \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V$
8	4 5	ssexd	$⊢ φ \to T \in V$
9	6 7 8 3	rescval2	$⊢ φ \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J = (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
10		simpr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to {Base}_{(C ↾_{𝑠} S)} \subseteq T$
11		ovexd	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V$
12	8	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \in V$
13		eqid	$⊢ ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T$
14		baseid	$⊢ Base = Slot {Base}_{ndx}$
15		1re	$⊢ 1 \in ℝ$
16		1nn	$⊢ 1 \in ℕ$
17		4nn0	$⊢ 4 \in ℕ_{0}$
18		1nn0	$⊢ 1 \in ℕ_{0}$
19		1lt10	$⊢ 1 < 10$
20	16 17 18 19	declti	$⊢ 1 < 14$
21	15 20	ltneii	$⊢ 1 \neq 14$
22		basendx	$⊢ {Base}_{ndx} = 1$
23		homndx	$⊢ Hom (ndx) = 14$
24	22 23	neeq12i	$⊢ {Base}_{ndx} \neq Hom (ndx) \leftrightarrow 1 \neq 14$
25	21 24	mpbir	$⊢ {Base}_{ndx} \neq Hom (ndx)$
26	14 25	setsnid	$⊢ {Base}_{(C ↾_{𝑠} S)} = {Base}_{((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩)}$
27	13 26	ressid2	$⊢ ({Base}_{(C ↾_{𝑠} S)} \subseteq T \land (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V \land T \in V) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩$
28	10 11 12 27	syl3anc	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩$
29	28	oveq1d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩$
30		ovex	$⊢ C ↾_{𝑠} S \in V$
31	8 8	xpexd	$⊢ φ \to T \times T \in V$
32		fnex	$⊢ (J Fn (T \times T) \land T \times T \in V) \to J \in V$
33	3 31 32	syl2anc	$⊢ φ \to J \in V$
34	33	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to J \in V$
35		setsabs	$⊢ (C ↾_{𝑠} S \in V \land J \in V) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), J⟩$
36	30 34 35	sylancr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), J⟩$
37		eqid	$⊢ C ↾_{𝑠} S = C ↾_{𝑠} S$
38		eqid	$⊢ {Base}_{C} = {Base}_{C}$
39	37 38	ressbas	$⊢ S \in W \to S \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} S)}$
40	4 39	syl	$⊢ φ \to S \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} S)}$
41	40	sseq1d	$⊢ φ \to (S \cap {Base}_{C} \subseteq T \leftrightarrow {Base}_{(C ↾_{𝑠} S)} \subseteq T)$
42	41	biimpar	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq T$
43		inss2	$⊢ S \cap {Base}_{C} \subseteq {Base}_{C}$
44	43	a1i	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq {Base}_{C}$
45	42 44	ssind	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq T \cap {Base}_{C}$
46	5	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \subseteq S$
47	46	ssrind	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \cap {Base}_{C} \subseteq S \cap {Base}_{C}$
48	45 47	eqssd	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} = T \cap {Base}_{C}$
49	48	oveq2d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} (S \cap {Base}_{C}) = C ↾_{𝑠} (T \cap {Base}_{C})$
50	4	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \in W$
51	38	ressinbas	$⊢ S \in W \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
52	50 51	syl	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
53	38	ressinbas	$⊢ T \in V \to C ↾_{𝑠} T = C ↾_{𝑠} (T \cap {Base}_{C})$
54	12 53	syl	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} T = C ↾_{𝑠} (T \cap {Base}_{C})$
55	49 52 54	3eqtr4d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S = C ↾_{𝑠} T$
56	55	oveq1d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
57	29 36 56	3eqtrd	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
58		simpr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T$
59		ovexd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V$
60	8	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \in V$
61	13 26	ressval2	$⊢ (\neg {Base}_{(C ↾_{𝑠} S)} \subseteq T \land (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V \land T \in V) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩$
62	58 59 60 61	syl3anc	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩$
63		ovexd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S \in V$
64	25	necomi	$⊢ Hom (ndx) \neq {Base}_{ndx}$
65	64	a1i	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to Hom (ndx) \neq {Base}_{ndx}$
66	4 4	xpexd	$⊢ φ \to S \times S \in V$
67		fnex	$⊢ (H Fn (S \times S) \land S \times S \in V) \to H \in V$
68	2 66 67	syl2anc	$⊢ φ \to H \in V$
69	68	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to H \in V$
70		fvex	$⊢ {Base}_{(C ↾_{𝑠} S)} \in V$
71	70	inex2	$⊢ T \cap {Base}_{(C ↾_{𝑠} S)} \in V$
72	71	a1i	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \cap {Base}_{(C ↾_{𝑠} S)} \in V$
73		fvex	$⊢ Hom (ndx) \in V$
74		fvex	$⊢ {Base}_{ndx} \in V$
75	73 74	setscom	$⊢ ((C ↾_{𝑠} S \in V \land Hom (ndx) \neq {Base}_{ndx}) \land (H \in V \land T \cap {Base}_{(C ↾_{𝑠} S)} \in V)) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩ = ((C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩) sSet ⟨Hom (ndx), H⟩$
76	63 65 69 72 75	syl22anc	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩ = ((C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩) sSet ⟨Hom (ndx), H⟩$
77		eqid	$⊢ (C ↾_{𝑠} S) ↾_{𝑠} T = (C ↾_{𝑠} S) ↾_{𝑠} T$
78		eqid	$⊢ {Base}_{(C ↾_{𝑠} S)} = {Base}_{(C ↾_{𝑠} S)}$
79	77 78	ressval2	$⊢ (\neg {Base}_{(C ↾_{𝑠} S)} \subseteq T \land C ↾_{𝑠} S \in V \land T \in V) \to (C ↾_{𝑠} S) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩$
80	58 63 60 79	syl3anc	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩$
81	4	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \in W$
82	5	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \subseteq S$
83		ressabs	$⊢ (S \in W \land T \subseteq S) \to (C ↾_{𝑠} S) ↾_{𝑠} T = C ↾_{𝑠} T$
84	81 82 83	syl2anc	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) ↾_{𝑠} T = C ↾_{𝑠} T$
85	80 84	eqtr3d	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩ = C ↾_{𝑠} T$
86	85	oveq1d	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩) sSet ⟨Hom (ndx), H⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩$
87	62 76 86	3eqtrd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩$
88	87	oveq1d	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = ((C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩$
89		ovex	$⊢ C ↾_{𝑠} T \in V$
90	33	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to J \in V$
91		setsabs	$⊢ (C ↾_{𝑠} T \in V \land J \in V) \to ((C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
92	89 90 91	sylancr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
93	88 92	eqtrd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
94	57 93	pm2.61dan	$⊢ φ \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
95	9 94	eqtrd	$⊢ φ \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
96		eqid	$⊢ C ↾_{cat} H = C ↾_{cat} H$
97	96 1 4 2	rescval2	$⊢ φ \to C ↾_{cat} H = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩$
98	97	oveq1d	$⊢ φ \to (C ↾_{cat} H) ↾_{cat} J = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J$
99		eqid	$⊢ C ↾_{cat} J = C ↾_{cat} J$
100	99 1 8 3	rescval2	$⊢ φ \to C ↾_{cat} J = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
101	95 98 100	3eqtr4d	$⊢ φ \to (C ↾_{cat} H) ↾_{cat} J = C ↾_{cat} J$

Metamath Proof Explorer

Theorem rescabs

Proof