Metamath Proof Explorer

Theorem refsymrel2

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrel2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion refsymrel2 
|- ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 dfrefrel2 
 |-  ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
2 dfsymrel2 
 |-  ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
3 1 2 anbi12i 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) /\ ( `' R C_ R /\ Rel R ) ) )
4 anandi3r 
 |-  ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R /\ `' R C_ R ) <-> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) /\ ( `' R C_ R /\ Rel R ) ) )
5 3anan32 
 |-  ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R /\ `' R C_ R ) <-> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ `' R C_ R ) /\ Rel R ) )
6 3 4 5 3bitr2i 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ `' R C_ R ) /\ Rel R ) )
7 symrefref2 
 |-  ( `' R C_ R -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) )
8 7 pm5.32ri 
 |-  ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ `' R C_ R ) <-> ( ( _I |` dom R ) C_ R /\ `' R C_ R ) )
9 8 anbi1i 
 |-  ( ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ `' R C_ R ) /\ Rel R ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) )
10 6 9 bitri 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) )