Theorem dfeqvrels3

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

	Ref	Expression
Assertion	dfeqvrels3	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) }

Proof

Step	Hyp	Ref	Expression
1		dfeqvrels2	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
2		idrefALT	⊢ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 )
3		cnvsym	⊢ ( ◡ 𝑟 ⊆ 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) )
4		cotr	⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) )
5	2 3 4	3anbi123i	⊢ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) )
6	1 5	rabbieq	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) }