elrefsymrels2

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 ) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrels2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 22-Jul-2019)

		Ref	Expression
	Assertion	elrefsymrels2	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \in Rels)$

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
2		dmeq	$⊢ r = R \to dom r = dom R$
3	2	reseq2d	$⊢ r = R \to {I ↾}_{dom r} = {I ↾}_{dom R}$
4		id	$⊢ r = R \to r = R$
5	3 4	sseq12d	$⊢ r = R \to ({I ↾}_{dom r} \subseteq r \leftrightarrow {I ↾}_{dom R} \subseteq R)$
6		cnveq	$⊢ r = R \to r^{-1} = R^{-1}$
7	6 4	sseq12d	$⊢ r = R \to (r^{-1} \subseteq r \leftrightarrow R^{-1} \subseteq R)$
8	5 7	anbi12d	$⊢ r = R \to (({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r) \leftrightarrow ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R))$
9	1 8	rabeqel	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \in Rels)$

Metamath Proof Explorer

Theorem elrefsymrels2

Proof