Theorem refrelsredund3

Description: The naive version of the class of reflexive relations { r e. Rels | A. x e. dom r x r x } is redundant with respect to the class of reflexive relations (see dfrefrels3 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

	Ref	Expression
Assertion	refrelsredund3	⊢ { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 } Redund ⟨ RefRels , EqvRels ⟩

Proof

Step	Hyp	Ref	Expression
1		refrelsredund2	⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , EqvRels ⟩
2		idrefALT	⊢ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 )
3	2	rabbii	⊢ { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 }
4	3	redundeq1	⊢ ( { 𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟 ) ⊆ 𝑟 } Redund ⟨ RefRels , EqvRels ⟩ ↔ { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 } Redund ⟨ RefRels , EqvRels ⟩ )
5	1 4	mpbi	⊢ { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 } Redund ⟨ RefRels , EqvRels ⟩