Metamath Proof Explorer


Theorem 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 Rels | I dom r r Redund RefRels RefRels SymRels

Proof

Step Hyp Ref Expression
1 inxpssres I dom r × ran r I dom r
2 sstr2 I dom r × ran r I dom r I dom r r I dom r × ran r r
3 1 2 ax-mp I dom r r I dom r × ran r r
4 3 ssrabi r Rels | I dom r r r Rels | I dom r × ran r r
5 dfrefrels2 RefRels = r Rels | I dom r × ran r r
6 4 5 sseqtrri r Rels | I dom r r RefRels
7 in32 r Rels | I dom r r SymRels RefRels = r Rels | I dom r r RefRels SymRels
8 inrab r Rels | I dom r r r Rels | r -1 r = r Rels | I dom r r r -1 r
9 dfsymrels2 SymRels = r Rels | r -1 r
10 9 ineq2i r Rels | I dom r r SymRels = r Rels | I dom r r r Rels | r -1 r
11 refsymrels2 RefRels SymRels = r Rels | I dom r r r -1 r
12 8 10 11 3eqtr4i r Rels | I dom r r SymRels = RefRels SymRels
13 12 ineq1i r Rels | I dom r r SymRels RefRels = RefRels SymRels RefRels
14 inass r Rels | I dom r r RefRels SymRels = r Rels | I dom r r RefRels SymRels
15 7 13 14 3eqtr3ri r Rels | I dom r r RefRels SymRels = RefRels SymRels RefRels
16 in32 RefRels SymRels RefRels = RefRels RefRels SymRels
17 inass RefRels RefRels SymRels = RefRels RefRels SymRels
18 15 16 17 3eqtri r Rels | I dom r r RefRels SymRels = RefRels RefRels SymRels
19 df-redund r Rels | I dom r r Redund RefRels RefRels SymRels r Rels | I dom r r RefRels r Rels | I dom r r RefRels SymRels = RefRels RefRels SymRels
20 6 18 19 mpbir2an r Rels | I dom r r Redund RefRels RefRels SymRels