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

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 = { 𝑟 ∈ 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 𝑟 ) ) }