# Metamath Proof Explorer

## Theorem ener

Description: Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998) (Revised by Mario Carneiro, 15-Nov-2014) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion ener ${⊢}\approx \mathrm{Er}\mathrm{V}$

### Proof

Step Hyp Ref Expression
1 relen ${⊢}\mathrm{Rel}\approx$
2 bren ${⊢}{x}\approx {y}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 vex ${⊢}{x}\in \mathrm{V}$
5 f1ocnv ${⊢}{f}:{x}\underset{1-1 onto}{⟶}{y}\to {{f}}^{-1}:{y}\underset{1-1 onto}{⟶}{x}$
6 f1oen2g ${⊢}\left({y}\in \mathrm{V}\wedge {x}\in \mathrm{V}\wedge {{f}}^{-1}:{y}\underset{1-1 onto}{⟶}{x}\right)\to {y}\approx {x}$
7 3 4 5 6 mp3an12i ${⊢}{f}:{x}\underset{1-1 onto}{⟶}{y}\to {y}\approx {x}$
8 7 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}\to {y}\approx {x}$
9 2 8 sylbi ${⊢}{x}\approx {y}\to {y}\approx {x}$
10 bren ${⊢}{x}\approx {y}↔\exists {g}\phantom{\rule{.4em}{0ex}}{g}:{x}\underset{1-1 onto}{⟶}{y}$
11 bren ${⊢}{y}\approx {z}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{y}\underset{1-1 onto}{⟶}{z}$
12 exdistrv ${⊢}\exists {g}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({g}:{x}\underset{1-1 onto}{⟶}{y}\wedge {f}:{y}\underset{1-1 onto}{⟶}{z}\right)↔\left(\exists {g}\phantom{\rule{.4em}{0ex}}{g}:{x}\underset{1-1 onto}{⟶}{y}\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{y}\underset{1-1 onto}{⟶}{z}\right)$
13 vex ${⊢}{z}\in \mathrm{V}$
14 f1oco ${⊢}\left({f}:{y}\underset{1-1 onto}{⟶}{z}\wedge {g}:{x}\underset{1-1 onto}{⟶}{y}\right)\to \left({f}\circ {g}\right):{x}\underset{1-1 onto}{⟶}{z}$
15 14 ancoms ${⊢}\left({g}:{x}\underset{1-1 onto}{⟶}{y}\wedge {f}:{y}\underset{1-1 onto}{⟶}{z}\right)\to \left({f}\circ {g}\right):{x}\underset{1-1 onto}{⟶}{z}$
16 f1oen2g ${⊢}\left({x}\in \mathrm{V}\wedge {z}\in \mathrm{V}\wedge \left({f}\circ {g}\right):{x}\underset{1-1 onto}{⟶}{z}\right)\to {x}\approx {z}$
17 4 13 15 16 mp3an12i ${⊢}\left({g}:{x}\underset{1-1 onto}{⟶}{y}\wedge {f}:{y}\underset{1-1 onto}{⟶}{z}\right)\to {x}\approx {z}$
18 17 exlimivv ${⊢}\exists {g}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({g}:{x}\underset{1-1 onto}{⟶}{y}\wedge {f}:{y}\underset{1-1 onto}{⟶}{z}\right)\to {x}\approx {z}$
19 12 18 sylbir ${⊢}\left(\exists {g}\phantom{\rule{.4em}{0ex}}{g}:{x}\underset{1-1 onto}{⟶}{y}\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{y}\underset{1-1 onto}{⟶}{z}\right)\to {x}\approx {z}$
20 10 11 19 syl2anb ${⊢}\left({x}\approx {y}\wedge {y}\approx {z}\right)\to {x}\approx {z}$
21 4 enref ${⊢}{x}\approx {x}$
22 4 21 2th ${⊢}{x}\in \mathrm{V}↔{x}\approx {x}$
23 1 9 20 22 iseri ${⊢}\approx \mathrm{Er}\mathrm{V}$