Definition df-symrel

Description: Define the symmetric relation predicate. (Read: R is a symmetric relation.) For sets, being an element of the class of symmetric relations ( df-symrels ) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel . Alternate definitions are dfsymrel2 and dfsymrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)

	Ref	Expression
Assertion	df-symrel	⊢ ( SymRel 𝑅 ↔ ( ◡ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	wsymrel	⊢ SymRel 𝑅
2	0	cdm	⊢ dom 𝑅
3	0	crn	⊢ ran 𝑅
4	2 3	cxp	⊢ ( dom 𝑅 × ran 𝑅 )
5	0 4	cin	⊢ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
6	5	ccnv	⊢ ◡ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
7	6 5	wss	⊢ ◡ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
8	0	wrel	⊢ Rel 𝑅
9	7 8	wa	⊢ ( ◡ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 )
10	1 9	wb	⊢ ( SymRel 𝑅 ↔ ( ◡ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) )