resssxp

Description: If the R -image of a class A is a subclass of B , then the restriction of R to A is a subset of the Cartesian product of A and B . (Contributed by RP, 24-Dec-2019)

		Ref	Expression
	Assertion	resssxp	$⊢ R [A] \subseteq B \leftrightarrow {R ↾}_{A} \subseteq A \times B$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ R [A] = ran ({R ↾}_{A})$
2	1	sseq1i	$⊢ R [A] \subseteq B \leftrightarrow ran ({R ↾}_{A}) \subseteq B$
3		dmres	$⊢ dom ({R ↾}_{A}) = A \cap dom R$
4		inss1	$⊢ A \cap dom R \subseteq A$
5	3 4	eqsstri	$⊢ dom ({R ↾}_{A}) \subseteq A$
6	5	biantrur	$⊢ ran ({R ↾}_{A}) \subseteq B \leftrightarrow (dom ({R ↾}_{A}) \subseteq A \land ran ({R ↾}_{A}) \subseteq B)$
7		relres	$⊢ Rel ({R ↾}_{A})$
8		relssdmrn	$⊢ Rel ({R ↾}_{A}) \to {R ↾}_{A} \subseteq dom ({R ↾}_{A}) \times ran ({R ↾}_{A})$
9	7 8	ax-mp	$⊢ {R ↾}_{A} \subseteq dom ({R ↾}_{A}) \times ran ({R ↾}_{A})$
10		xpss12	$⊢ (dom ({R ↾}_{A}) \subseteq A \land ran ({R ↾}_{A}) \subseteq B) \to dom ({R ↾}_{A}) \times ran ({R ↾}_{A}) \subseteq A \times B$
11	9 10	sstrid	$⊢ (dom ({R ↾}_{A}) \subseteq A \land ran ({R ↾}_{A}) \subseteq B) \to {R ↾}_{A} \subseteq A \times B$
12		dmss	$⊢ {R ↾}_{A} \subseteq A \times B \to dom ({R ↾}_{A}) \subseteq dom (A \times B)$
13		dmxpss	$⊢ dom (A \times B) \subseteq A$
14	12 13	sstrdi	$⊢ {R ↾}_{A} \subseteq A \times B \to dom ({R ↾}_{A}) \subseteq A$
15		rnss	$⊢ {R ↾}_{A} \subseteq A \times B \to ran ({R ↾}_{A}) \subseteq ran (A \times B)$
16		rnxpss	$⊢ ran (A \times B) \subseteq B$
17	15 16	sstrdi	$⊢ {R ↾}_{A} \subseteq A \times B \to ran ({R ↾}_{A}) \subseteq B$
18	14 17	jca	$⊢ {R ↾}_{A} \subseteq A \times B \to (dom ({R ↾}_{A}) \subseteq A \land ran ({R ↾}_{A}) \subseteq B)$
19	11 18	impbii	$⊢ (dom ({R ↾}_{A}) \subseteq A \land ran ({R ↾}_{A}) \subseteq B) \leftrightarrow {R ↾}_{A} \subseteq A \times B$
20	2 6 19	3bitri	$⊢ R [A] \subseteq B \leftrightarrow {R ↾}_{A} \subseteq A \times B$

Metamath Proof Explorer

Theorem resssxp

Proof