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 = { 𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) }

Proof

Step	Hyp	Ref	Expression
1		df-cnvrefrels	⊢ CnvRefRels = ( CnvRefs ∩ Rels )
2		df-cnvrefs	⊢ CnvRefs = { 𝑟 ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) }
3		dmexg	⊢ ( 𝑟 ∈ V → dom 𝑟 ∈ V )
4	3	elv	⊢ dom 𝑟 ∈ V
5		rnexg	⊢ ( 𝑟 ∈ V → ran 𝑟 ∈ V )
6	5	elv	⊢ ran 𝑟 ∈ V
7	4 6	xpex	⊢ ( dom 𝑟 × ran 𝑟 ) ∈ V
8		inex2g	⊢ ( ( dom 𝑟 × ran 𝑟 ) ∈ V → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V )
9		brcnvssr	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
10	7 8 9	mp2b	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) )
11		elrels6	⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) )
12	11	elv	⊢ ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
13	12	biimpi	⊢ ( 𝑟 ∈ Rels → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
14	13	sseq1d	⊢ ( 𝑟 ∈ Rels → ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
15	10 14	bitrid	⊢ ( 𝑟 ∈ Rels → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
16	1 2 15	abeqinbi	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) }