Metamath Proof Explorer


Theorem refrelredund4

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

Ref Expression
Assertion refrelredund4 redund I dom R R Rel R RefRel R RefRel R SymRel R

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 anim1i I dom R R Rel R I dom R × ran R R Rel R
5 dfrefrel2 RefRel R I dom R × ran R R Rel R
6 4 5 sylibr I dom R R Rel R RefRel R
7 an12 I dom R R Rel R RefRel R SymRel R RefRel R I dom R R Rel R SymRel R
8 anandir I dom R R R -1 R Rel R I dom R R Rel R R -1 R Rel R
9 refsymrel2 RefRel R SymRel R I dom R R R -1 R Rel R
10 dfsymrel2 SymRel R R -1 R Rel R
11 10 anbi2i I dom R R Rel R SymRel R I dom R R Rel R R -1 R Rel R
12 8 9 11 3bitr4i RefRel R SymRel R I dom R R Rel R SymRel R
13 12 anbi2i RefRel R RefRel R SymRel R RefRel R I dom R R Rel R SymRel R
14 7 13 bitr4i I dom R R Rel R RefRel R SymRel R RefRel R RefRel R SymRel R
15 df-redundp redund I dom R R Rel R RefRel R RefRel R SymRel R I dom R R Rel R RefRel R I dom R R Rel R RefRel R SymRel R RefRel R RefRel R SymRel R
16 6 14 15 mpbir2an redund I dom R R Rel R RefRel R RefRel R SymRel R