dfrefrels2

Description: Alternate definition of the class of reflexive relations. This is a 0-ary class constant, which is recommended for definitions (see the 1. Guideline at https://us.metamath.org/ileuni/mathbox.html ). Proper classes (like _I , see iprc ) are not elements of this (or any) class: if a class is an element of another class, it is not a proper class but a set, see elex . So if we use 0-ary constant classes as our main definitions, they are valid only for sets, not for proper classes. For proper classes we use predicate-type definitions like df-refrel . See also the comment of df-rels .

Note that while elementhood in the class of relations cancels restriction of r in dfrefrels2 , it keeps restriction of _I : this is why the very similar definitions df-refs , df-syms and df-trs diverge when we switch from (general) sets to relations in dfrefrels2 , dfsymrels2 and dftrrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

		Ref	Expression
	Assertion	dfrefrels2	$⊢ RefRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$

Proof

Step	Hyp	Ref	Expression
1		df-refrels	$⊢ RefRels = Refs \cap Rels$
2		df-refs	$⊢ Refs = \{r \| (I \cap (dom r \times ran r)) S (r \cap (dom r \times ran r))\}$
3		inex1g	$⊢ r \in V \to r \cap (dom r \times ran r) \in V$
4	3	elv	$⊢ r \cap (dom r \times ran r) \in V$
5		brssr	$⊢ r \cap (dom r \times ran r) \in V \to ((I \cap (dom r \times ran r)) S (r \cap (dom r \times ran r)) \leftrightarrow I \cap (dom r \times ran r) \subseteq r \cap (dom r \times ran r))$
6	4 5	ax-mp	$⊢ (I \cap (dom r \times ran r)) S (r \cap (dom r \times ran r)) \leftrightarrow I \cap (dom r \times ran r) \subseteq r \cap (dom r \times ran r)$
7		elrels6	$⊢ r \in V \to (r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r)$
8	7	elv	$⊢ r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r$
9	8	biimpi	$⊢ r \in Rels \to r \cap (dom r \times ran r) = r$
10	9	sseq2d	$⊢ r \in Rels \to (I \cap (dom r \times ran r) \subseteq r \cap (dom r \times ran r) \leftrightarrow I \cap (dom r \times ran r) \subseteq r)$
11	6 10	bitrid	$⊢ r \in Rels \to ((I \cap (dom r \times ran r)) S (r \cap (dom r \times ran r)) \leftrightarrow I \cap (dom r \times ran r) \subseteq r)$
12	1 2 11	abeqinbi	$⊢ RefRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$

Metamath Proof Explorer

Theorem dfrefrels2

Proof