refsymrels2

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, 20-Jul-2019)

		Ref	Expression
	Assertion	refsymrels2	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$

Proof

Step	Hyp	Ref	Expression
1		dfrefrels2	$⊢ RefRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$
2		dfsymrels2	$⊢ SymRels = \{r \in Rels \| r^{-1} \subseteq r\}$
3	1 2	ineq12i	$⊢ RefRels \cap SymRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\} \cap \{r \in Rels \| r^{-1} \subseteq r\}$
4		inrab	$⊢ \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\} \cap \{r \in Rels \| r^{-1} \subseteq r\} = \{r \in Rels \| (I \cap (dom r \times ran r) \subseteq r \land r^{-1} \subseteq r)\}$
5		symrefref2	$⊢ r^{-1} \subseteq r \to (I \cap (dom r \times ran r) \subseteq r \leftrightarrow {I ↾}_{dom r} \subseteq r)$
6	5	pm5.32ri	$⊢ (I \cap (dom r \times ran r) \subseteq r \land r^{-1} \subseteq r) \leftrightarrow ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)$
7	6	rabbii	$⊢ \{r \in Rels \| (I \cap (dom r \times ran r) \subseteq r \land r^{-1} \subseteq r)\} = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
8	3 4 7	3eqtri	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$

Metamath Proof Explorer

Theorem refsymrels2

Proof