Theorem dfrefrels2

Description: Alternate definition of the class of reflexive relations. This is a 0-ary class constant, which is recommended for definitions (see the 1. Guideline at https://us.metamath.org/ileuni/mathbox.html ). Proper classes (like _I , see iprc ) are not elements of this (or any) class: if a class is an element of another class, it is not a proper class but a set, see elex . So if we use 0-ary constant classes as our main definitions, they are valid only for sets, not for proper classes. For proper classes we use predicate-type definitions like df-refrel . See also the comment of df-rels .

Note that while elementhood in the class of relations cancels restriction of r in dfrefrels2 , it keeps restriction of _I : this is why the very similar definitions df-refs , df-syms and df-trs diverge when we switch from (general) sets to relations in dfrefrels2 , dfsymrels2 and dftrrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

	Ref	Expression
Assertion	dfrefrels2	⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }

Proof

Step	Hyp	Ref	Expression
1		df-refrels	⊢ RefRels = ( Refs ∩ Rels )
2		df-refs	⊢ Refs = { 𝑟 ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) }
3		inex1g	⊢ ( 𝑟 ∈ V → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V )
4	3	elv	⊢ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V
5		brssr	⊢ ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ) )
6	4 5	ax-mp	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) )
7		elrels6	⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) )
8	7	elv	⊢ ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
9	8	biimpi	⊢ ( 𝑟 ∈ Rels → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 )
10	9	sseq2d	⊢ ( 𝑟 ∈ Rels → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ) )
11	6 10	syl5bb	⊢ ( 𝑟 ∈ Rels → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ) )
12	1 2 11	abeqinbi	⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }