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

Metamath Proof Explorer

Definition df-symrel

Description: Define the symmetric relation predicate. (Read: R is a symmetric relation.) For sets, being an element of the class of symmetric relations ( df-symrels ) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel . Alternate definitions are dfsymrel2 and dfsymrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)

Ref Expression
Assertion df-symrel 
|- ( SymRel R <-> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 wsymrel 
 |-  SymRel R
2 0 cdm 
 |-  dom R
3 0 crn 
 |-  ran R
4 2 3 cxp 
 |-  ( dom R X. ran R )
5 0 4 cin 
 |-  ( R i^i ( dom R X. ran R ) )
6 5 ccnv 
 |-  `' ( R i^i ( dom R X. ran R ) )
7 6 5 wss 
 |-  `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) )
8 0 wrel 
 |-  Rel R
9 7 8 wa 
 |-  ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R )
10 1 9 wb 
 |-  ( SymRel R <-> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )