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

Metamath Proof Explorer

Theorem dfsymrels2

Description: Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

Ref Expression
Assertion dfsymrels2 SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 }

Proof

Step Hyp Ref Expression
1 df-symrels ⊢ SymRels = ( Syms ∩ Rels )
2 df-syms ⊢ Syms = { 𝑟 ∣ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) }
3 inex1g ⊢ ( 𝑟 ∈ V → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V )
4 3 elv ⊢ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V
5 brssr ⊢ ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
6 4 5 ax-mp ⊢ ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) )
7 elrels6 ⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) )
8 7 elv ⊢ ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
9 8 biimpi ⊢ ( 𝑟 ∈ Rels → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
10 9 cnveqd ⊢ ( 𝑟 ∈ Rels → ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = ◡ 𝑟 )
11 10 9 sseq12d ⊢ ( 𝑟 ∈ Rels → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ 𝑟 ⊆ 𝑟 ) )
12 6 11 bitrid ⊢ ( 𝑟 ∈ Rels → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ 𝑟 ⊆ 𝑟 ) )
13 1 2 12 abeqinbi ⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 }