rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 9-Nov-2024)

	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		slotsbhcdif	$⊢ ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx) \land Hom (ndx) \neq comp (ndx))$
16	15	simp1i	$⊢ {Base}_{ndx} \neq Hom (ndx)$
17	14 16	setsnid	$⊢ {Base}_{(C ↾_{𝑠} S)} = {Base}_{((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩)}$
18	13 17	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⟩$
19	10 11 12 18	syl3anc	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩$
20	19	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⟩$
21		ovex	$⊢ C ↾_{𝑠} S \in V$
22	8 8	xpexd	$⊢ φ \to T \times T \in V$
23	3 22	fnexd	$⊢ φ \to J \in V$
24	23	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to J \in V$
25		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⟩$
26	21 24 25	sylancr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), J⟩$
27		eqid	$⊢ C ↾_{𝑠} S = C ↾_{𝑠} S$
28		eqid	$⊢ {Base}_{C} = {Base}_{C}$
29	27 28	ressbas	$⊢ S \in W \to S \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} S)}$
30	4 29	syl	$⊢ φ \to S \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} S)}$
31	30	sseq1d	$⊢ φ \to (S \cap {Base}_{C} \subseteq T \leftrightarrow {Base}_{(C ↾_{𝑠} S)} \subseteq T)$
32	31	biimpar	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq T$
33		inss2	$⊢ S \cap {Base}_{C} \subseteq {Base}_{C}$
34	33	a1i	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq {Base}_{C}$
35	32 34	ssind	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} \subseteq T \cap {Base}_{C}$
36	5	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \subseteq S$
37	36	ssrind	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \cap {Base}_{C} \subseteq S \cap {Base}_{C}$
38	35 37	eqssd	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \cap {Base}_{C} = T \cap {Base}_{C}$
39	38	oveq2d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} (S \cap {Base}_{C}) = C ↾_{𝑠} (T \cap {Base}_{C})$
40	4	adantr	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to S \in W$
41	28	ressinbas	$⊢ S \in W \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
42	40 41	syl	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
43	28	ressinbas	$⊢ T \in V \to C ↾_{𝑠} T = C ↾_{𝑠} (T \cap {Base}_{C})$
44	12 43	syl	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} T = C ↾_{𝑠} (T \cap {Base}_{C})$
45	39 42 44	3eqtr4d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S = C ↾_{𝑠} T$
46	45	oveq1d	$⊢ (φ \land {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
47	20 26 46	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⟩$
48		simpr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T$
49		ovexd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩ \in V$
50	8	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \in V$
51	13 17	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)}⟩$
52	48 49 50 51	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)}⟩$
53		ovexd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to C ↾_{𝑠} S \in V$
54	16	necomi	$⊢ Hom (ndx) \neq {Base}_{ndx}$
55	54	a1i	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to Hom (ndx) \neq {Base}_{ndx}$
56	4 4	xpexd	$⊢ φ \to S \times S \in V$
57	2 56	fnexd	$⊢ φ \to H \in V$
58	57	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to H \in V$
59		fvex	$⊢ {Base}_{(C ↾_{𝑠} S)} \in V$
60	59	inex2	$⊢ T \cap {Base}_{(C ↾_{𝑠} S)} \in V$
61	60	a1i	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \cap {Base}_{(C ↾_{𝑠} S)} \in V$
62		fvex	$⊢ Hom (ndx) \in V$
63		fvex	$⊢ {Base}_{ndx} \in V$
64	62 63	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⟩$
65	53 55 58 61 64	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⟩$
66		eqid	$⊢ (C ↾_{𝑠} S) ↾_{𝑠} T = (C ↾_{𝑠} S) ↾_{𝑠} T$
67		eqid	$⊢ {Base}_{(C ↾_{𝑠} S)} = {Base}_{(C ↾_{𝑠} S)}$
68	66 67	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)}⟩$
69	48 53 50 68	syl3anc	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) ↾_{𝑠} T = (C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩$
70	5	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to T \subseteq S$
71		ressabs	$⊢ (S \in W \land T \subseteq S) \to (C ↾_{𝑠} S) ↾_{𝑠} T = C ↾_{𝑠} T$
72	4 70 71	syl2an2r	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) ↾_{𝑠} T = C ↾_{𝑠} T$
73	69 72	eqtr3d	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to (C ↾_{𝑠} S) sSet ⟨{Base}_{ndx}, T \cap {Base}_{(C ↾_{𝑠} S)}⟩ = C ↾_{𝑠} T$
74	73	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⟩$
75	52 65 74	3eqtrd	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), H⟩$
76	75	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⟩$
77		ovex	$⊢ C ↾_{𝑠} T \in V$
78	23	adantr	$⊢ (φ \land \neg {Base}_{(C ↾_{𝑠} S)} \subseteq T) \to J \in V$
79		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⟩$
80	77 78 79	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⟩$
81	76 80	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⟩$
82	47 81	pm2.61dan	$⊢ φ \to (((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩ = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
83	9 82	eqtrd	$⊢ φ \to ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
84		eqid	$⊢ C ↾_{cat} H = C ↾_{cat} H$
85	84 1 4 2	rescval2	$⊢ φ \to C ↾_{cat} H = (C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩$
86	85	oveq1d	$⊢ φ \to (C ↾_{cat} H) ↾_{cat} J = ((C ↾_{𝑠} S) sSet ⟨Hom (ndx), H⟩) ↾_{cat} J$
87		eqid	$⊢ C ↾_{cat} J = C ↾_{cat} J$
88	87 1 8 3	rescval2	$⊢ φ \to C ↾_{cat} J = (C ↾_{𝑠} T) sSet ⟨Hom (ndx), J⟩$
89	83 86 88	3eqtr4d	$⊢ φ \to (C ↾_{cat} H) ↾_{cat} J = C ↾_{cat} J$

Metamath Proof Explorer

Theorem rescabs

Proof