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

Metamath Proof Explorer

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 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) }