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

Metamath Proof Explorer

Theorem dfcnvrefrels2

Description: Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 . (Contributed by Peter Mazsa, 21-Jul-2021)

Ref Expression
Assertion dfcnvrefrels2 
|- CnvRefRels = { r e. Rels | r C_ ( _I i^i ( dom r X. ran r ) ) }

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 dmexg 
 |-  ( r e. _V -> dom r e. _V )
4 3 elv 
 |-  dom r e. _V
5 rnexg 
 |-  ( r e. _V -> ran r e. _V )
6 5 elv 
 |-  ran r e. _V
7 4 6 xpex 
 |-  ( dom r X. ran r ) e. _V
8 inex2g 
 |-  ( ( dom r X. ran r ) e. _V -> ( _I i^i ( dom r X. ran r ) ) e. _V )
9 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 ) ) ) )
10 7 8 9 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 ) ) )
11 elrels6 
 |-  ( r e. _V -> ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r ) )
12 11 elv 
 |-  ( r e. Rels <-> ( r i^i ( dom r X. ran r ) ) = r )
13 12 biimpi 
 |-  ( r e. Rels -> ( r i^i ( dom r X. ran r ) ) = r )
14 13 sseq1d 
 |-  ( r e. Rels -> ( ( r i^i ( dom r X. ran r ) ) C_ ( _I i^i ( dom r X. ran r ) ) <-> r C_ ( _I i^i ( dom r X. ran r ) ) ) )
15 10 14 bitrid 
 |-  ( r e. Rels -> ( ( _I i^i ( dom r X. ran r ) ) `' _S ( r i^i ( dom r X. ran r ) ) <-> r C_ ( _I i^i ( dom r X. ran r ) ) ) )
16 1 2 15 abeqinbi 
 |-  CnvRefRels = { r e. Rels | r C_ ( _I i^i ( dom r X. ran r ) ) }