Theorem refrelsredund2

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

	Ref	Expression
Assertion	refrelsredund2	⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , EqvRels ⟩

Proof

Step	Hyp	Ref	Expression
1		refrelsredund4	⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , ( RefRels ∩ SymRels ) ⟩
2		df-eqvrels	⊢ EqvRels = ( ( RefRels ∩ SymRels ) ∩ TrRels )
3		inss1	⊢ ( ( RefRels ∩ SymRels ) ∩ TrRels ) ⊆ ( RefRels ∩ SymRels )
4	2 3	eqsstri	⊢ EqvRels ⊆ ( RefRels ∩ SymRels )
5	4	redundss3	⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , ( RefRels ∩ SymRels ) ⟩ → { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , EqvRels ⟩ )
6	1 5	ax-mp	⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , EqvRels ⟩