This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvref4

Description: Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023)

		Ref	Expression
	Assertion	cnvref4	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq S \cap (dom R \times ran R) \leftrightarrow R \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		dfrel6	$⊢ Rel R \leftrightarrow R \cap (dom R \times ran R) = R$
2	1	biimpi	$⊢ Rel R \to R \cap (dom R \times ran R) = R$
3	2	dmeqd	$⊢ Rel R \to dom (R \cap (dom R \times ran R)) = dom R$
4	2	rneqd	$⊢ Rel R \to ran (R \cap (dom R \times ran R)) = ran R$
5	3 4	xpeq12d	$⊢ Rel R \to dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R)) = dom R \times ran R$
6	5	ineq2d	$⊢ Rel R \to S \cap (dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R))) = S \cap (dom R \times ran R)$
7	6	sseq2d	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq S \cap (dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R))) \leftrightarrow R \cap (dom R \times ran R) \subseteq S \cap (dom R \times ran R))$
8		relxp	$⊢ Rel (dom R \times ran R)$
9		relin2	$⊢ Rel (dom R \times ran R) \to Rel (R \cap (dom R \times ran R))$
10		relssinxpdmrn	$⊢ Rel (R \cap (dom R \times ran R)) \to (R \cap (dom R \times ran R) \subseteq S \cap (dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R))) \leftrightarrow R \cap (dom R \times ran R) \subseteq S)$
11	8 9 10	mp2b	$⊢ R \cap (dom R \times ran R) \subseteq S \cap (dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R))) \leftrightarrow R \cap (dom R \times ran R) \subseteq S$
12	2	sseq1d	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq S \leftrightarrow R \subseteq S)$
13	11 12	bitrid	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq S \cap (dom (R \cap (dom R \times ran R)) \times ran (R \cap (dom R \times ran R))) \leftrightarrow R \subseteq S)$
14	7 13	bitr3d	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq S \cap (dom R \times ran R) \leftrightarrow R \subseteq S)$