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\leftrightarrow \exists ff: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 ff: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\leftrightarrow \exists gg:x\underset{1-1\; onto}{⟶}y$$
11		bren	$$⊢y\approx z\leftrightarrow \exists ff:y\underset{1-1\; onto}{⟶}z$$
12		exdistrv	$$⊢\exists g\exists f\left(g:x\underset{1-1\; onto}{⟶}y\wedge f:y\underset{1-1\; onto}{⟶}z\right)\leftrightarrow \left(\exists gg:x\underset{1-1\; onto}{⟶}y\wedge \exists ff: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\exists f\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 gg:x\underset{1-1\; onto}{⟶}y\wedge \exists ff: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}\leftrightarrow x\approx x$$
23	1 9 20 22	iseri	$$⊢\approx \mathrm{Er}\mathrm{V}$$