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 Rels | r I dom r × ran r

Proof

Step Hyp Ref Expression
1 df-cnvrefrels CnvRefRels = CnvRefs Rels
2 df-cnvrefs CnvRefs = r | I dom r × ran r S -1 r dom r × ran r
3 dmexg r V dom r V
4 3 elv dom r V
5 rnexg r V ran r V
6 5 elv ran r V
7 4 6 xpex dom r × ran r V
8 inex2g dom r × ran r V I dom r × ran r V
9 brcnvssr I dom r × ran r V I dom r × ran r S -1 r dom r × ran r r dom r × ran r I dom r × ran r
10 7 8 9 mp2b I dom r × ran r S -1 r dom r × ran r r dom r × ran r I dom r × ran r
11 elrels6 r V r Rels r dom r × ran r = r
12 11 elv r Rels r dom r × ran r = r
13 12 biimpi r Rels r dom r × ran r = r
14 13 sseq1d r Rels r dom r × ran r I dom r × ran r r I dom r × ran r
15 10 14 syl5bb r Rels I dom r × ran r S -1 r dom r × ran r r I dom r × ran r
16 1 2 15 abeqinbi CnvRefRels = r Rels | r I dom r × ran r