Theorem dfcnvrefrels3

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

	Ref	Expression
Assertion	dfcnvrefrels3	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		df-cnvrefrels	⊢ CnvRefRels = ( CnvRefs ∩ Rels )
2		df-cnvrefs	⊢ CnvRefs = { 𝑟 ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) }
3	1 2	abeqin	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) }
4		dmexg	⊢ ( 𝑟 ∈ V → dom 𝑟 ∈ V )
5	4	elv	⊢ dom 𝑟 ∈ V
6		rnexg	⊢ ( 𝑟 ∈ V → ran 𝑟 ∈ V )
7	6	elv	⊢ ran 𝑟 ∈ V
8	5 7	xpex	⊢ ( dom 𝑟 × ran 𝑟 ) ∈ V
9		inex2g	⊢ ( ( dom 𝑟 × ran 𝑟 ) ∈ V → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V )
10		brcnvssr	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
11	8 9 10	mp2b	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) )
12		inxpssidinxp	⊢ ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) )
13	11 12	bitri	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) )
14	3 13	rabbieq	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) }