Definition df-refrel

Description: Define the reflexive relation predicate. (Read: R is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 . Alternate definitions are dfrefrel2 and dfrefrel3 . For sets, being an element of the class of reflexive relations ( df-refrels ) is equivalent to satisfying the reflexive relation predicate, that is ( R e. RefRels <-> RefRel R ) when R is a set, see elrefrelsrel . (Contributed by Peter Mazsa, 16-Jul-2021)

	Ref	Expression
Assertion	df-refrel	⊢ ( RefRel 𝑅 ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) )

Detailed syntax breakdown

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