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	syl5bb	|- ( 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 ) ) }