Metamath Proof Explorer

Theorem dfsymrels2

Description: Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

Ref Expression
Assertion dfsymrels2 
|- SymRels = { r e. Rels | `' r C_ r }

Proof

Step Hyp Ref Expression
1 df-symrels 
 |-  SymRels = ( Syms i^i Rels )
2 df-syms 
 |-  Syms = { r | `' ( r i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) }
3 inex1g 
 |-  ( r e. _V -> ( r i^i ( dom r X. ran r ) ) e. _V )
4 3 elv 
 |-  ( r i^i ( dom r X. ran r ) ) e. _V
5 brssr 
 |-  ( ( r i^i ( dom r X. ran r ) ) e. _V -> ( `' ( r i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> `' ( r i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) ) )
6 4 5 ax-mp 
 |-  ( `' ( r i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> `' ( r i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) )
7 elrels6 
 |-  ( r e. _V -> ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r ) )
8 7 elv 
 |-  ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r )
9 8 biimpi 
 |-  ( r e. Rels -> ( r i^i ( dom r X. ran r ) ) = r )
10 9 cnveqd 
 |-  ( r e. Rels -> `' ( r i^i ( dom r X. ran r ) ) = `' r )
11 10 9 sseq12d 
 |-  ( r e. Rels -> ( `' ( r i^i ( dom r X. ran r ) ) C_ ( r i^i ( dom r X. ran r ) ) <-> `' r C_ r ) )
12 6 11 syl5bb 
 |-  ( r e. Rels -> ( `' ( r i^i ( dom r X. ran r ) ) _S ( r i^i ( dom r X. ran r ) ) <-> `' r C_ r ) )
13 1 2 12 abeqinbi 
 |-  SymRels = { r e. Rels | `' r C_ r }