sscres

Description: Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	sscres	$⊢ (H Fn (S \times S) \land S \in V) \to ({H ↾}_{(T \times T)}) \subseteq_{cat} H$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ S \cap T \subseteq S$
2		simpl	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to x \in (S \cap T)$
3	2	elin2d	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to x \in T$
4		simpr	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to y \in (S \cap T)$
5	4	elin2d	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to y \in T$
6	3 5	ovresd	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to x ({H ↾}_{(T \times T)}) y = x H y$
7		eqimss	$⊢ x ({H ↾}_{(T \times T)}) y = x H y \to x ({H ↾}_{(T \times T)}) y \subseteq x H y$
8	6 7	syl	$⊢ (x \in (S \cap T) \land y \in (S \cap T)) \to x ({H ↾}_{(T \times T)}) y \subseteq x H y$
9	8	rgen2	$⊢ \forall x \in (S \cap T) \forall y \in (S \cap T) x ({H ↾}_{(T \times T)}) y \subseteq x H y$
10	1 9	pm3.2i	$⊢ (S \cap T \subseteq S \land \forall x \in (S \cap T) \forall y \in (S \cap T) x ({H ↾}_{(T \times T)}) y \subseteq x H y)$
11		simpl	$⊢ (H Fn (S \times S) \land S \in V) \to H Fn (S \times S)$
12		inss1	$⊢ (S \times S) \cap (T \times T) \subseteq S \times S$
13		fnssres	$⊢ (H Fn (S \times S) \land (S \times S) \cap (T \times T) \subseteq S \times S) \to ({H ↾}_{((S \times S) \cap (T \times T))}) Fn ((S \times S) \cap (T \times T))$
14	11 12 13	sylancl	$⊢ (H Fn (S \times S) \land S \in V) \to ({H ↾}_{((S \times S) \cap (T \times T))}) Fn ((S \times S) \cap (T \times T))$
15		resres	$⊢ {({H ↾}_{(S \times S)}) ↾}_{(T \times T)} = {H ↾}_{((S \times S) \cap (T \times T))}$
16		fnresdm	$⊢ H Fn (S \times S) \to {H ↾}_{(S \times S)} = H$
17	16	adantr	$⊢ (H Fn (S \times S) \land S \in V) \to {H ↾}_{(S \times S)} = H$
18	17	reseq1d	$⊢ (H Fn (S \times S) \land S \in V) \to {({H ↾}_{(S \times S)}) ↾}_{(T \times T)} = {H ↾}_{(T \times T)}$
19	15 18	eqtr3id	$⊢ (H Fn (S \times S) \land S \in V) \to {H ↾}_{((S \times S) \cap (T \times T))} = {H ↾}_{(T \times T)}$
20		inxp	$⊢ (S \times S) \cap (T \times T) = (S \cap T) \times (S \cap T)$
21	20	a1i	$⊢ (H Fn (S \times S) \land S \in V) \to (S \times S) \cap (T \times T) = (S \cap T) \times (S \cap T)$
22	19 21	fneq12d	$⊢ (H Fn (S \times S) \land S \in V) \to (({H ↾}_{((S \times S) \cap (T \times T))}) Fn ((S \times S) \cap (T \times T)) \leftrightarrow ({H ↾}_{(T \times T)}) Fn ((S \cap T) \times (S \cap T)))$
23	14 22	mpbid	$⊢ (H Fn (S \times S) \land S \in V) \to ({H ↾}_{(T \times T)}) Fn ((S \cap T) \times (S \cap T))$
24		simpr	$⊢ (H Fn (S \times S) \land S \in V) \to S \in V$
25	23 11 24	isssc	$⊢ (H Fn (S \times S) \land S \in V) \to (({H ↾}_{(T \times T)}) \subseteq_{cat} H \leftrightarrow (S \cap T \subseteq S \land \forall x \in (S \cap T) \forall y \in (S \cap T) x ({H ↾}_{(T \times T)}) y \subseteq x H y))$
26	10 25	mpbiri	$⊢ (H Fn (S \times S) \land S \in V) \to ({H ↾}_{(T \times T)}) \subseteq_{cat} H$

Metamath Proof Explorer

Theorem sscres

Proof