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 ∣ ◡ 𝑟 ⊆ 𝑟 }