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

Metamath Proof Explorer

Definition df-er

Description: Define the equivalence relation predicate. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref , ersymb , and ertr . (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 2-Nov-2015)

Ref Expression
Assertion df-er ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 cA ⊢ 𝐴
2 1 0 wer ⊢ 𝑅 Er 𝐴
3 0 wrel ⊢ Rel 𝑅
4 0 cdm ⊢ dom 𝑅
5 4 1 wceq ⊢ dom 𝑅 = 𝐴
6 0 ccnv ⊢ ◡ 𝑅
7 0 0 ccom ⊢ ( 𝑅 ∘ 𝑅 )
8 6 7 cun ⊢ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) )
9 8 0 wss ⊢ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅
10 3 5 9 w3a ⊢ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
11 2 10 wb ⊢ ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )