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

Metamath Proof Explorer

Definition df-comembers

Description: Define the class of comember equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022) (Revised by Peter Mazsa, 24-Jul-2023)

Ref Expression
Assertion df-comembers CoMembErs = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccomembers ⊢ CoMembErs
1 va ⊢ 𝑎
2 cep ⊢ E
3 2 ccnv ⊢ ◡ E
4 1 cv ⊢ 𝑎
5 3 4 cres ⊢ ( ◡ E ↾ 𝑎 )
6 5 ccoss ⊢ ≀ ( ◡ E ↾ 𝑎 )
7 cers ⊢ Ers
8 6 4 7 wbr ⊢ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎
9 8 1 cab ⊢ { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }
10 0 9 wceq ⊢ CoMembErs = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }