Metamath Proof Explorer

Theorem dfcnvrefrels3

Description: Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion dfcnvrefrels3 
|- CnvRefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x r y -> x = y ) }

Proof

Step Hyp Ref Expression
1 df-cnvrefrels 
 |-  CnvRefRels = ( CnvRefs i^i Rels )
2 df-cnvrefs 
 |-  CnvRefs = { r | ( _I i^i ( dom r X. ran r ) ) `' _S ( r i^i ( dom r X. ran r ) ) }
3 1 2 abeqin 
 |-  CnvRefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) `' _S ( r i^i ( dom r X. ran r ) ) }
4 dmexg 
 |-  ( r e. _V -> dom r e. _V )
5 4 elv 
 |-  dom r e. _V
6 rnexg 
 |-  ( r e. _V -> ran r e. _V )
7 6 elv 
 |-  ran r e. _V
8 5 7 xpex 
 |-  ( dom r X. ran r ) e. _V
9 inex2g 
 |-  ( ( dom r X. ran r ) e. _V -> ( _I i^i ( dom r X. ran r ) ) e. _V )
10 brcnvssr 
 |-  ( ( _I i^i ( dom r X. ran r ) ) e. _V -> ( ( _I 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_ ( _I i^i ( dom r X. ran r ) ) ) )
11 8 9 10 mp2b 
 |-  ( ( _I 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_ ( _I i^i ( dom r X. ran r ) ) )
12 inxpssidinxp 
 |-  ( ( r i^i ( dom r X. ran r ) ) C_ ( _I i^i ( dom r X. ran r ) ) <-> A. x e. dom r A. y e. ran r ( x r y -> x = y ) )
13 11 12 bitri 
 |-  ( ( _I i^i ( dom r X. ran r ) ) `' _S ( r i^i ( dom r X. ran r ) ) <-> A. x e. dom r A. y e. ran r ( x r y -> x = y ) )
14 3 13 rabbieq 
 |-  CnvRefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x r y -> x = y ) }