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

Metamath Proof Explorer

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 𝑅 ) )