# Metamath Proof Explorer

## Theorem dfcoels

Description: Alternate definition of the class of coelements on the class A . (Contributed by Peter Mazsa, 20-Apr-2019)

Ref Expression
Assertion dfcoels ${⊢}\sim {A}=\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 df-coels ${⊢}\sim {A}=\wr \left({{\mathrm{E}}^{-1}↾}_{{A}}\right)$
2 1cossres ${⊢}\wr \left({{\mathrm{E}}^{-1}↾}_{{A}}\right)=\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({u}{\mathrm{E}}^{-1}{x}\wedge {u}{\mathrm{E}}^{-1}{y}\right)\right\}$
3 brcnvep ${⊢}{u}\in \mathrm{V}\to \left({u}{\mathrm{E}}^{-1}{x}↔{x}\in {u}\right)$
4 3 elv ${⊢}{u}{\mathrm{E}}^{-1}{x}↔{x}\in {u}$
5 brcnvep ${⊢}{u}\in \mathrm{V}\to \left({u}{\mathrm{E}}^{-1}{y}↔{y}\in {u}\right)$
6 5 elv ${⊢}{u}{\mathrm{E}}^{-1}{y}↔{y}\in {u}$
7 4 6 anbi12i ${⊢}\left({u}{\mathrm{E}}^{-1}{x}\wedge {u}{\mathrm{E}}^{-1}{y}\right)↔\left({x}\in {u}\wedge {y}\in {u}\right)$
8 7 rexbii ${⊢}\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({u}{\mathrm{E}}^{-1}{x}\wedge {u}{\mathrm{E}}^{-1}{y}\right)↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)$
9 8 opabbii ${⊢}\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({u}{\mathrm{E}}^{-1}{x}\wedge {u}{\mathrm{E}}^{-1}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)\right\}$
10 1 2 9 3eqtri ${⊢}\sim {A}=\left\{⟨{x},{y}⟩|\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\wedge {y}\in {u}\right)\right\}$