refrelsredund4

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 ) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022)

		Ref	Expression
	Assertion	refrelsredund4	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} Redund ⟨RefRels, (RefRels \cap SymRels)⟩$

Proof

Step	Hyp	Ref	Expression
1		inxpssres	$⊢ I \cap (dom r \times ran r) \subseteq {I ↾}_{dom r}$
2		sstr2	$⊢ I \cap (dom r \times ran r) \subseteq {I ↾}_{dom r} \to ({I ↾}_{dom r} \subseteq r \to I \cap (dom r \times ran r) \subseteq r)$
3	1 2	ax-mp	$⊢ {I ↾}_{dom r} \subseteq r \to I \cap (dom r \times ran r) \subseteq r$
4	3	ssrabi	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \subseteq \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$
5		dfrefrels2	$⊢ RefRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$
6	4 5	sseqtrri	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \subseteq RefRels$
7		in32	$⊢ (\{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap SymRels) \cap RefRels = (\{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap RefRels) \cap SymRels$
8		inrab	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap \{r \in Rels \| r^{-1} \subseteq r\} = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
9		dfsymrels2	$⊢ SymRels = \{r \in Rels \| r^{-1} \subseteq r\}$
10	9	ineq2i	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap SymRels = \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap \{r \in Rels \| r^{-1} \subseteq r\}$
11		refsymrels2	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
12	8 10 11	3eqtr4i	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap SymRels = RefRels \cap SymRels$
13	12	ineq1i	$⊢ (\{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap SymRels) \cap RefRels = (RefRels \cap SymRels) \cap RefRels$
14		inass	$⊢ (\{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap RefRels) \cap SymRels = \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap (RefRels \cap SymRels)$
15	7 13 14	3eqtr3ri	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap (RefRels \cap SymRels) = (RefRels \cap SymRels) \cap RefRels$
16		in32	$⊢ (RefRels \cap SymRels) \cap RefRels = (RefRels \cap RefRels) \cap SymRels$
17		inass	$⊢ (RefRels \cap RefRels) \cap SymRels = RefRels \cap (RefRels \cap SymRels)$
18	15 16 17	3eqtri	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap (RefRels \cap SymRels) = RefRels \cap (RefRels \cap SymRels)$
19		df-redund	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} Redund ⟨RefRels, (RefRels \cap SymRels)⟩ \leftrightarrow (\{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \subseteq RefRels \land \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} \cap (RefRels \cap SymRels) = RefRels \cap (RefRels \cap SymRels))$
20	6 18 19	mpbir2an	$⊢ \{r \in Rels \| {I ↾}_{dom r} \subseteq r\} Redund ⟨RefRels, (RefRels \cap SymRels)⟩$

Metamath Proof Explorer

Theorem refrelsredund4

Proof