This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem refsymrel3

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the A. x e. dom R x R x version for its reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrel3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion refsymrel3 
|- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 dfrefrel3 
 |-  ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) )
2 dfsymrel3 
 |-  ( SymRel R <-> ( A. x A. y ( x R y -> y R x ) /\ Rel R ) )
3 1 2 anbi12i 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) /\ ( A. x A. y ( x R y -> y R x ) /\ Rel R ) ) )
4 anandi3r 
 |-  ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R /\ A. x A. y ( x R y -> y R x ) ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) /\ ( A. x A. y ( x R y -> y R x ) /\ Rel R ) ) )
5 3anan32 
 |-  ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R /\ A. x A. y ( x R y -> y R x ) ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
6 3 4 5 3bitr2i 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
7 symrefref3 
 |-  ( A. x A. y ( x R y -> y R x ) -> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) )
8 7 pm5.32ri 
 |-  ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) <-> ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) )
9 8 anbi1i 
 |-  ( ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
10 6 9 bitri 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )