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

Metamath Proof Explorer

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 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) }